CocycleExamples.lean

1 import KomorebiSpace.NonabelianExtensionFibers
2 import KomorebiSpace.ViewBoundaryExamples
3 import Mathlib.GroupTheory.Perm.Fin
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Loop cocycles: conjugacy classes versus automorphisms
9 
10 On the one-view category with C2 loops, constant group coefficients give
11 involutions up to conjugacy. The formal statements retain automorphisms
12 and distinguish cocycle existence from trivializability.
13 -/
14 universe u
15 namespace KomorebiSpace
16 open CategoryTheory GroupViewSystem
17 namespace CocycleExamples
18 open ViewBoundaryExamples (LoopView)
19 
20 variable (H : Type u) [Group H]
21 
22 def loopCoefficients : GroupViewSystem LoopView (fun _ => H) where
23   pull := fun _ => MonoidHom.id H
24   pull_id := by intros; rfl
25   pull_comp := by intros; rfl
26 
27 variable {H}
28 def involutionCocycle (p : H) (hp : p * p = 1) : (loopCoefficients H).Cocycle where
29   edge := fun f => if f then p else 1
30   edge_id := by intro v; rfl
31   edge_comp := by
32     intro v w z f g
33     change (if Bool.xor f g then p else 1) = (if f then p else 1) * (if g then p else 1)
34     cases f <;> cases g <;> simp [hp]
35 
36 /-- Every loop cocycle is determined by its nonidentity loop value. -/
37 theorem loop_value_square (c : (loopCoefficients H).Cocycle) :
38     c.edge (show LoopView.only ⟶ LoopView.only from true) *
39       c.edge (show LoopView.only ⟶ LoopView.only from true) = 1 := by
40   have he := c.edge_comp (show LoopView.only ⟶ LoopView.only from true)
41     (show LoopView.only ⟶ LoopView.only from true)
42   change c.edge (show LoopView.only ⟶ LoopView.only from false) =
43     c.edge (show LoopView.only ⟶ LoopView.only from true) *
44       c.edge (show LoopView.only ⟶ LoopView.only from true) at he
45   exact he.symm.trans (c.edge_id LoopView.only)
46 
47 theorem loop_cocycle_reconstruction (c : (loopCoefficients H).Cocycle) :
48     involutionCocycle (c.edge (show LoopView.only ⟶ LoopView.only from true))
49       (loop_value_square c) = c := by
50   apply GroupViewSystem.Cocycle.ext
51   intro v w f
52   cases v; cases w; cases f
53   · exact (c.edge_id LoopView.only).symm
54   · rfl
55 
56 def loopCocycleEquiv : (loopCoefficients H).Cocycle ≃ {p : H // p * p = 1} where
57   toFun c := ⟨c.edge (show LoopView.only ⟶ LoopView.only from true), loop_value_square c⟩
58   invFun p := involutionCocycle p.val p.property
59   left_inv := loop_cocycle_reconstruction
60   right_inv _ := rfl
61 
62 @[simp] theorem involution_edge (p : H) (hp : p * p = 1) :
63     (involutionCocycle p hp).edge (show LoopView.only ⟶ LoopView.only from true) = p := rfl
64 
65 /-- Orbit classes distinguish conjugacy, not equality of every local object. -/
66 theorem loop_class_eq_iff_conjugate (p q : H) (hp : p * p = 1) (hq : q * q = 1) :
67     (loopCoefficients H).orbitClass ∅ (involutionCocycle p hp) =
68       (loopCoefficients H).orbitClass ∅ (involutionCocycle q hq) ↔
69       ∃ a : H, a * p * a⁻¹ = q := by
70   rw [GroupViewSystem.orbitClass_eq_iff]
71   constructor
72   · rintro ⟨a, ha⟩
73     exact ⟨a.val LoopView.only,
74       congrArg (fun c => c.edge (show LoopView.only ⟶ LoopView.only from true)) ha⟩
75   · rintro ⟨a, ha⟩
76     refine ⟨⟨fun _ => a, by intro v; exact False.elim v.property⟩, ?_⟩
77     apply GroupViewSystem.Cocycle.ext
78     intro v w f
79     cases f
80     · change a * 1 * a⁻¹ = 1; group
81     · exact ha
82 
83 /-- Automorphisms at an involution are its centralizer. -/
84 theorem loop_stabilizer_iff (p : H) (hp : p * p = 1)
85     (a : (loopCoefficients H).basedGauge ∅) :
86     a ∈ (loopCoefficients H).stabilizer ∅ (involutionCocycle p hp) ↔
87       a.val LoopView.only * p = p * a.val LoopView.only := by
88   constructor
89   · intro h
90     have he := congrArg
91       (fun c : (loopCoefficients H).Cocycle =>
92         c.edge (show LoopView.only ⟶ LoopView.only from true)) h
93     change a.val LoopView.only * p * (a.val LoopView.only)⁻¹ = p at he
94     exact (mul_inv_eq_iff_eq_mul).mp he
95   · intro h
96     apply GroupViewSystem.Cocycle.ext
97     intro v w f
98     cases v; cases w; cases f
99     · change a.val LoopView.only * 1 * (a.val LoopView.only)⁻¹ = 1; group
100     · change a.val LoopView.only * p * (a.val LoopView.only)⁻¹ = p
101       exact (mul_inv_eq_iff_eq_mul).mpr h
102 
103 theorem involution_trivial_iff (p : H) (hp : p * p = 1) :
104     (loopCoefficients H).orbitClass ∅ (involutionCocycle p hp) =
105       (loopCoefficients H).neutralClass ∅ ↔ p = 1 := by
106   have ht : involutionCocycle (1 : H) (one_mul 1) = (loopCoefficients H).trivial := by
107     apply GroupViewSystem.Cocycle.ext
108     intro v w f
109     cases f <;> rfl
110   change (loopCoefficients H).orbitClass ∅ (involutionCocycle p hp) =
111     (loopCoefficients H).orbitClass ∅ (loopCoefficients H).trivial ↔ _
112   rw [← ht, loop_class_eq_iff_conjugate]
113   constructor
114   · rintro ⟨a, ha⟩
115     calc
116       p = a⁻¹ * (a * p * a⁻¹) * a := by group
117       _ = 1 := by rw [ha]; group
118   · intro hp1; exact ⟨1, by rw [hp1]; group⟩
119 
120 /-- A nontrivial loop cocycle is coherent transition data but has no global trivialization. -/
121 theorem involution_no_section (p : H) (hp : p * p = 1) (hne : p ≠ 1) :
122     ¬ Nonempty (((loopCoefficients H).twistedViews (involutionCocycle p hp)).Ambient) := by
123   rintro ⟨x⟩
124   have hx := x.property LoopView.only LoopView.only true
125   change p * x.val LoopView.only = x.val LoopView.only at hx
126   apply hne
127   exact mul_right_cancel (hx.trans (one_mul _).symm)
128 
129 abbrev S3 := Equiv.Perm (Fin 3)
130 def transposition : S3 := Equiv.swap 0 1
131 def otherTransposition : S3 := Equiv.swap 1 2
132 
133 theorem transposition_square : transposition * transposition = 1 := by decide
134 theorem otherTransposition_square : otherTransposition * otherTransposition = 1 := by decide
135 theorem transposition_nontrivial : transposition ≠ 1 := by decide
136 theorem transpositions_noncommute : transposition * otherTransposition ≠ otherTransposition * transposition := by decide
137 
138 def trivialObject : (loopCoefficients S3).GaugeObject ∅ := ⟨(loopCoefficients S3).trivial⟩
139 def nontrivialObject : (loopCoefficients S3).GaugeObject ∅ :=
140   ⟨involutionCocycle transposition transposition_square⟩
141 
142 def constantGauge (a : S3) : (loopCoefficients S3).basedGauge ∅ :=
143   ⟨fun _ => a, by intro v; exact False.elim v.property⟩
144 
145 /-- Every permutation fixes the trivial cocycle, giving a genuine automorphism arrow. -/
146 def trivialAutomorphism (a : S3) : trivialObject ⟶ trivialObject :=
147   ⟨constantGauge a, by
148     apply GroupViewSystem.Cocycle.ext
149     intro v w f
150     change a * 1 * a⁻¹ = 1
151     group⟩
152 
153 theorem trivialAutomorphism_injective : Function.Injective trivialAutomorphism := by
154   intro a b h
155   exact congrArg (fun f : trivialObject ⟶ trivialObject => f.change.val LoopView.only) h
156 
157 def trivialAutEquiv : S3 ≃ (trivialObject ⟶ trivialObject) where
158   toFun := trivialAutomorphism
159   invFun f := f.change.val LoopView.only
160   left_inv _ := rfl
161   right_inv f := by
162     apply GroupViewSystem.GaugeObject.Hom.ext
163     apply Subtype.ext
164     funext v
165     cases v
166     rfl
167 
168 /-- Automorphism composition is noncommutative in this actual cocycle groupoid. -/
169 theorem actual_automorphisms_noncommute :
170     trivialAutomorphism transposition ≫ trivialAutomorphism otherTransposition ≠
171       trivialAutomorphism otherTransposition ≫ trivialAutomorphism transposition := by
172   intro h
173   have he := congrArg (fun f : trivialObject ⟶ trivialObject => f.change.val LoopView.only) h
174   exact transpositions_noncommute he.symm
175 
176 theorem same_local_fibers_inequivalent : ¬ Nonempty (trivialObject ≅ nontrivialObject) := by
177   intro h
178   have he := ((loopCoefficients S3).iso_nonempty_iff_class ∅ trivialObject nontrivialObject).mp h
179   have hn : (loopCoefficients S3).orbitClass ∅ (involutionCocycle transposition transposition_square) =
180       (loopCoefficients S3).neutralClass ∅ := he.symm
181   exact transposition_nontrivial ((involution_trivial_iff transposition transposition_square).mp hn)
182 
183 theorem nontrivial_cocycle_not_trivializable :
184     ¬ Nonempty (((loopCoefficients S3).twistedViews nontrivialObject.labels).Ambient) :=
185   involution_no_section transposition transposition_square transposition_nontrivial
186 
187 /-- Framing the only view forbids every nonidentity gauge, without identifying its cocycles. -/
188 theorem full_framing_gauge_unique (a : (loopCoefficients S3).basedGauge Set.univ) : a = 1 := by
189   apply Subtype.ext
190   funext v
191   exact a.property ⟨v, Set.mem_univ v⟩
192 
193 /-- The finite classification is checked by kernel-reduced decidable enumeration. -/
194 theorem s3_involutions (p : S3) :
195     p * p = 1 ↔ p = 1 ∨ p = transposition ∨ p = otherTransposition ∨ p = Equiv.swap 0 2 := by
196   revert p
197   decide
198 
199 theorem s3_nonidentity_involutions_conjugate (p : S3) (hp : p * p = 1) (hne : p ≠ 1) :
200     ∃ a : S3, a * p * a⁻¹ = transposition := by
201   have h : ∀ p : S3, p * p = 1 → p ≠ 1 → ∃ a : S3, a * p * a⁻¹ = transposition := by decide
202   exact h p hp hne
203 
204 /-- Every object lies in one of exactly two isomorphism classes; the classes are distinct above. -/
205 theorem s3_orbit_dichotomy (c : (loopCoefficients S3).Cocycle) :
206     (loopCoefficients S3).orbitClass ∅ c = (loopCoefficients S3).neutralClass ∅ ∨
207       (loopCoefficients S3).orbitClass ∅ c =
208         (loopCoefficients S3).orbitClass ∅ nontrivialObject.labels := by
209   let p := c.edge (show LoopView.only ⟶ LoopView.only from true)
210   have hp : p * p = 1 := loop_value_square c
211   have he : involutionCocycle p hp = c := loop_cocycle_reconstruction c
212   by_cases h1 : p = 1
213   · left
214     rw [← he]
215     exact (involution_trivial_iff p hp).mpr h1
216   · right
217     rw [← he]
218     exact (loop_class_eq_iff_conjugate p transposition hp transposition_square).mpr
219       (s3_nonidentity_involutions_conjugate p hp h1)
220 
221 end CocycleExamples
222 end KomorebiSpace

Back to source controls