NonabelianExtensionFibers.lean

1 import KomorebiSpace.NonabelianExtension
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Nonabelian extension fibers and invisible coherent changes
7 
8 The action on trivializations is free and transitive when a base exists.
9 This must not be confused with the generally nontrivial stabilizers of
10 cocycle objects in the gauge groupoid.
11 -/
12 universe u v w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace GroupViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable {G : V → Type w} [∀ a, Group (G a)]
18 variable (F : GroupViewSystem V G)
19 
20 def invisible (U : Set V) : Subgroup (∀ v, G v) where
21   carrier := {h | (∀ v w (f : v ⟶ w), F.pull f (h w) = h v) ∧ ∀ v : U, h v.val = 1}
22   one_mem' := ⟨by intros; exact map_one _, by intros; rfl⟩
23   mul_mem' := by
24     intro a b ha hb
25     constructor
26     · intro v w f
27       change F.pull f (a w * b w) = a v * b v
28       rw [map_mul, ha.1, hb.1]
29     · intro v
30       change a v.val * b v.val = 1
31       rw [ha.2 v, hb.2 v, one_mul]
32   inv_mem' := by
33     intro a ha
34     constructor
35     · intro v w f
36       change F.pull f ((a w)⁻¹) = (a v)⁻¹
37       rw [map_inv, ha.1]
38     · intro v
39       change (a v.val)⁻¹ = 1
40       rw [ha.2 v, inv_one]
41 
42 /-- The identity-label stabilizer is exactly the invisible coherent group. -/
43 def invisibleStabilizerEquiv (U : Set V) : F.invisible U ≃* F.stabilizer U F.trivial where
44   toFun h := ⟨⟨h.val, h.property.2⟩, (F.trivial_stabilizer_iff U _).mpr h.property.1⟩
45   invFun h := ⟨h.val.val, (F.trivial_stabilizer_iff U _).mp h.property, h.val.property⟩
46   left_inv _ := rfl
47   right_inv _ := rfl
48   map_mul' _ _ := rfl
49 
50 /-- A chosen twisted global extension parametrizes all the others by right multiplication. -/
51 def extensionParameters (c : F.Cocycle) (U : Set V)
52     (s : (F.twistedViews c).Partial U)
53     (base : (F.twistedViews c).Extensions U s) :
54     F.invisible U ≃ (F.twistedViews c).Extensions U s where
55   toFun h := ⟨⟨fun v => base.val.val v * h.val v, by
56     intro v w f
57     change c.edge f * F.pull f (base.val.val w * h.val w) = base.val.val v * h.val v
58     rw [map_mul, ← mul_assoc]
59     have hb := base.val.property v w f
60     change c.edge f * F.pull f (base.val.val w) = base.val.val v at hb
61     rw [hb, h.property.1]⟩, by
62     apply ViewSystem.Partial.ext
63     intro v
64     change base.val.val v.val * h.val v.val = s.val v
65     rw [h.property.2 v, mul_one]
66     exact congrArg (fun t : (F.twistedViews c).Partial U => t.val v) base.property⟩
67   invFun x := ⟨fun v => (base.val.val v)⁻¹ * x.val.val v, by
68     constructor
69     · intro v w f
70       change F.pull f ((base.val.val w)⁻¹ * x.val.val w) = (base.val.val v)⁻¹ * x.val.val v
71       rw [map_mul, map_inv]
72       have hb := base.val.property v w f
73       have hx := x.val.property v w f
74       change c.edge f * F.pull f (base.val.val w) = base.val.val v at hb
75       change c.edge f * F.pull f (x.val.val w) = x.val.val v at hx
76       rw [← hb, ← hx]
77       group
78     · intro v
79       change (base.val.val v.val)⁻¹ * x.val.val v.val = 1
80       have hb := congrArg (fun t : (F.twistedViews c).Partial U => t.val v) base.property
81       have hx := congrArg (fun t : (F.twistedViews c).Partial U => t.val v) x.property
82       change base.val.val v.val = s.val v at hb
83       change x.val.val v.val = s.val v at hx
84       rw [hb, hx]; group⟩
85   left_inv h := by apply Subtype.ext; funext v; change _⁻¹ * (_ * _) = _; group
86   right_inv x := by
87     apply Subtype.ext
88     apply ViewSystem.Ambient.ext
89     intro v
90     change _ * (_⁻¹ * _) = _
91     group
92 
93 @[simp] theorem extensionParameters_coordinate (c : F.Cocycle) (U : Set V)
94     (s : (F.twistedViews c).Partial U) (base : (F.twistedViews c).Extensions U s)
95     (h : F.invisible U) (v : V) :
96     (F.extensionParameters c U s base h).val.val v = base.val.val v * h.val v := rfl
97 
98 @[simp] theorem extensionParameters_inverse (c : F.Cocycle) (U : Set V)
99     (s : (F.twistedViews c).Partial U) (base x : (F.twistedViews c).Extensions U s) (v : V) :
100     ((F.extensionParameters c U s base).symm x).val v = (base.val.val v)⁻¹ * x.val.val v := rfl
101 
102 theorem extension_subsingleton_iff (c : F.Cocycle) (U : Set V)
103     (s : (F.twistedViews c).Partial U) (base : (F.twistedViews c).Extensions U s) :
104     Subsingleton ((F.twistedViews c).Extensions U s) ↔ Subsingleton (F.invisible U) :=
105   (F.extensionParameters c U s base).subsingleton_congr.symm
106 
107 theorem unique_extension_iff (c : F.Cocycle) (U : Set V)
108     (s : (F.twistedViews c).Partial U) :
109     (∃! x : (F.twistedViews c).Ambient, (F.twistedViews c).restrict U x = s) ↔
110       F.extensionOrbit c U s = F.neutralClass U ∧ Subsingleton (F.invisible U) := by
111   constructor
112   · rintro ⟨x, hx, hu⟩
113     let base : (F.twistedViews c).Extensions U s := ⟨x, hx⟩
114     refine ⟨(F.extensionOrbit_neutral_iff c U s).mpr ⟨base⟩, ?_⟩
115     apply (F.extension_subsingleton_iff c U s base).mp
116     refine ⟨fun a b => ?_⟩
117     apply Subtype.ext
118     exact (hu a.val a.property).trans (hu b.val b.property).symm
119   · rintro ⟨ho, hh⟩
120     obtain ⟨base⟩ := (F.extensionOrbit_neutral_iff c U s).mp ho
121     have hs := (F.extension_subsingleton_iff c U s base).mpr hh
122     refine ⟨base.val, base.property, ?_⟩
123     intro x hx
124     exact congrArg Subtype.val (hs.elim (⟨x, hx⟩ : (F.twistedViews c).Extensions U s) base)
125 
126 theorem invisible_antitone {U W : Set V} (h : U ⊆ W) : F.invisible W ≤ F.invisible U := by
127   intro a ha
128   exact ⟨ha.1, fun v => ha.2 ⟨v.val, h v.property⟩⟩
129 
130 end GroupViewSystem
131 end KomorebiSpace

Back to source controls