CocycleGaugeGroupoid.lean

1 import KomorebiSpace.GroupViewSystems
2 import Mathlib.CategoryTheory.Groupoid
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The groupoid of cocycles and framed gauge changes
8 
9 Gauge changes are identity on a prescribed view domain. The orbit quotient
10 forgets automorphisms; the groupoid deliberately retains them. Its objects
11 are coherent cocycles, not arbitrary inconsistent transition labels.
12 -/
13 universe u v w
14 namespace KomorebiSpace
15 open CategoryTheory
16 namespace GroupViewSystem
17 variable {V : Type u} [Category.{v} V]
18 variable {G : V → Type w} [∀ a, Group (G a)]
19 variable (F : GroupViewSystem V G)
20 
21 /-- Allowed gauge changes keep every prescribed local trivialization fixed. -/
22 def basedGauge (_F : GroupViewSystem V G) (U : Set V) : Subgroup (∀ v, G v) where
23   carrier := {a | ∀ v : U, a v.val = 1}
24   one_mem' := by intro v; rfl
25   mul_mem' := by intro a b ha hb v; change a v.val * b v.val = 1; rw [ha v, hb v, one_mul]
26   inv_mem' := by intro a ha v; change (a v.val)⁻¹ = 1; rw [ha v, inv_one]
27 
28 /-- A wrapper keeps the framing domain visible to typeclass inference. -/
29 structure GaugeObject (U : Set V) where
30   labels : F.Cocycle
31 
32 namespace GaugeObject
33 variable {F} {U : Set V}
34 structure Hom (c d : F.GaugeObject U) where
35   change : F.basedGauge U
36   target : F.gauge change.val c.labels = d.labels
37 
38 @[ext] theorem Hom.ext {c d : F.GaugeObject U} {a b : Hom c d}
39     (h : a.change = b.change) : a = b := by cases a; cases b; cases h; rfl
40 
41 def identity (c : F.GaugeObject U) : Hom c c :=
42   ⟨1, F.gauge_one c.labels⟩
43 
44 def compose {c d e : F.GaugeObject U} (a : Hom c d) (b : Hom d e) : Hom c e :=
45   ⟨b.change * a.change, by
46     change F.gauge (b.change.val * a.change.val) c.labels = e.labels
47     rw [← F.gauge_mul, a.target, b.target]⟩
48 
49 def reverse {c d : F.GaugeObject U} (a : Hom c d) : Hom d c :=
50   ⟨a.change⁻¹, by
51     change F.gauge a.change.val⁻¹ d.labels = c.labels
52     rw [← a.target, F.gauge_inv_gauge]⟩
53 
54 instance : Groupoid (F.GaugeObject U) where
55   Hom := Hom
56   id := identity
57   comp := compose
58   id_comp := by intro c d a; apply Hom.ext; exact mul_one _
59   comp_id := by intro c d a; apply Hom.ext; exact one_mul _
60   assoc := by intro b c d e a h k; apply Hom.ext; exact (mul_assoc _ _ _).symm
61   inv := reverse
62   inv_comp := by intro c d a; apply Hom.ext; exact mul_inv_cancel _
63   comp_inv := by intro c d a; apply Hom.ext; exact inv_mul_cancel _
64 
65 @[simp] theorem composition_change {c d e : F.GaugeObject U}
66     (a : c ⟶ d) (b : d ⟶ e) : (a ≫ b).change = b.change * a.change := rfl
67 
68 @[simp] theorem inverse_change {c d : F.GaugeObject U} (a : c ⟶ d) :
69     (Groupoid.inv a).change = a.change⁻¹ := rfl
70 end GaugeObject
71 
72 /-- Explicit orbit relation. This is not defined by solvability of an extension. -/
73 def GaugeEquivalent (U : Set V) (c d : F.Cocycle) : Prop :=
74   ∃ a : F.basedGauge U, F.gauge a.val c = d
75 
76 theorem gaugeEquivalent_refl (U : Set V) (c : F.Cocycle) : F.GaugeEquivalent U c c :=
77   ⟨1, F.gauge_one c⟩
78 
79 theorem gaugeEquivalent_symm {U : Set V} {c d : F.Cocycle}
80     (h : F.GaugeEquivalent U c d) : F.GaugeEquivalent U d c := by
81   obtain ⟨a, ha⟩ := h
82   refine ⟨a⁻¹, ?_⟩
83   change F.gauge a.val⁻¹ d = c
84   rw [← ha, F.gauge_inv_gauge]
85 
86 theorem gaugeEquivalent_trans {U : Set V} {c d e : F.Cocycle}
87     (h : F.GaugeEquivalent U c d) (k : F.GaugeEquivalent U d e) :
88     F.GaugeEquivalent U c e := by
89   obtain ⟨a, ha⟩ := h
90   obtain ⟨b, hb⟩ := k
91   refine ⟨b * a, ?_⟩
92   change F.gauge (b.val * a.val) c = e
93   rw [← F.gauge_mul, ha, hb]
94 
95 def gaugeSetoid (U : Set V) : Setoid F.Cocycle where
96   r := F.GaugeEquivalent U
97   iseqv := ⟨F.gaugeEquivalent_refl U, F.gaugeEquivalent_symm, F.gaugeEquivalent_trans⟩
98 
99 /-- A pointed orbit set; no group operation is asserted in the noncommutative case. -/
100 def Orbit (U : Set V) := Quotient (F.gaugeSetoid U)
101 
102 def orbitClass (U : Set V) (c : F.Cocycle) : F.Orbit U := Quotient.mk _ c
103 
104 def neutralClass (U : Set V) : F.Orbit U := F.orbitClass U F.trivial
105 
106 theorem orbitClass_eq_iff (U : Set V) (c d : F.Cocycle) :
107     F.orbitClass U c = F.orbitClass U d ↔ F.GaugeEquivalent U c d :=
108   Quotient.eq
109 
110 theorem morphism_nonempty_iff_class (U : Set V) (c d : F.GaugeObject U) :
111     Nonempty (c ⟶ d) ↔ F.orbitClass U c.labels = F.orbitClass U d.labels := by
112   rw [F.orbitClass_eq_iff]
113   constructor
114   · rintro ⟨a⟩; exact ⟨a.change, a.target⟩
115   · rintro ⟨a, ha⟩; exact ⟨⟨a, ha⟩⟩
116 
117 theorem iso_nonempty_iff_class (U : Set V) (c d : F.GaugeObject U) :
118     Nonempty (c ≅ d) ↔ F.orbitClass U c.labels = F.orbitClass U d.labels := by
119   rw [← F.morphism_nonempty_iff_class]
120   constructor
121   · rintro ⟨a⟩; exact ⟨a.hom⟩
122   · rintro ⟨a⟩; exact ⟨(Groupoid.isoEquivHom c d).symm a⟩
123 
124 /-- Automorphisms are the stabilizer, not an additional set of inequivalent objects. -/
125 def stabilizer (U : Set V) (c : F.Cocycle) : Subgroup (F.basedGauge U) where
126   carrier := {a | F.gauge a.val c = c}
127   one_mem' := F.gauge_one c
128   mul_mem' := by
129     intro a b ha hb
130     change F.gauge (a.val * b.val) c = c
131     rw [← F.gauge_mul, hb, ha]
132   inv_mem' := by
133     intro a ha
134     change F.gauge a.val⁻¹ c = c
135     calc
136       _ = F.gauge a.val⁻¹ (F.gauge a.val c) := by rw [ha]
137       _ = c := F.gauge_inv_gauge a.val c
138 
139 theorem stabilizer_characterization (U : Set V) (c : F.Cocycle) (a : F.basedGauge U) :
140     a ∈ F.stabilizer U c ↔
141       ∀ v w (f : v ⟶ w), a.val v = c.edge f * F.pull f (a.val w) * (c.edge f)⁻¹ := by
142   constructor
143   · intro h v w f
144     have he := congrArg (fun t : F.Cocycle => t.edge f) h
145     change a.val v * c.edge f * (F.pull f (a.val w))⁻¹ = c.edge f at he
146     calc
147       _ = (a.val v * c.edge f * (F.pull f (a.val w))⁻¹) *
148         F.pull f (a.val w) * (c.edge f)⁻¹ := by group
149       _ = _ := by rw [he]
150   · intro h
151     apply Cocycle.ext
152     intro v w f
153     change a.val v * c.edge f * (F.pull f (a.val w))⁻¹ = c.edge f
154     rw [h v w f]
155     group
156 
157 theorem trivial_stabilizer_iff (U : Set V) (a : F.basedGauge U) :
158     a ∈ F.stabilizer U F.trivial ↔
159       ∀ v w (f : v ⟶ w), F.pull f (a.val w) = a.val v := by
160   rw [F.stabilizer_characterization]
161   simp only [trivial, one_mul, inv_one, mul_one]
162   exact forall_congr' (fun _ => forall_congr' (fun _ => forall_congr' (fun _ => eq_comm)))
163 
164 /-- Fixing one arrow parametrizes every other arrow by a source automorphism. -/
165 def morphismParameters (U : Set V) {c d : F.GaugeObject U} (a : c ⟶ d) :
166     F.stabilizer U c.labels ≃ (c ⟶ d) where
167   toFun h := ⟨a.change * h.val, by
168     change F.gauge (a.change.val * h.val.val) c.labels = d.labels
169     rw [← F.gauge_mul, h.property, a.target]⟩
170   invFun b := ⟨a.change⁻¹ * b.change, by
171     change F.gauge (a.change.val⁻¹ * b.change.val) c.labels = c.labels
172     rw [← F.gauge_mul, b.target, ← a.target, F.gauge_inv_gauge]⟩
173   left_inv h := by apply Subtype.ext; change _⁻¹ * (_ * _) = _; group
174   right_inv b := by apply GaugeObject.Hom.ext; change _ * (_⁻¹ * _) = _; group
175 
176 theorem morphism_unique_iff_stabilizer (U : Set V) {c d : F.GaugeObject U} (a : c ⟶ d) :
177     Subsingleton (c ⟶ d) ↔ Subsingleton (F.stabilizer U c.labels) :=
178   (F.morphismParameters U a).subsingleton_congr.symm
179 
180 end GroupViewSystem
181 end KomorebiSpace

Back to source controls