ElementaryEnvelope.lean

1 import PaperXI.CocycleQuotient
2 import Mathlib.Algebra.Module.ZMod
3 import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
4 import Mathlib.LinearAlgebra.BilinearForm.Properties
5 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
6 
7 /-! Paper XI, 8.4 and the elementary-abelian portion of 9.4–9.5.
8 The complex cocycle is arbitrary. Only its commutator is forced to have
9 values in the group of pth roots of unity. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.ElementaryEnvelope
13 open CocycleCommutator
14 
15 variable {A : Type*} [CommGroup A] {p : ℕ}
16 
17 /-- Exponent p forces the actual scalar commutator, not the cocycle, into μp. -/
18 theorem commutator_pow (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1) (a b : A) :
19     commutator c a b ^ p = 1 := by
20   calc
21     _ = characterMap c (a ^ p) b := by rw [map_pow]; rfl
22     _ = 1 := by rw [hp, map_one]; rfl
23 
24 /-- The original elementary abelian group has its actual prime-field module structure. -/
25 abbrev groupModule (hp : ∀ a : A, a ^ p = 1) : Module (ZMod p) (Additive A) :=
26   AddCommGroup.zmodModule (fun a => congrArg Additive.ofMul (hp a.toMul))
27 
28 theorem finiteDimensional_group [Finite A] [Fact p.Prime]
29     (hp : ∀ a : A, a ^ p = 1) :
30     letI := groupModule hp
31     FiniteDimensional (ZMod p) (Additive A) := by
32   let := groupModule hp
33   exact Module.Finite.of_finite
34 
35 /-- The radical quotient, with additive notation. -/
36 def Space (c : Cocycle A ℂˣ) := Additive (A ⧸ radical c)
37   deriving AddCommGroup
38 
39 theorem quotient_pow (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1)
40     (z : A ⧸ radical c) : z ^ p = 1 := by
41   induction z using QuotientGroup.induction_on with | H a =>
42     change (QuotientGroup.mk' (radical c) a) ^ p = 1
43     rw [← map_pow, hp, map_one]
44 
45 instance spaceModule (c : Cocycle A ℂˣ) [Fact (∀ a : A, a ^ p = 1)] :
46     Module (ZMod p) (Space c) :=
47   AddCommGroup.zmodModule (fun z =>
48     congrArg Additive.ofMul (quotient_pow c Fact.out z.toMul))
49 
50 instance finiteSpace (c : Cocycle A ℂˣ) [Finite A] : Finite (Space c) :=
51   inferInstanceAs (Finite (Additive (A ⧸ radical c)))
52 
53 instance finiteDimensionalSpace (c : Cocycle A ℂˣ) [Finite A]
54     [Fact p.Prime] [Fact (∀ a : A, a ^ p = 1)] :
55     FiniteDimensional (ZMod p) (Space c) := Module.Finite.of_finite
56 
57 /-- The standard additive character, with its value bundled in μp. -/
58 def rootCharacter (p : ℕ) [NeZero p] : ZMod p →+ Additive (rootsOfUnity p ℂ) where
59   toFun t := Additive.ofMul (rootsOfUnityCircleEquiv p (ZMod.rootsOfUnityAddChar p t))
60   map_zero' := by
61     change rootsOfUnityCircleEquiv p (ZMod.rootsOfUnityAddChar p 0) = 1
62     rw [AddChar.map_zero_eq_one, map_one]
63   map_add' t u := by
64     change rootsOfUnityCircleEquiv p (ZMod.rootsOfUnityAddChar p (t + u)) = _
65     rw [AddChar.map_add_eq_mul, map_mul]
66     rfl
67 
68 /-- The standard character gives an actual additive equivalence Fp ≃ μp. -/
69 def rootEquiv (p : ℕ) [NeZero p] : ZMod p ≃+ Additive (rootsOfUnity p ℂ) :=
70   AddEquiv.ofBijective (rootCharacter p) ⟨by
71     intro t u h
72     have h' := (rootsOfUnityCircleEquiv p).injective h
73     exact (bijective_rootsOfUnityAddChar p).injective h',
74     surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar p⟩
75 
76 @[simp] theorem rootEquiv_coe (p : ℕ) [NeZero p] (t : ZMod p) :
77     (((rootEquiv p t).toMul : ℂˣ) : ℂ) = ZMod.stdAddChar t := rfl
78 
79 /-- The logarithm with respect to the chosen standard character. -/
80 def rootLog (p : ℕ) [NeZero p] : Additive (rootsOfUnity p ℂ) ≃+ ZMod p :=
81   (rootEquiv p).symm
82 
83 @[simp] theorem rootLog_character (p : ℕ) [NeZero p] (t : ZMod p) :
84     rootLog p (rootEquiv p t) = t := (rootEquiv p).symm_apply_apply t
85 
86 @[simp] theorem character_rootLog (p : ℕ) [NeZero p] (z : Additive (rootsOfUnity p ℂ)) :
87     rootEquiv p (rootLog p z) = z := (rootEquiv p).apply_symm_apply z
88 
89 /-- The descended scalar pairing has values in μp as well. -/
90 theorem quotientPairing_pow (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1)
91     (z w : A ⧸ radical c) : quotientPairing c z w ^ p = 1 := by
92   calc
93     _ = quotientPairing c (z ^ p) w := by rw [map_pow]; rfl
94     _ = 1 := by rw [quotient_pow c hp, map_one]; rfl
95 
96 /-- The root-valued pairing on the actual quotient. -/
97 def rootPairing (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1) :
98     (A ⧸ radical c) →* ((A ⧸ radical c) →* rootsOfUnity p ℂ) where
99   toFun z :=
100     { toFun := fun w => ⟨quotientPairing c z w, by
101         rw [mem_rootsOfUnity]; exact quotientPairing_pow c hp z w⟩
102       map_one' := Subtype.ext ((quotientPairing c z).map_one)
103       map_mul' := fun w v => Subtype.ext ((quotientPairing c z).map_mul w v) }
104   map_one' := by
105     apply MonoidHom.ext
106     intro w
107     apply Subtype.ext
108     exact congrArg (fun f : (A ⧸ radical c) →* ℂˣ => f w) (map_one (quotientPairing c))
109   map_mul' z w := by
110     apply MonoidHom.ext
111     intro v
112     apply Subtype.ext
113     exact congrArg (fun f : (A ⧸ radical c) →* ℂˣ => f v) (map_mul (quotientPairing c) z w)
114 
115 @[simp] theorem rootPairing_coe (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1)
116     (z w : A ⧸ radical c) : (rootPairing c hp z w : ℂˣ) = quotientPairing c z w := rfl
117 
118 /-- The original commutator as an actual μp-valued bicharacter. -/
119 def rootCommutator (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1) :
120     A →* (A →* rootsOfUnity p ℂ) where
121   toFun a := (rootPairing c hp (QuotientGroup.mk a)).comp (QuotientGroup.mk' (radical c))
122   map_one' := by
123     apply MonoidHom.ext
124     intro a
125     apply Subtype.ext
126     exact commutator_one_left c a
127   map_mul' a b := by
128     apply MonoidHom.ext
129     intro d
130     apply Subtype.ext
131     exact commutator_mul_left c a b d
132 
133 @[simp] theorem rootCommutator_coe (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1)
134     (a b : A) : (rootCommutator c hp a b : ℂˣ) = commutator c a b := rfl
135 
136 theorem rootCommutator_self (c : Cocycle A ℂˣ) (hp : ∀ a : A, a ^ p = 1) (a : A) :
137     rootCommutator c hp a a = 1 := Subtype.ext (commutator_self c a)
138 
139 end PaperXI.ElementaryEnvelope

Back to source controls