RelativeAmbiguity.lean

1 import KomorebiSpace.RelativeSections
2 import KomorebiSpace.NonabelianExtensionFibers
3 
4 set_option autoImplicit false
5 set_option backward.isDefEq.respectTransparency false
6 
7 /-!
8 # The group of invisible coherent changes under equivalent views
9 
10 This is the existing ambiguity group, with its actual multiplication. The
11 comparison is a multiplicative equivalence, and it intertwines the previously
12 proved parametrization of all extensions after choosing a base extension.
13 -/
14 universe u₁ u₂ v₁ v₂ w
15 namespace KomorebiSpace
16 open CategoryTheory
17 namespace GroupViewSystem
18 variable {V : Type u₁} [Category.{v₁} V]
19 variable {W : Type u₂} [Category.{v₂} W]
20 variable {G : W → Type w} [∀ a, Group (G a)]
21 variable (F : GroupViewSystem W G)
22 
23 /-- Coherent invisible changes pull back without altering their group law. -/
24 def reindexInvisible (H : V ⥤ W) (U : Set W) (a : F.invisible U) :
25     (F.reindex H).invisible (H.obj ⁻¹' U) :=
26   ⟨fun v => a.val (H.obj v),
27     ⟨fun v w f => a.property.1 (H.obj v) (H.obj w) (H.map f),
28      fun v => a.property.2 ⟨H.obj v.val,v.property⟩⟩⟩
29 
30 /-- Recover invisibility at every prescribed target view using saturation. -/
31 def recoverInvisible (e : V ≌ W) (U : Set W) (hU : CompositionSite.IsoClosed U)
32     (a : (F.reindex e.functor).invisible (e.functor.obj ⁻¹' U)) : F.invisible U := by
33   let y : (F.views.reindex e.functor).Ambient := ⟨a.val,a.property.1⟩
34   let x := F.views.recoverSection e y
35   refine ⟨x.val, x.property, ?_⟩
36   intro w
37   have hm : e.functor.obj (e.inverse.obj w.val) ∈ U :=
38     hU (e.counitIso.app w.val).symm w.property
39   change F.pull (returnArrow e w.val) (a.val (e.inverse.obj w.val)) = 1
40   rw [a.property.2 ⟨e.inverse.obj w.val,hm⟩, map_one]
41 
42 /-- The complete nonabelian ambiguity group is preserved, not just its cardinality. -/
43 def invisibleViewEquivalence (e : V ≌ W) (U : Set W)
44     (hU : CompositionSite.IsoClosed U) :
45     F.invisible U ≃* (F.reindex e.functor).invisible (e.functor.obj ⁻¹' U) where
46   toFun := F.reindexInvisible e.functor U
47   invFun := F.recoverInvisible e U hU
48   left_inv a := by
49     apply Subtype.ext
50     funext w
51     exact a.property.1 _ _ (returnArrow e w)
52   right_inv a := by
53     apply Subtype.ext
54     funext v
55     change F.pull (returnArrow e (e.functor.obj v))
56       (a.val (e.inverse.obj (e.functor.obj v))) = a.val v
57     rw [← mapped_unit_eq_return e v]
58     exact a.property.1 _ _ (e.unitIso.hom.app v)
59   map_mul' _ _ := rfl
60 
61 @[simp] theorem invisibleViewEquivalence_coordinate (e : V ≌ W) (U : Set W)
62     (hU : CompositionSite.IsoClosed U) (a : F.invisible U) (v : V) :
63     (F.invisibleViewEquivalence e U hU a).val v = a.val (e.functor.obj v) := rfl
64 
65 /-- The action parametrizing possible extensions agrees with view pullback. -/
66 theorem extensionParameters_reindex (e : V ≌ W) (U : Set W)
67     (hU : CompositionSite.IsoClosed U) (c : F.Cocycle)
68     (s : (F.twistedViews c).Partial U) (base : (F.twistedViews c).Extensions U s)
69     (a : F.invisible U) :
70     F.relativeTwistedEquivalence e U hU c s (F.extensionParameters c U s base a) =
71       (F.reindex e.functor).extensionParameters (F.reindexCocycle e.functor c)
72         (e.functor.obj ⁻¹' U) ((F.twistedViews c).reindexPartial e.functor U s)
73         (F.relativeTwistedEquivalence e U hU c s base)
74         (F.invisibleViewEquivalence e U hU a) := by
75   apply Subtype.ext
76   apply ViewSystem.Ambient.ext
77   intro v
78   rfl
79 
80 /-- The full existence-and-uniqueness condition is invariant for the transported problem. -/
81 theorem relative_unique_iff (e : V ≌ W) (U : Set W)
82     (hU : CompositionSite.IsoClosed U) (c : F.Cocycle)
83     (s : (F.twistedViews c).Partial U) :
84     (∃! x : (F.twistedViews c).Ambient, (F.twistedViews c).restrict U x = s) ↔
85       (∃! y : ((F.reindex e.functor).twistedViews (F.reindexCocycle e.functor c)).Ambient,
86         ((F.reindex e.functor).twistedViews (F.reindexCocycle e.functor c)).restrict
87           (e.functor.obj ⁻¹' U) y = (F.twistedViews c).reindexPartial e.functor U s) := by
88   rw [F.unique_extension_iff, (F.reindex e.functor).unique_extension_iff]
89   exact and_congr (F.relative_neutral_iff e U hU c s)
90     (F.invisibleViewEquivalence e U hU).toEquiv.subsingleton_congr
91 
92 end GroupViewSystem
93 end KomorebiSpace

Back to source controls