ElementaryEnvelopeForm.lean

1 import PaperXI.ElementaryEnvelope
2 
3 /-! The actual alternating prime-field form on the commutator radical quotient.
4 The logarithm equivalence is explicit: the standard character supplies one,
5 and all alternative choices have a proved scalar comparison. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ElementaryEnvelope
9 open CocycleCommutator
10 
11 variable {A : Type*} [CommGroup A] {p : ℕ} [Fact p.Prime]
12 variable (c : Cocycle A ℂˣ) [Fact (∀ a : A, a ^ p = 1)]
13 
14 /-- Apply the actual root logarithm in both additive quotient variables. -/
15 def logarithmicPairing (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
16     Space c →+ (Space c →+ ZMod p) where
17   toFun x := e.symm.toAddMonoidHom.comp (rootPairing c Fact.out x.toMul).toAdditive
18   map_zero' := by
19     apply AddMonoidHom.ext
20     intro y
21     change e.symm (Additive.ofMul (rootPairing c Fact.out 1 y.toMul)) = 0
22     have h : rootPairing c Fact.out 1 y.toMul = 1 :=
23       congrArg (fun f : (A ⧸ radical c) →* rootsOfUnity p ℂ => f y.toMul)
24         (map_one (rootPairing c Fact.out))
25     rw [h]
26     exact map_zero e.symm
27   map_add' x y := by
28     apply AddMonoidHom.ext
29     intro z
30     change e.symm (Additive.ofMul (rootPairing c Fact.out (x.toMul * y.toMul) z.toMul)) = _
31     have h := congrArg (fun f : (A ⧸ radical c) →* rootsOfUnity p ℂ => f z.toMul)
32       (map_mul (rootPairing c Fact.out) x.toMul y.toMul)
33     rw [h]
34     exact map_add e.symm _ _
35 
36 /-- Any chosen identification Fp ≃ μp gives a bilinear form, by construction. -/
37 def formWith (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
38     LinearMap.BilinForm (ZMod p) (Space c) :=
39   ((AddMonoidHom.toZModLinearMapEquiv p).toAddMonoidHom.comp
40     (logarithmicPairing c e)).toZModLinearMap p
41 
42 @[simp] theorem formWith_apply (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ))
43     (x y : Space c) : formWith c e x y =
44       e.symm (Additive.ofMul (rootPairing c Fact.out x.toMul y.toMul)) := rfl
45 
46 /-- Exponentiating the form recovers the original quotient commutator. -/
47 theorem formWith_character (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ))
48     (x y : Space c) :
49     ((e (formWith c e x y)).toMul : ℂˣ) = quotientPairing c x.toMul y.toMul := by
50   rw [formWith_apply, e.apply_symm_apply]
51   rfl
52 
53 /-- Both scalar laws are those of the actual constructed bilinear map. -/
54 theorem formWith_smul_left (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ))
55     (r : ZMod p) (x y : Space c) :
56     formWith c e (r • x) y = r * formWith c e x y := by
57   exact LinearMap.BilinForm.smul_left _ _ _
58 
59 theorem formWith_smul_right (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ))
60     (r : ZMod p) (x y : Space c) :
61     formWith c e x (r • y) = r * formWith c e x y := by
62   exact LinearMap.BilinForm.smul_right _ _ _
63 
64 theorem formWith_isAlt (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
65     (formWith c e).IsAlt := by
66   intro x
67   rw [formWith_apply]
68   have h : rootPairing (p := p) c Fact.out x.toMul x.toMul = 1 :=
69     Subtype.ext (quotientPairing_self c x.toMul)
70   rw [h]
71   exact map_zero e.symm
72 
73 theorem formWith_eq_zero_iff (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ))
74     (x y : Space c) :
75     formWith c e x y = 0 ↔ quotientPairing c x.toMul y.toMul = 1 := by
76   rw [formWith_apply, e.symm.map_eq_zero_iff]
77   change rootPairing c Fact.out x.toMul y.toMul = 1 ↔ _
78   exact Subtype.ext_iff
79 
80 theorem formWith_nondegenerate (e : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
81     (formWith c e).Nondegenerate := by
82   constructor
83   · intro x hx
84     have h : x.toMul = 1 := (quotientPairing_nondegenerate_left c x.toMul).mp
85       (fun y => (formWith_eq_zero_iff c e x (Additive.ofMul y)).mp (hx (Additive.ofMul y)))
86     exact congrArg Additive.ofMul h
87   · intro y hy
88     have h : y.toMul = 1 := (quotientPairing_nondegenerate_right c y.toMul).mp
89       (fun x => (formWith_eq_zero_iff c e (Additive.ofMul x) y).mp (hy (Additive.ofMul x)))
90     exact congrArg Additive.ofMul h
91 
92 /-- The form for the fixed standard additive character. -/
93 def form : LinearMap.BilinForm (ZMod p) (Space c) := formWith c (rootEquiv p)
94 
95 theorem form_isAlt : (form (p := p) c).IsAlt := formWith_isAlt c (rootEquiv p)
96 
97 theorem form_nondegenerate : (form (p := p) c).Nondegenerate :=
98   formWith_nondegenerate c (rootEquiv p)
99 
100 /-- The standard character/logarithm roundtrip lands in the literal scalar pairing. -/
101 theorem form_stdAddChar (x y : Space c) :
102     ZMod.stdAddChar (form (p := p) c x y) =
103       (quotientPairing c x.toMul y.toMul : ℂ) := by
104   rw [← rootEquiv_coe]
105   exact congrArg Units.val (formWith_character c (rootEquiv p) x y)
106 
107 /-- Changing the identification of μp changes the field coordinate by this
108 nonzero scalar, rather than giving an identical form. -/
109 theorem choice_scalar_ne_zero
110     (e e' : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
111     (e.trans e'.symm) 1 ≠ 0 := by
112   intro h
113   exact one_ne_zero ((e.trans e'.symm).injective (h.trans (map_zero _).symm))
114 
115 theorem choice_map_eq_mul
116     (e e' : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) (t : ZMod p) :
117     (e.trans e'.symm) t = (e.trans e'.symm) 1 * t := by
118   let L := (e.trans e'.symm).toAddMonoidHom.toZModLinearMap p
119   have h := L.map_smul t (1 : ZMod p)
120   change (e.trans e'.symm) (t * 1) = t * (e.trans e'.symm) 1 at h
121   simpa only [mul_one, mul_comm] using h
122 
123 /-- Exact choice comparison, with scalar determined by the two characters. -/
124 theorem formWith_choice
125     (e e' : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) (x y : Space c) :
126     formWith c e' x y = (e.trans e'.symm) 1 * formWith c e x y := by
127   rw [← choice_map_eq_mul e e']
128   simp only [formWith_apply, AddEquiv.trans_apply, e.apply_symm_apply]
129 
130 /-- Any two primitive character choices produce a nonzero scalar multiple. -/
131 theorem exists_choice_scalar
132     (e e' : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) :
133     ∃ u : (ZMod p)ˣ, ∀ x y : Space c,
134       formWith c e' x y = (u : ZMod p) * formWith c e x y := by
135   exact ⟨Units.mk0 _ (choice_scalar_ne_zero e e'), formWith_choice c e e'⟩
136 
137 end PaperXI.ElementaryEnvelope

Back to source controls