ActualScalarLift113.lean

1 import PaperXI.ScalarRepresentation112
2 import PaperXI.CyclicDefect113
3 
4 /-! Honest actions on an actual group induce honest scalar-pushout actions.
5 The section phase and its multiplication law are conclusions. The original
6 theta, its literal kernel subgroup, and the quotient labels are retained. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ActualScalarLift113
10 open ScalarRepresentation112 ScalarCocycle112 CyclicDefect113
11 
12 variable {G A : Type*} [Group G] [CommGroup A]
13   (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
14   (hinv : TypeSideDescent.Invariant D θ)
15   (q : G →* A) (hker : q.ker = D)
16   (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
17 
18 /-- The scalar pushout map is derived from the actual normalized section. -/
19 def actualPushout : G →* Extension (actualScalarCocycle D θ hinv q hker t ht ht1) where
20   toFun g := ⟨sectionScalar D θ q hker t ht g, q g⟩
21   map_one' := by
22     apply Extension.ext
23     · exact sectionScalar_one D θ q hker t ht ht1
24     · exact q.map_one
25   map_mul' g h := by
26     apply Extension.ext
27     · exact sectionScalar_mul D θ hinv q hker t ht g h
28     · exact q.map_mul g h
29 
30 @[simp] theorem actualPushout_section (a : A) :
31     actualPushout D θ hinv q hker t ht ht1 (t a) =
32       Extension.sectionOf (actualScalarCocycle D θ hinv q hker t ht ht1) a := by
33   apply Extension.ext
34   · exact sectionScalar_section D θ q hker t ht a
35   · exact ht a
36 
37 @[simp] theorem actualPushout_subgroup (d : D) :
38     actualPushout D θ hinv q hker t ht ht1 (d : G) =
39       Extension.scalarInclusion (actualScalarCocycle D θ hinv q hker t ht ht1) (θ d) := by
40   apply Extension.ext
41   · exact sectionScalar_on_subgroup D θ q hker t ht ht1 d
42   · change (d : G) ∈ q.ker
43     rw [hker]
44     exact d.property
45 
46 variable (α : G ≃* G) (β : A ≃* A) (hq : ∀ g, q (α g) = β (q g))
47 
48 include hq in
49 /-- Powers of the quotient action are induced by the actual group action. -/
50 theorem quotient_action_power (n : ℕ) (g : G) :
51     q ((α ^ n) g) = (β ^ n) (q g) := by
52   induction n with
53   | zero => rfl
54   | succ n ih =>
55     rw [pow_succ', pow_succ']
56     change q (α ((α ^ n) g)) = β ((β ^ n) (q g))
57     rw [hq, ih]
58 
59 include hq ht in
60 /-- Honesty of the quotient's cyclic action is derived using the supplied
61 actual quotient section, rather than being an additional assumption. -/
62 theorem quotient_power_eq_one (n : ℕ) (hn : α ^ n = 1) : β ^ n = 1 := by
63   apply MulEquiv.ext
64   intro a
65   have h := quotient_action_power q α β hq n (t a)
66   rw [hn] at h
67   change q (t a) = (β ^ n) (q (t a)) at h
68   rw [ht] at h
69   exact h.symm
70 
71 /-- The subgroup map is induced by the actual automorphism and exact kernel. -/
72 def subgroupMap : D →* D where
73   toFun d := ⟨α (d : G), by
74     have hd : q (d : G) = 1 := by
75       change (d : G) ∈ q.ker
76       rw [hker]
77       exact d.property
78     have hm : α (d : G) ∈ q.ker := by
79       change q (α (d : G)) = 1
80       rw [hq, hd, map_one]
81     simpa only [hker] using hm⟩
82   map_one' := by apply Subtype.ext; exact α.map_one
83   map_mul' d e := by apply Subtype.ext; exact α.map_mul (d : G) (e : G)
84 
85 variable (hθ : ∀ d : D, θ (subgroupMap D q hker α β hq d) = θ d)
86 
87 /-- The phase is the original theta of the actual section discrepancy. -/
88 def actualPhase (a : A) : ℂˣ := sectionScalar D θ q hker t ht (α (t a))
89 
90 omit [D.Normal] in
91 include ht1 in
92 @[simp] theorem actualPhase_one : actualPhase D θ q hker t ht α 1 = 1 := by
93   simp only [actualPhase, ht1, map_one, sectionScalar_one D θ q hker t ht ht1]
94 
95 include hθ hinv ht1 in
96 /-- Scalar covariance follows from actual theta preservation, not from a
97 premise about a projective section or an already corrected cochain. -/
98 theorem sectionScalar_action (g : G) :
99     sectionScalar D θ q hker t ht (α g) =
100       sectionScalar D θ q hker t ht g * actualPhase D θ q hker t ht α (q g) := by
101   let d := sectionResidue D q hker t ht g
102   have hg : g = (d : G) * t (q g) := by
103     simp only [d, sectionResidue]
104     group
105   have hdq : q (α (d : G)) = 1 := by
106     rw [hq]
107     have hd : q (d : G) = 1 := by
108       change (d : G) ∈ q.ker
109       rw [hker]
110       exact d.property
111     rw [hd, map_one]
112   have hdθ : sectionScalar D θ q hker t ht (α (d : G)) = θ d := by
113     change sectionScalar D θ q hker t ht
114       (subgroupMap D q hker α β hq d : G) = θ d
115     rw [sectionScalar_on_subgroup D θ q hker t ht ht1, hθ]
116   calc
117     sectionScalar D θ q hker t ht (α g) =
118         sectionScalar D θ q hker t ht (α (d : G) * α (t (q g))) := by
119       rw [← map_mul, ← hg]
120     _ = θ d * actualPhase D θ q hker t ht α (q g) := by
121       rw [sectionScalar_mul D θ hinv, hdθ, hdq,
122         sectionCocycle_one_left D θ q hker t ht ht1, mul_one]
123       rfl
124     _ = _ := rfl
125 
126 include hθ hinv ht1 in
127 theorem actualPhase_mul (a b : A) :
128     sectionCocycle D θ q hker t ht a b * actualPhase D θ q hker t ht α (a*b) =
129       actualPhase D θ q hker t ht α a * actualPhase D θ q hker t ht α b *
130         sectionCocycle D θ q hker t ht (β a) (β b) := by
131   have h := sectionScalar_action D θ hinv q hker t ht ht1 α β hq hθ (t a * t b)
132   rw [map_mul α, sectionScalar_mul D θ hinv, hq, hq, ht, ht,
133     map_mul q, ht, ht] at h
134   exact h.symm
135 
136 /-- An actual automorphism induces an automorphism of the scalar pushout. -/
137 def actualLift : ScalarLift (actualScalarCocycle D θ hinv q hker t ht ht1) β where
138   action := {
139     toFun x := ⟨x.scalar * actualPhase D θ q hker t ht α x.base, β x.base⟩
140     invFun y := ⟨y.scalar / actualPhase D θ q hker t ht α (β.symm y.base), β.symm y.base⟩
141     left_inv x := by apply Extension.ext <;> simp
142     right_inv y := by apply Extension.ext <;> simp
143     map_mul' x y := by
144       apply Extension.ext
145       · change (x.scalar * y.scalar * sectionCocycle D θ q hker t ht x.base y.base) *
146           actualPhase D θ q hker t ht α (x.base*y.base) =
147           (x.scalar * actualPhase D θ q hker t ht α x.base) *
148           (y.scalar * actualPhase D θ q hker t ht α y.base) *
149           sectionCocycle D θ q hker t ht (β x.base) (β y.base)
150         rw [mul_assoc, actualPhase_mul D θ hinv q hker t ht ht1 α β hq hθ]
151         ac_rfl
152       · exact β.map_mul x.base y.base
153   }
154   on_base _ := rfl
155   fixes_scalar z := by
156     apply Extension.ext
157     · change z * actualPhase D θ q hker t ht α 1 = z
158       rw [actualPhase_one D θ q hker t ht ht1 α, mul_one]
159     · exact β.map_one
160 
161 theorem actualLift_phase (a : A) :
162     (actualLift D θ hinv q hker t ht ht1 α β hq hθ).phase a =
163       actualPhase D θ q hker t ht α a := by
164   change 1 * actualPhase D θ q hker t ht α a = _
165   exact one_mul _
166 
167 theorem actualLift_intertwines (g : G) :
168     (actualLift D θ hinv q hker t ht ht1 α β hq hθ).action
169       (actualPushout D θ hinv q hker t ht ht1 g) =
170         actualPushout D θ hinv q hker t ht ht1 (α g) := by
171   apply Extension.ext
172   · exact (sectionScalar_action D θ hinv q hker t ht ht1 α β hq hθ g).symm
173   · exact (hq g).symm
174 
175 theorem actualLift_power_intertwines (n : ℕ) (g : G) :
176     ((actualLift D θ hinv q hker t ht ht1 α β hq hθ).action ^ n)
177       (actualPushout D θ hinv q hker t ht ht1 g) =
178         actualPushout D θ hinv q hker t ht ht1 ((α ^ n) g) := by
179   induction n with
180   | zero => rfl
181   | succ n ih =>
182     rw [pow_succ', pow_succ']
183     change (actualLift D θ hinv q hker t ht ht1 α β hq hθ).action
184       (((actualLift D θ hinv q hker t ht ht1 α β hq hθ).action ^ n)
185         (actualPushout D θ hinv q hker t ht ht1 g)) =
186       actualPushout D θ hinv q hker t ht ht1 (α ((α ^ n) g))
187     rw [ih, actualLift_intertwines]
188 
189 /-- An honest cyclic action on the actual group gives an honest cyclic
190 action on the scalar pushout, with no separate phase-period hypothesis. -/
191 theorem actualLift_power_eq_one (n : ℕ) (hn : α ^ n = 1) :
192     (actualLift D θ hinv q hker t ht ht1 α β hq hθ).action ^ n = 1 := by
193   let c := actualScalarCocycle D θ hinv q hker t ht ht1
194   let L := actualLift D θ hinv q hker t ht ht1 α β hq hθ
195   have hfix (j : ℕ) (z : ℂˣ) : (L.action ^ j) (Extension.scalarInclusion c z) =
196       Extension.scalarInclusion c z := by
197     induction j with
198     | zero => rfl
199     | succ k ih =>
200       rw [pow_succ']
201       change L.action ((L.action ^ k) (Extension.scalarInclusion c z)) = _
202       rw [ih, L.fixes_scalar]
203   have hsec (a : A) : (L.action ^ n) (Extension.sectionOf c a) =
204       Extension.sectionOf c a := by
205     have h := actualLift_power_intertwines D θ hinv q hker t ht ht1 α β hq hθ n (t a)
206     rw [hn] at h
207     change (L.action ^ n) (actualPushout D θ hinv q hker t ht ht1 (t a)) =
208       actualPushout D θ hinv q hker t ht ht1 (t a) at h
209     simpa only [actualPushout_section] using h
210   apply MulEquiv.ext
211   intro x
212   have hx : x = Extension.scalarInclusion c x.scalar * Extension.sectionOf c x.base := by
213     apply Extension.ext
214     · change x.scalar = x.scalar * 1 *
215         (actualScalarCocycle D θ hinv q hker t ht ht1).coeff 1 x.base
216       rw [(actualScalarCocycle D θ hinv q hker t ht ht1).one_left, mul_one, mul_one]
217     · exact (one_mul x.base).symm
218   change (L.action ^ n) x = x
219   rw [hx, map_mul, hfix, hsec]
220 
221 end PaperXI.ActualScalarLift113

Back to source controls