ElementaryEnvelopeTransport.lean

1 import PaperXI.ElementaryEnvelopeForm
2 
3 /-! Functoriality of the actual elementary commutator envelope.
4 All maps here descend the given group maps, and preserve the form for one
5 common chosen root coordinate. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.ElementaryEnvelope
9 open CocycleCommutator
10 
11 variable {A B D : Type*} [CommGroup A] [CommGroup B] [CommGroup D]
12 variable (c : Cocycle A ℂˣ) (d : Cocycle B ℂˣ)
13 
14 /-- Pairing-preserving group equivalences carry the actual radical onto the radical. -/
15 theorem radical_map (e : A ≃* B)
16     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) :
17     (radical c).map e.toMonoidHom = radical d := by
18   ext b
19   constructor
20   · rintro ⟨a, ha, rfl⟩
21     change a ∈ radical c at ha
22     rw [mem_radical_iff] at ha ⊢
23     intro t
24     obtain ⟨u, rfl⟩ := e.surjective t
25     exact (he a u).trans (ha u)
26   · intro hb
27     refine ⟨e.symm b, ?_, e.apply_symm_apply b⟩
28     change e.symm b ∈ radical c
29     rw [mem_radical_iff] at hb ⊢
30     intro a
31     rw [← he, e.apply_symm_apply, hb]
32 
33 /-- The actual map on the radical quotient. -/
34 def quotientEquiv (e : A ≃* B)
35     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) :
36     (A ⧸ radical c) ≃* (B ⧸ radical d) :=
37   QuotientGroup.congr (radical c) (radical d) e (radical_map c d e he)
38 
39 @[simp] theorem quotientEquiv_mk (e : A ≃* B)
40     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) (a : A) :
41     quotientEquiv c d e he (QuotientGroup.mk a) = QuotientGroup.mk (e a) := rfl
42 
43 theorem quotientEquiv_pairing (e : A ≃* B)
44     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b)
45     (x y : A ⧸ radical c) :
46     quotientPairing d (quotientEquiv c d e he x) (quotientEquiv c d e he y) =
47       quotientPairing c x y := by
48   induction x using QuotientGroup.induction_on with | H a =>
49     induction y using QuotientGroup.induction_on with | H b =>
50       exact he a b
51 
52 variable {p : ℕ} [Fact p.Prime]
53 variable [Fact (∀ a : A, a ^ p = 1)] [Fact (∀ b : B, b ^ p = 1)]
54 
55 /-- The quotient map is a linear equivalence over the actual prime field. -/
56 def linearEquiv (e : A ≃* B)
57     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) :
58     Space c ≃ₗ[ZMod p] Space d :=
59   let f : Space c ≃+ Space d := (quotientEquiv c d e he).toAdditive
60   { f with map_smul' := ZMod.map_smul f }
61 
62 @[simp] theorem linearEquiv_mk (e : A ≃* B)
63     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) (a : A) :
64     linearEquiv (p := p) c d e he (Additive.ofMul (QuotientGroup.mk a)) =
65       Additive.ofMul (QuotientGroup.mk (e a)) := rfl
66 
67 /-- Common root coordinates give an actual isometry, without a scalar ambiguity. -/
68 theorem linearEquiv_formWith (e : A ≃* B)
69     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b)
70     (r : ZMod p ≃+ Additive (rootsOfUnity p ℂ)) (x y : Space c) :
71     formWith d r (linearEquiv (p := p) c d e he x) (linearEquiv (p := p) c d e he y) =
72       formWith c r x y := by
73   simp only [formWith_apply]
74   apply congrArg r.symm
75   apply congrArg Additive.ofMul
76   apply Subtype.ext
77   exact quotientEquiv_pairing c d e he x.toMul y.toMul
78 
79 theorem linearEquiv_form (e : A ≃* B)
80     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b) (x y : Space c) :
81     form (p := p) d (linearEquiv (p := p) c d e he x) (linearEquiv (p := p) c d e he y) =
82       form (p := p) c x y := linearEquiv_formWith c d e he (rootEquiv p) x y
83 
84 /-- Representatives suffice for propositions about the actual quotient space. -/
85 theorem space_induction_on {P : Space c → Prop} (x : Space c)
86     (h : ∀ a : A, P (Additive.ofMul (QuotientGroup.mk a))) : P x :=
87   QuotientGroup.induction_on (C := fun z => P (Additive.ofMul z)) x.toMul h
88 
89 theorem linearEquiv_refl :
90     linearEquiv (p := p) c c (MulEquiv.refl A) (fun _ _ => rfl) =
91       LinearEquiv.refl (ZMod p) (Space c) := by
92   apply LinearEquiv.ext
93   intro x
94   apply space_induction_on c x
95   intro a
96   rfl
97 
98 theorem linearEquiv_trans (f : Cocycle D ℂˣ) [Fact (∀ a : D, a ^ p = 1)]
99     (e : A ≃* B) (e' : B ≃* D)
100     (he : ∀ a b, commutator d (e a) (e b) = commutator c a b)
101     (he' : ∀ a b, commutator f (e' a) (e' b) = commutator d a b) :
102     linearEquiv (p := p) c f (e.trans e')
103       (fun a b => (he' (e a) (e b)).trans (he a b)) =
104       (linearEquiv (p := p) c d e he).trans (linearEquiv (p := p) d f e' he') := by
105   apply LinearEquiv.ext
106   intro x
107   apply space_induction_on c x
108   intro a
109   rfl
110 
111 /-- A genuine group action on A preserving commutators descends to a genuine
112 linear action on its radical quotient. -/
113 def action {G : Type*} [Group G] (α : G →* MulAut A)
114     (hα : ∀ g a b, commutator c (α g a) (α g b) = commutator c a b) :
115     G →* (Space c ≃ₗ[ZMod p] Space c) where
116   toFun g := linearEquiv c c (α g) (hα g)
117   map_one' := by
118     apply LinearEquiv.ext
119     intro x
120     apply space_induction_on c x
121     intro a
122     change Additive.ofMul (QuotientGroup.mk (α 1 a)) = Additive.ofMul (QuotientGroup.mk a)
123     rw [map_one]
124     rfl
125   map_mul' g h := by
126     apply LinearEquiv.ext
127     intro x
128     apply space_induction_on c x
129     intro a
130     change Additive.ofMul (QuotientGroup.mk (α (g * h) a)) =
131       Additive.ofMul (QuotientGroup.mk (α g (α h a)))
132     rw [map_mul]
133     rfl
134 
135 @[simp] theorem action_mk {G : Type*} [Group G] (α : G →* MulAut A)
136     (hα : ∀ g a b, commutator c (α g a) (α g b) = commutator c a b)
137     (g : G) (a : A) :
138     action (p := p) c α hα g (Additive.ofMul (QuotientGroup.mk a)) =
139       Additive.ofMul (QuotientGroup.mk (α g a)) := rfl
140 
141 /-- Every group element preserves the constructed alternating nondegenerate form. -/
142 theorem action_form {G : Type*} [Group G] (α : G →* MulAut A)
143     (hα : ∀ g a b, commutator c (α g a) (α g b) = commutator c a b)
144     (g : G) (x y : Space c) :
145     form (p := p) c (action (p := p) c α hα g x) (action (p := p) c α hα g y) =
146       form (p := p) c x y := linearEquiv_form c c (α g) (hα g) x y
147 
148 end PaperXI.ElementaryEnvelope

Back to source controls