ScalarCocycle112.lean

1 import Mathlib.Algebra.Category.Grp.Injective
2 import Mathlib.Algebra.Group.TypeTags.Hom
3 import Mathlib.Analysis.Complex.Polynomial.Basic
4 import Mathlib.Tactic.Group
5 import Mathlib.Tactic.Ext
6 
7 /-! Scalar cocycle classification for complex projective comparison.
8 No identification of the full finite centers or dyadic group lift is assumed. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ScalarCocycle112
12 
13 variable {A C : Type*} [CommGroup A] [CommGroup C]
14 
15 /-- The normalized multiplicative cocycle convention used by Paper XI. -/
16 structure Cocycle (A C : Type*) [CommGroup A] [CommGroup C] where
17   coeff : A → A → C
18   assoc : ∀ a b d, coeff a b * coeff (a * b) d = coeff b d * coeff a (b * d)
19   one_left : ∀ a, coeff 1 a = 1
20   one_right : ∀ a, coeff a 1 = 1
21 
22 /-- Ratio of the coefficients in opposite orders. -/
23 def commutator (c : Cocycle A C) (a b : A) : C := c.coeff a b / c.coeff b a
24 
25 /-- A separate carrier prevents accidental use of the direct-product group law. -/
26 structure Extension (c : Cocycle A C) where
27   scalar : C
28   base : A
29 
30 namespace Extension
31 variable (c : Cocycle A C)
32 
33 @[ext] theorem ext {x y : Extension c} (h₁ : x.scalar = y.scalar) (h₂ : x.base = y.base) :
34     x = y := by cases x; cases y; cases h₁; cases h₂; rfl
35 
36 instance : Mul (Extension c) := ⟨fun x y =>
37   ⟨x.scalar * y.scalar * c.coeff x.base y.base, x.base * y.base⟩⟩
38 instance : One (Extension c) := ⟨⟨1, 1⟩⟩
39 instance : Inv (Extension c) := ⟨fun x =>
40   ⟨x.scalar⁻¹ / c.coeff x.base⁻¹ x.base, x.base⁻¹⟩⟩
41 
42 @[simp] theorem mul_scalar (x y : Extension c) :
43     (x * y).scalar = x.scalar * y.scalar * c.coeff x.base y.base := rfl
44 @[simp] theorem mul_base (x y : Extension c) : (x * y).base = x.base * y.base := rfl
45 @[simp] theorem one_scalar : (1 : Extension c).scalar = 1 := rfl
46 @[simp] theorem one_base : (1 : Extension c).base = 1 := rfl
47 
48 instance : Group (Extension c) where
49   mul_assoc x y z := by
50     apply ext
51     · change (x.scalar * y.scalar * c.coeff x.base y.base) * z.scalar *
52         c.coeff (x.base * y.base) z.base = x.scalar *
53         (y.scalar * z.scalar * c.coeff y.base z.base) * c.coeff x.base (y.base * z.base)
54       calc
55         _ = (x.scalar * y.scalar * z.scalar) *
56           (c.coeff x.base y.base * c.coeff (x.base * y.base) z.base) := by ac_rfl
57         _ = _ := by rw [c.assoc]; ac_rfl
58     · exact mul_assoc _ _ _
59   one_mul x := by ext <;> simp [c.one_left]
60   mul_one x := by ext <;> simp [c.one_right]
61   inv_mul_cancel x := by
62     apply ext
63     · change (x.scalar⁻¹ / c.coeff x.base⁻¹ x.base) * x.scalar *
64         c.coeff x.base⁻¹ x.base = 1
65       simp [div_eq_mul_inv, mul_comm]
66     · exact inv_mul_cancel _
67 
68 /-- The twisted extension is abelian exactly where symmetric coefficients are used. -/
69 @[instance_reducible] def commGroup (hsym : ∀ a b, c.coeff a b = c.coeff b a) : CommGroup (Extension c) :=
70   { (inferInstance : Group (Extension c)) with
71     mul_comm := fun x y => by
72       apply ext
73       · simp only [mul_scalar, hsym x.base y.base]
74         ac_rfl
75       · exact mul_comm _ _ }
76 
77 /-- Inclusion of the scalar subgroup. -/
78 def scalarInclusion : C →* Extension c where
79   toFun z := ⟨z, 1⟩
80   map_one' := rfl
81   map_mul' z w := by ext <;> simp [c.one_left]
82 
83 @[simp] theorem scalarInclusion_scalar (z : C) :
84     (scalarInclusion c z).scalar = z := rfl
85 @[simp] theorem scalarInclusion_base (z : C) :
86     (scalarInclusion c z).base = 1 := rfl
87 
88 theorem scalarInclusion_injective : Function.Injective (scalarInclusion c) :=
89   fun _ _ h => congrArg Extension.scalar h
90 
91 /-- The fixed normalized set-theoretic section. -/
92 def sectionOf (a : A) : Extension c := ⟨1, a⟩
93 
94 @[simp] theorem sectionOf_one : sectionOf c 1 = 1 := rfl
95 
96 theorem sectionOf_mul (a b : A) :
97     sectionOf c a * sectionOf c b = scalarInclusion c (c.coeff a b) * sectionOf c (a * b) := by
98   ext <;> simp [sectionOf, c.one_left]
99 
100 end Extension
101 
102 /-- Divisible scalar coefficients split every symmetric normalized cocycle.
103 The cochain is constructed from a retraction of the scalar subgroup. -/
104 theorem symmetric_exists_cochain [DivisibleBy (Additive C) ℤ]
105     (c : Cocycle A C) (hsym : ∀ a b, c.coeff a b = c.coeff b a) :
106     ∃ s : A → C, s 1 = 1 ∧ ∀ a b, c.coeff a b = s a * s b / s (a * b) := by
107   let : CommGroup (Extension c) := Extension.commGroup c hsym
108   obtain ⟨r, hr⟩ := (Module.Baer.of_divisible (Additive C)).extension_property_addMonoidHom
109     (Extension.scalarInclusion c).toAdditive
110     (fun x y h => Extension.scalarInclusion_injective c h)
111     (AddMonoidHom.id (Additive C))
112   let R : Extension c →* C := MonoidHom.toAdditive.symm r
113   have hR (z : C) : R (Extension.scalarInclusion c z) = z := by
114     exact DFunLike.congr_fun hr (Additive.ofMul z)
115   refine ⟨fun a => R (Extension.sectionOf c a), ?_, ?_⟩
116   · exact R.map_one
117   · intro a b
118     have hm := congrArg R (Extension.sectionOf_mul c a b)
119     rw [map_mul, map_mul, hR] at hm
120     exact (eq_div_iff_mul_eq').mpr hm.symm
121 
122 /-- The pointwise ratio of normalized cocycles. -/
123 def ratio (c d : Cocycle A C) : Cocycle A C where
124   coeff a b := c.coeff a b / d.coeff a b
125   assoc a b e := by
126     simp only [div_mul_div_comm, c.assoc, d.assoc]
127   one_left a := by simp [c.one_left, d.one_left]
128   one_right a := by simp [c.one_right, d.one_right]
129 
130 /-- Equality of scalar commutators makes the ratio cocycle symmetric. -/
131 theorem ratio_symmetric (c d : Cocycle A C)
132     (h : ∀ a b, commutator c a b = commutator d a b) :
133     ∀ a b, (ratio c d).coeff a b = (ratio c d).coeff b a := by
134   intro a b
135   apply (div_eq_div_iff_mul_eq_mul).mpr
136   have hab := (div_eq_div_iff_mul_eq_mul).mp (h a b)
137   simpa only [mul_comm] using hab
138 
139 /-- Equal commutators imply a normalized scalar change of basis over every
140 coefficient group whose additive type tag is divisible. -/
141 theorem same_commutator_exists_cochain_of_divisible [DivisibleBy (Additive C) ℤ]
142     (c d : Cocycle A C) (h : ∀ a b, commutator c a b = commutator d a b) :
143     ∃ s : A → C, s 1 = 1 ∧
144       ∀ a b, c.coeff a b = (s a * s b / s (a * b)) * d.coeff a b := by
145   obtain ⟨s, hs, he⟩ := symmetric_exists_cochain (ratio c d) (ratio_symmetric c d h)
146   refine ⟨s, hs, fun a b => ?_⟩
147   exact (div_eq_iff_eq_mul).mp (he a b)
148 
149 /-- Nonzero complex numbers have roots of every positive order. -/
150 theorem complex_units_exists_pow (z : ℂˣ) {n : ℕ} (hn : n ≠ 0) :
151     ∃ w : ℂˣ, w ^ n = z := by
152   obtain ⟨w, hw⟩ := IsAlgClosed.exists_pow_nat_eq (z : ℂ) (Nat.pos_of_ne_zero hn)
153   have hw0 : w ≠ 0 := by
154     intro h0
155     rw [h0, zero_pow hn] at hw
156     exact z.ne_zero hw.symm
157   refine ⟨Units.mk0 w hw0, ?_⟩
158   apply Units.ext
159   exact hw
160 
161 /-- Divisibility of complex scalar coefficients, proved from algebraic closure. -/
162 @[instance_reducible] def complexUnitsDivisible : DivisibleBy (Additive ℂˣ) ℤ := by
163   let : DivisibleBy (Additive ℂˣ) ℕ := divisibleByOfSMulRightSurj _ _ (by
164     intro n hn z
165     obtain ⟨w, hw⟩ := complex_units_exists_pow z hn
166     exact ⟨Additive.ofMul w, hw⟩)
167   exact AddGroup.divisibleByIntOfDivisibleByNat _
168 
169 /-- Complex normalized scalar cocycles with equal commutators are cohomologous.
170 The normalized cochain is a conclusion, not a supplied input. -/
171 theorem same_commutator_exists_cochain
172     (c d : Cocycle A ℂˣ) (h : ∀ a b, commutator c a b = commutator d a b) :
173     ∃ s : A → ℂˣ, s 1 = 1 ∧
174       ∀ a b, c.coeff a b = (s a * s b / s (a * b)) * d.coeff a b := by
175   let : DivisibleBy (Additive ℂˣ) ℤ := complexUnitsDivisible
176   exact same_commutator_exists_cochain_of_divisible c d h
177 
178 /-- Raw-function adapter for Paper XI's original `Cocycle` with normalization
179 stored separately: pass its coefficient and associativity fields and the two
180 normalization components. -/
181 theorem same_commutator_exists_cochain_raw
182     (c d : A → A → ℂˣ)
183     (hc : ∀ a b e, c a b * c (a * b) e = c b e * c a (b * e))
184     (hd : ∀ a b e, d a b * d (a * b) e = d b e * d a (b * e))
185     (hc₁ : ∀ a, c 1 a = 1) (hc₂ : ∀ a, c a 1 = 1)
186     (hd₁ : ∀ a, d 1 a = 1) (hd₂ : ∀ a, d a 1 = 1)
187     (h : ∀ a b, c a b / c b a = d a b / d b a) :
188     ∃ s : A → ℂˣ, s 1 = 1 ∧ ∀ a b, c a b = (s a * s b / s (a * b)) * d a b :=
189   same_commutator_exists_cochain ⟨c, hc, hc₁, hc₂⟩ ⟨d, hd, hd₁, hd₂⟩ h
190 
191 #print axioms symmetric_exists_cochain
192 #print axioms same_commutator_exists_cochain
193 #print axioms same_commutator_exists_cochain_raw
194 
195 end PaperXI.ScalarCocycle112

Back to source controls