CyclicDefect113.lean

1 import PaperXI.ScalarCocycle112
2 import Mathlib.Data.Int.GCD
3 import Mathlib.Algebra.Group.Hom.Instances
4 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
5 
6 /-! Explicit coprime correction of the character defect left by scalar
7 cocycle comparison. Arithmetic realization is not asserted here. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CyclicDefect113
11 open Finset
12 open ScalarCocycle112
13 
14 variable {A C : Type*} [CommGroup A] [CommGroup C]
15 
16 /-- Norm of an arbitrary scalar function along a finite cyclic orbit. -/
17 def orbitNorm (β : A ≃* A) (f : A → C) (n : ℕ) (a : A) : C :=
18   ∏ i ∈ range n, f ((β ^ i) a)
19 
20 /-- Weighted norm, formed in the character group. -/
21 def weightedCharacter (β : A ≃* A) (r : A →* C) (n : ℕ) : A →* C :=
22   ∏ i ∈ range n, (r.comp (β ^ i).toMonoidHom) ^ i
23 
24 @[simp] theorem orbitNorm_zero (β : A ≃* A) (f : A → C) (a : A) :
25     orbitNorm β f 0 a = 1 := by simp [orbitNorm]
26 
27 theorem orbitNorm_succ (β : A ≃* A) (f : A → C) (n : ℕ) (a : A) :
28     orbitNorm β f (n+1) a = orbitNorm β f n a * f ((β ^ n) a) := by
29   simp [orbitNorm, prod_range_succ]
30 
31 @[simp] theorem weightedCharacter_zero (β : A ≃* A) (r : A →* C) (a : A) :
32     weightedCharacter β r 0 a = 1 := by simp [weightedCharacter]
33 
34 theorem weightedCharacter_succ (β : A ≃* A) (r : A →* C) (n : ℕ) (a : A) :
35     weightedCharacter β r (n+1) a =
36       weightedCharacter β r n a * r ((β ^ n) a) ^ n := by
37   simp [weightedCharacter, prod_range_succ]
38 
39 theorem power_apply_shift (β : A ≃* A) (n : ℕ) (a : A) :
40     (β ^ n) (β a) = (β ^ (n+1)) a := by
41   rw [pow_succ]
42   rfl
43 
44 /-- The weighted norm is an explicit contracting operator for cyclic defects. -/
45 theorem weightedCharacter_shift (β : A ≃* A) (r : A →* C) (n : ℕ) (a : A) :
46     weightedCharacter β r n (β a) * orbitNorm β r n (β a) =
47       weightedCharacter β r n a * r ((β ^ n) a) ^ n := by
48   induction n with
49   | zero => simp
50   | succ n ih =>
51     rw [weightedCharacter_succ, orbitNorm_succ, weightedCharacter_succ,
52       power_apply_shift]
53     calc
54       _ = (weightedCharacter β r n (β a) * orbitNorm β r n (β a)) *
55           r ((β ^ (n+1)) a) ^ (n+1) := by rw [pow_succ (r ((β ^ (n+1)) a))]; ac_rfl
56       _ = _ := by rw [ih]
57 
58 /-- A Bezout power inverts n-th powers on the m-torsion subgroup. -/
59 theorem bezout_power {n m : ℕ} (hcop : n.Coprime m) (z : C) (hm : z ^ m = 1) :
60     (z ^ n) ^ (Nat.gcdA n m) = z := by
61   have hbez : (1 : ℤ) = n * Nat.gcdA n m + m * Nat.gcdB n m := by
62     simpa only [hcop.gcd_eq_one, Int.natCast_one] using Nat.gcd_eq_gcd_ab n m
63   calc
64     (z ^ n) ^ (Nat.gcdA n m) = z ^ (n * Nat.gcdA n m) := by
65       rw [← zpow_natCast, ← zpow_mul]
66     _ = z ^ (n * Nat.gcdA n m) * z ^ (m * Nat.gcdB n m) := by
67       rw [zpow_mul z (m : ℤ), zpow_natCast, hm, one_zpow, mul_one]
68     _ = z := by rw [← zpow_add, ← hbez, zpow_one]
69 
70 /-- The correcting character is explicit, using a weighted norm and Bezout. -/
71 def correctingCharacter (β : A ≃* A) (r : A →* C) (n m : ℕ) : A →* C :=
72   weightedCharacter β r n ^ (Nat.gcdA n m)
73 
74 /-- Every norm-one character defect for a coprime cyclic action is a
75 coboundary. No correcting character is assumed. -/
76 theorem correctingCharacter_coboundary (β : A ≃* A) (r : A →* C)
77     (n m : ℕ) (hβ : β ^ n = 1) (hm : ∀ a : A, a ^ m = 1)
78     (hcop : n.Coprime m) (hnorm : ∀ a, orbitNorm β r n a = 1) (a : A) :
79     correctingCharacter β r n m (β a) / correctingCharacter β r n m a = r a := by
80   have ht := weightedCharacter_shift β r n a
81   rw [hnorm, mul_one, hβ] at ht
82   change weightedCharacter β r n (β a) = weightedCharacter β r n a * r a ^ n at ht
83   have hr : r a ^ m = 1 := by rw [← map_pow, hm, map_one]
84   change weightedCharacter β r n (β a) ^ (Nat.gcdA n m) /
85     weightedCharacter β r n a ^ (Nat.gcdA n m) = _
86   rw [ht, mul_zpow, mul_div_cancel_left]
87   exact bezout_power hcop (r a) hr
88 
89 
90 /-- An actual automorphism of a scalar extension, fixing the scalars and
91 covering the specified quotient automorphism. Its phase is not supplied. -/
92 structure ScalarLift (c : Cocycle A C) (β : A ≃* A) where
93   action : Extension c ≃* Extension c
94   on_base : ∀ x, (action x).base = β x.base
95   fixes_scalar : ∀ z, action (Extension.scalarInclusion c z) =
96     Extension.scalarInclusion c z
97 
98 namespace ScalarLift
99 variable {c : Cocycle A C} {β : A ≃* A} (L : ScalarLift c β)
100 
101 /-- The phase of the given lift on the fixed section. -/
102 def phase (a : A) : C := (L.action (Extension.sectionOf c a)).scalar
103 
104 @[simp] theorem phase_one : L.phase 1 = 1 := by
105   simp [phase]
106 
107 /-- The lift on every element is determined by its derived section phase. -/
108 theorem scalar_formula (x : Extension c) :
109     (L.action x).scalar = x.scalar * L.phase x.base := by
110   have hx : x = Extension.scalarInclusion c x.scalar * Extension.sectionOf c x.base := by
111     apply Extension.ext <;> simp [Extension.sectionOf, c.one_left]
112   calc
113     (L.action x).scalar =
114         (L.action (Extension.scalarInclusion c x.scalar * Extension.sectionOf c x.base)).scalar :=
115       congrArg (fun y => (L.action y).scalar) hx
116     _ = _ := by
117       rw [map_mul, L.fixes_scalar]
118       simp [phase, c.one_left]
119 
120 /-- The phase law follows from the actual lifted group automorphism. -/
121 theorem phase_mul (a b : A) :
122     L.phase (a*b) = L.phase a * L.phase b * c.coeff (β a) (β b) / c.coeff a b := by
123   have h := congrArg Extension.scalar
124     (L.action.map_mul (Extension.sectionOf c a) (Extension.sectionOf c b))
125   rw [L.scalar_formula] at h
126   simp only [Extension.mul_scalar, Extension.mul_base, Extension.sectionOf,
127     one_mul, phase, L.on_base] at h
128   apply (eq_div_iff_mul_eq').mpr
129   simpa only [phase, Extension.sectionOf, mul_comm] using h
130 
131 theorem power_base (n : ℕ) (x : Extension c) :
132     ((L.action ^ n) x).base = (β ^ n) x.base := by
133   induction n with
134   | zero => rfl
135   | succ n ih =>
136     rw [pow_succ', pow_succ']
137     change (L.action ((L.action ^ n) x)).base = β ((β ^ n) x.base)
138     rw [L.on_base, ih]
139 
140 /-- Iteration of the full lift derives the norm of its section phases. -/
141 theorem power_scalar (n : ℕ) (x : Extension c) :
142     ((L.action ^ n) x).scalar = x.scalar * orbitNorm β L.phase n x.base := by
143   induction n with
144   | zero => simp
145   | succ n ih =>
146     rw [pow_succ']
147     change (L.action ((L.action ^ n) x)).scalar = _
148     rw [L.scalar_formula, L.power_base, ih, orbitNorm_succ]
149     exact mul_assoc _ _ _
150 
151 /-- Honest finite order of the actual lift implies its phase norm is one. -/
152 theorem norm_eq_one (n : ℕ) (hn : L.action ^ n = 1) (a : A) :
153     orbitNorm β L.phase n a = 1 := by
154   have h := L.power_scalar n (Extension.sectionOf c a)
155   rw [hn] at h
156   simpa [Extension.sectionOf] using h.symm
157 
158 end ScalarLift
159 
160 
161 /-- A function's coboundary has telescoping cyclic norm. -/
162 theorem orbitNorm_coboundary (β : A ≃* A) (s : A → C) (n : ℕ) (a : A) :
163     orbitNorm β (fun b => s (β b) / s b) n a = s ((β ^ n) a) / s a := by
164   induction n with
165   | zero => simp
166   | succ n ih =>
167     rw [orbitNorm_succ, ih]
168     have hβ : β ((β ^ n) a) = (β ^ (n+1)) a := by rw [pow_succ']; rfl
169     rw [hβ]
170     simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
171 
172 theorem orbitNorm_mul (β : A ≃* A) (f g : A → C) (n : ℕ) (a : A) :
173     orbitNorm β (fun b => f b * g b) n a = orbitNorm β f n a * orbitNorm β g n a := by
174   simp [orbitNorm, prod_mul_distrib]
175 
176 theorem orbitNorm_div (β : A ≃* A) (f g : A → C) (n : ℕ) (a : A) :
177     orbitNorm β (fun b => f b / g b) n a = orbitNorm β f n a / orbitNorm β g n a := by
178   simp [orbitNorm, prod_div_distrib]
179 
180 section Defect
181 variable (c d : Cocycle A C) (β : A ≃* A)
182   (L : ScalarLift c β) (M : ScalarLift d β) (s : A → C)
183   (hs1 : s 1 = 1)
184   (hs : ∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b)
185 
186 /-- The label-dependent defect of the supplied honest lifted actions. -/
187 def actionDefect (a : A) : C := L.phase a * s (β a) / (s a * M.phase a)
188 
189 include hs1 in
190 theorem actionDefect_one : actionDefect c d β L M s 1 = 1 := by
191   simp [actionDefect, hs1]
192 
193 include hs in
194 /-- Multiplicativity of the defect is derived, rather than postulated. -/
195 theorem actionDefect_mul (a b : A) :
196     actionDefect c d β L M s (a*b) =
197       actionDefect c d β L M s a * actionDefect c d β L M s b := by
198   simp only [actionDefect, L.phase_mul, M.phase_mul, map_mul]
199   rw [hs a b, hs (β a) (β b)]
200   simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
201   rw [mul_left_comm (s (a*b)) ((s a)⁻¹), mul_left_comm (s (a*b)) ((s b)⁻¹),
202     mul_inv_cancel_left]
203 
204 /-- The discrepancy of the actual lifts is an actual character. -/
205 def defectCharacter : A →* C where
206   toFun := actionDefect c d β L M s
207   map_one' := actionDefect_one c d β L M s hs1
208   map_mul' := actionDefect_mul c d β L M s hs
209 
210 /-- Norm one follows from the full cyclic action laws and telescoping. -/
211 theorem actionDefect_norm (n : ℕ) (hβ : β ^ n = 1)
212     (hL : L.action ^ n = 1) (hM : M.action ^ n = 1) (a : A) :
213     orbitNorm β (actionDefect c d β L M s) n a = 1 := by
214   have hfun : actionDefect c d β L M s =
215       fun b => (L.phase b / M.phase b) * (s (β b) / s b) := by
216     funext b
217     simp [actionDefect, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
218   rw [hfun, orbitNorm_mul, orbitNorm_div, orbitNorm_coboundary,
219     L.norm_eq_one n hL, M.norm_eq_one n hM, hβ]
220   simp
221 
222 /-- The cochain corrected by the explicitly constructed defect character. -/
223 def correctedCochain (n m : ℕ) (a : A) : C :=
224   s a / correctingCharacter β (defectCharacter c d β L M s hs1 hs) n m a
225 
226 include hs1 in
227 theorem correctedCochain_one (n m : ℕ) :
228     correctedCochain c d β L M s hs1 hs n m 1 = 1 := by
229   simp [correctedCochain, hs1]
230 
231 /-- Character correction preserves the original cocycle comparison. -/
232 theorem correctedCochain_cocycle (n m : ℕ) (a b : A) :
233     c.coeff a b =
234       (correctedCochain c d β L M s hs1 hs n m a *
235         correctedCochain c d β L M s hs1 hs n m b /
236           correctedCochain c d β L M s hs1 hs n m (a*b)) * d.coeff a b := by
237   rw [hs a b]
238   simp only [correctedCochain, map_mul]
239   simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
240 
241 /-- Covariance is a conclusion obtained by solving the derived character
242 cocycle. It is not a premise on the original scalar cochain. -/
243 theorem correctedCochain_covariant (n m : ℕ) (hβ : β ^ n = 1)
244     (hL : L.action ^ n = 1) (hM : M.action ^ n = 1)
245     (hm : ∀ a : A, a ^ m = 1) (hcop : n.Coprime m) (a : A) :
246     L.phase a * correctedCochain c d β L M s hs1 hs n m (β a) =
247       correctedCochain c d β L M s hs1 hs n m a * M.phase a := by
248   let r := defectCharacter c d β L M s hs1 hs
249   have hn : ∀ b, orbitNorm β r n b = 1 := actionDefect_norm c d β L M s n hβ hL hM
250   have hc := correctingCharacter_coboundary β r n m hβ hm hcop hn a
251   have hx : correctingCharacter β r n m (β a) =
252       (L.phase a * s (β a) / (s a * M.phase a)) * correctingCharacter β r n m a := by
253     exact (div_eq_iff_eq_mul).mp hc
254   change L.phase a * (s (β a) / correctingCharacter β r n m (β a)) =
255     (s a / correctingCharacter β r n m a) * M.phase a
256   rw [hx]
257   simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
258 
259 end Defect
260 
261 
262 /-- The normalized cochain gives an isomorphism of the scalar pushout
263 extensions. This does not identify the original finite central groups. -/
264 def scalarBridge (c d : Cocycle A C) (s : A → C)
265     (hs : ∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b) :
266     Extension c ≃* Extension d where
267   toFun x := ⟨x.scalar * s x.base, x.base⟩
268   invFun y := ⟨y.scalar / s y.base, y.base⟩
269   left_inv x := by apply Extension.ext <;> simp
270   right_inv y := by apply Extension.ext <;> simp
271   map_mul' x y := by
272     apply Extension.ext
273     · change (x.scalar * y.scalar * c.coeff x.base y.base) * s (x.base * y.base) =
274         (x.scalar * s x.base) * (y.scalar * s y.base) * d.coeff x.base y.base
275       rw [hs]
276       simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
277     · rfl
278 
279 @[simp] theorem scalarBridge_base (c d : Cocycle A C) (s : A → C)
280     (hs : ∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b)
281     (x : Extension c) : (scalarBridge c d s hs x).base = x.base := rfl
282 
283 /-- A normalized bridge retains each scalar exactly. -/
284 theorem scalarBridge_fixes_scalar (c d : Cocycle A C) (s : A → C) (hs1 : s 1 = 1)
285     (hs : ∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b) (z : C) :
286     scalarBridge c d s hs (Extension.scalarInclusion c z) = Extension.scalarInclusion d z := by
287   apply Extension.ext <;> simp [scalarBridge, hs1]
288 
289 /-- Derived cochain covariance is exactly full lifted equivariance. -/
290 theorem scalarBridge_equivariant (c d : Cocycle A C) (β : A ≃* A)
291     (L : ScalarLift c β) (M : ScalarLift d β) (s : A → C)
292     (hs : ∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b)
293     (hcov : ∀ a, L.phase a * s (β a) = s a * M.phase a) (x : Extension c) :
294     scalarBridge c d s hs (L.action x) = M.action (scalarBridge c d s hs x) := by
295   apply Extension.ext
296   · change (L.action x).scalar * s (L.action x).base =
297       (M.action (scalarBridge c d s hs x)).scalar
298     rw [L.scalar_formula, L.on_base, M.scalar_formula]
299     change (x.scalar * L.phase x.base) * s (β x.base) =
300       (x.scalar * s x.base) * M.phase x.base
301     rw [mul_assoc, hcov, mul_assoc]
302   · change (L.action x).base = (M.action (scalarBridge c d s hs x)).base
303     rw [L.on_base, M.on_base, scalarBridge_base]
304 
305 /-- Equal commutators and honest coprime cyclic lifts construct a normalized
306 equivariant cochain. Neither an initial cochain nor a covariance correction is
307 assumed. This is a theorem about complex scalar pushout extensions. -/
308 theorem exists_equivariant_cochain
309     (c d : Cocycle A ℂˣ) (β : A ≃* A)
310     (L : ScalarLift c β) (M : ScalarLift d β)
311     (n m : ℕ) (hβ : β ^ n = 1) (hL : L.action ^ n = 1) (hM : M.action ^ n = 1)
312     (hm : ∀ a : A, a ^ m = 1) (hcop : n.Coprime m)
313     (hcomm : ∀ a b, commutator c a b = commutator d a b) :
314     ∃ s : A → ℂˣ, s 1 = 1 ∧
315       (∀ a b, c.coeff a b = (s a * s b / s (a*b)) * d.coeff a b) ∧
316       (∀ a, L.phase a * s (β a) = s a * M.phase a) := by
317   obtain ⟨s, hs1, hs⟩ := same_commutator_exists_cochain c d hcomm
318   refine ⟨correctedCochain c d β L M s hs1 hs n m,
319     correctedCochain_one c d β L M s hs1 hs n m,
320     correctedCochain_cocycle c d β L M s hs1 hs n m, ?_⟩
321   exact correctedCochain_covariant c d β L M s hs1 hs n m hβ hL hM hm hcop
322 
323 /-- An equivariant scalar bridge exists, fixing every original scalar and
324 quotient label and commuting with the two supplied full lifted actions. -/
325 theorem exists_equivariant_scalarBridge
326     (c d : Cocycle A ℂˣ) (β : A ≃* A)
327     (L : ScalarLift c β) (M : ScalarLift d β)
328     (n m : ℕ) (hβ : β ^ n = 1) (hL : L.action ^ n = 1) (hM : M.action ^ n = 1)
329     (hm : ∀ a : A, a ^ m = 1) (hcop : n.Coprime m)
330     (hcomm : ∀ a b, commutator c a b = commutator d a b) :
331     ∃ F : Extension c ≃* Extension d,
332       (∀ z, F (Extension.scalarInclusion c z) = Extension.scalarInclusion d z) ∧
333       (∀ x, (F x).base = x.base) ∧
334       (∀ x, F (L.action x) = M.action (F x)) := by
335   obtain ⟨s, hs1, hs, hcov⟩ := exists_equivariant_cochain c d β L M n m hβ hL hM hm hcop hcomm
336   exact ⟨scalarBridge c d s hs, scalarBridge_fixes_scalar c d s hs1 hs,
337     scalarBridge_base c d s hs, scalarBridge_equivariant c d β L M s hs hcov⟩
338 
339 end PaperXI.CyclicDefect113

Back to source controls