CyclicNormalization113.lean

1 import PaperXI.GlobalHeisenbergBridge112
2 import Mathlib.Data.Int.GCD
3 import Mathlib.GroupTheory.SpecificGroups.Cyclic
4 
5 /-! Same-carrier existence and uniqueness of determinant-one cyclic
6 implementers. The full automorphism and prescribed central character are
7 retained. No arithmetic realization or identification of the original kappa
8 is asserted. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.CyclicNormalization113
12 open Representation GlobalHeisenbergBridge112
13 
14 section ScalarCorrection
15 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
16 
17 /-- Scalar correction of an actual implementer on its original carrier. -/
18 def scale (c : ℂˣ) (A : V ≃ₗ[ℂ] V) : V ≃ₗ[ℂ] V :=
19   A.trans (LinearEquiv.smulOfUnit c)
20 
21 @[simp] theorem scale_apply (c : ℂˣ) (A : V ≃ₗ[ℂ] V) (v : V) :
22     scale c A v = (c : ℂ) • A v := rfl
23 
24 @[simp] theorem scale_pow_apply (c : ℂˣ) (A : V ≃ₗ[ℂ] V) (m : ℕ) (v : V) :
25     (scale c A ^ m) v = ((c ^ m : ℂˣ) : ℂ) • (A ^ m) v := by
26   induction m generalizing v with
27   | zero => simp
28   | succ m ih =>
29     rw [pow_succ, LinearEquiv.mul_apply, ih, scale_apply, map_smul]
30     simp only [pow_succ, Units.val_mul, smul_smul, LinearEquiv.mul_apply]
31 
32 /-- Bézout gives the unique d-th root among n-torsion scalars. -/
33 theorem scalar_correction_exists (u : ℂˣ) (n d : ℕ)
34     (hcop : Nat.Coprime n d) (hu : u ^ n = 1) :
35     ∃ c : ℂˣ, c ^ n = 1 ∧ c ^ d = u := by
36   refine ⟨u ^ Nat.gcdB n d, ?_, ?_⟩
37   · rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, hu, one_zpow]
38   · have he : (1 : ℤ) = (n : ℤ) * Nat.gcdA n d + (d : ℤ) * Nat.gcdB n d := by
39       simpa only [hcop, Nat.cast_one] using Nat.gcd_eq_gcd_ab n d
40     have hu' : u ^ (n : ℤ) = 1 := by simpa using hu
41     have h := congrArg (fun a : ℤ => u ^ a) he
42     rw [zpow_one, zpow_add, zpow_mul, zpow_mul, hu', one_zpow, one_mul] at h
43     rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul]
44     exact h.symm
45 
46 variable [FiniteDimensional ℂ V]
47 
48 @[simp] theorem det_scale (c : ℂˣ) (A : V ≃ₗ[ℂ] V) :
49     LinearEquiv.det (scale c A) = c ^ Module.finrank ℂ V * LinearEquiv.det A := by
50   apply Units.ext
51   rw [LinearEquiv.coe_det]
52   have he : (scale c A).toLinearMap = (c : ℂ) • A.toLinearMap := by ext v; rfl
53   rw [he, LinearMap.det_smul]
54   simp only [Units.val_mul, Units.val_pow_eq_pow_val, LinearEquiv.coe_det]
55 
56 /-- Every honest cyclic operator has a determinant-one scalar correction
57 when its order is coprime to the dimension. Both operators act on V. -/
58 theorem normalize_honest (A : V ≃ₗ[ℂ] V) (n : ℕ) (hAn : A ^ n = 1)
59     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
60     ∃ c : ℂˣ, c ^ n = 1 ∧ (scale c A) ^ n = 1 ∧
61       LinearEquiv.det (scale c A) = 1 := by
62   have hd : (LinearEquiv.det A) ^ n = 1 := by
63     rw [← map_pow, hAn, map_one]
64   obtain ⟨c, hcn, hcd⟩ := scalar_correction_exists (LinearEquiv.det A)⁻¹ n
65     (Module.finrank ℂ V) hcop (by rw [inv_pow, hd, inv_one])
66   refine ⟨c, hcn, ?_, ?_⟩
67   · ext v
68     simp only [scale_pow_apply, hcn, Units.val_one, one_smul, hAn]
69   · rw [det_scale, hcd, inv_mul_cancel]
70 
71 end ScalarCorrection
72 
73 section Implementers
74 variable {P V : Type*} [Group P] [AddCommGroup V] [Module ℂ V]
75 
76 /-- The implementer identity propagates to actual powers of the full
77 lifted automorphism, not merely its action on an associated graded space. -/
78 theorem implements_pow (ρ : Representation ℂ P V) (α : MulAut P)
79     (A : V ≃ₗ[ℂ] V)
80     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v)) (m : ℕ) :
81     ∀ p v, (A ^ m) (ρ p v) = ρ ((α ^ m) p) ((A ^ m) v) := by
82   induction m with
83   | zero => intro p v; rfl
84   | succ m ih =>
85     intro p v
86     change (A ^ m) (A (ρ p v)) = ρ ((α ^ m) (α p)) ((A ^ m) (A v))
87     rw [hA, ih]
88 
89 /-- Scalar correction preserves the exact same automorphism identity. -/
90 theorem scale_implements (ρ : Representation ℂ P V) (α : MulAut P)
91     (A : V ≃ₗ[ℂ] V) (c : ℂˣ)
92     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v)) :
93     ∀ p v, scale c A (ρ p v) = ρ (α p) (scale c A v) := by
94   intro p v
95   simp only [scale_apply, hA, map_smul]
96 
97 variable [FiniteDimensional ℂ V]
98 
99 /-- The n-th power of an arbitrary invertible implementer is scalar,
100 by Schur. The operator need not initially define an honest cyclic action. -/
101 theorem implementer_power_scalar (ρ : Representation ℂ P V) [IsIrreducible ρ]
102     (α : MulAut P) (A : V ≃ₗ[ℂ] V)
103     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
104     (n : ℕ) (hα : α ^ n = 1) :
105     ∃ z : ℂˣ, ∀ v, (A ^ n) v = (z : ℂ) • v := by
106   apply SchurScalar.commuting_unit ρ (A ^ n)
107   intro p v
108   simpa only [hα, MulAut.one_apply] using implements_pow ρ α A hA n p v
109 
110 /-- Nonzero complex scalars admit unit-valued n-th roots. -/
111 theorem unit_nth_root (z : ℂˣ) (n : ℕ) (hn : 0 < n) :
112     ∃ c : ℂˣ, c ^ n = z := by
113   obtain ⟨w, hw⟩ := IsAlgClosed.exists_pow_nat_eq (z : ℂ) hn
114   have hw0 : w ≠ 0 := by
115     intro h
116     rw [h, zero_pow (Nat.ne_of_gt hn)] at hw
117     exact z.ne_zero hw.symm
118   refine ⟨Units.mk0 w hw0, ?_⟩
119   apply Units.ext
120   exact hw
121 
122 /-- An arbitrary intertwining operator can be corrected on the same carrier
123 to an honest cyclic action. Only existence uses a complex root. -/
124 theorem normalize_order (ρ : Representation ℂ P V) [IsIrreducible ρ]
125     (α : MulAut P) (A : V ≃ₗ[ℂ] V)
126     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
127     (n : ℕ) (hn : 0 < n) (hα : α ^ n = 1) :
128     ∃ c : ℂˣ, (scale c A) ^ n = 1 ∧
129       ∀ p v, scale c A (ρ p v) = ρ (α p) (scale c A v) := by
130   obtain ⟨z, hz⟩ := implementer_power_scalar ρ α A hA n hα
131   obtain ⟨c, hc⟩ := unit_nth_root z⁻¹ n hn
132   refine ⟨c, ?_, scale_implements ρ α A c hA⟩
133   ext v
134   simp only [scale_pow_apply, hc, hz, smul_smul, ← Units.val_mul,
135     inv_mul_cancel, Units.val_one, one_smul, LinearEquiv.coe_one, id_eq]
136 
137 /-- Existence of the canonical normalized generator, obtained from an
138 arbitrary implementer by order correction followed by Bézout determinant
139 correction. The output is still an operator on the original V. -/
140 theorem normalized_generator_exists (ρ : Representation ℂ P V) [IsIrreducible ρ]
141     (α : MulAut P) (A : V ≃ₗ[ℂ] V)
142     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
143     (n : ℕ) (hn : 0 < n) (hα : α ^ n = 1)
144     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
145     ∃ B : V ≃ₗ[ℂ] V, B ^ n = 1 ∧ LinearEquiv.det B = 1 ∧
146       ∀ p v, B (ρ p v) = ρ (α p) (B v) := by
147   obtain ⟨c, hcn, hcA⟩ := normalize_order ρ α A hA n hn hα
148   obtain ⟨d, _, hdn, hd⟩ := normalize_honest (scale c A) n hcn hcop
149   exact ⟨scale d (scale c A), hdn, hd, scale_implements ρ α (scale c A) d hcA⟩
150 
151 /-- Two normalized implementers for the same full automorphism are equal.
152 The scalar ambiguity is killed by the coprime order and determinant powers. -/
153 theorem normalized_generator_unique (ρ : Representation ℂ P V) [IsIrreducible ρ]
154     (α : MulAut P) (A B : V ≃ₗ[ℂ] V)
155     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
156     (hB : ∀ p v, B (ρ p v) = ρ (α p) (B v))
157     (n : ℕ) (hAn : A ^ n = 1) (hBn : B ^ n = 1)
158     (hdetA : LinearEquiv.det A = 1) (hdetB : LinearEquiv.det B = 1)
159     (hcop : Nat.Coprime n (Module.finrank ℂ V)) : A = B := by
160   have he := generator_equivariant_of_det_coprime ρ ρ (LinearEquiv.refl ℂ V)
161     (fun _ _ => rfl) α A B hA hB n hAn hBn (hdetA.trans hdetB.symm) hcop
162   ext v
163   exact he v
164 
165 /-- Existence and uniqueness on the original carrier from an arbitrary
166 initial implementer. This proves independence of every root choice. -/
167 theorem normalized_generator_existsUnique (ρ : Representation ℂ P V) [IsIrreducible ρ]
168     (α : MulAut P) (A : V ≃ₗ[ℂ] V)
169     (hA : ∀ p v, A (ρ p v) = ρ (α p) (A v))
170     (n : ℕ) (hn : 0 < n) (hα : α ^ n = 1)
171     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
172     ∃! B : V ≃ₗ[ℂ] V, B ^ n = 1 ∧ LinearEquiv.det B = 1 ∧
173       ∀ p v, B (ρ p v) = ρ (α p) (B v) := by
174   obtain ⟨B, hBn, hdB, hB⟩ := normalized_generator_exists ρ α A hA n hn hα hcop
175   refine ⟨B, ⟨hBn, hdB, hB⟩, ?_⟩
176   intro C hC
177   exact normalized_generator_unique ρ α C B hC.2.2 hB n hC.1 hBn hC.2.1 hdB hcop
178 
179 end Implementers
180 
181 section ActualCharacter
182 variable {P V : Type*} [Group P] [Finite P]
183   [AddCommGroup V] [Module ℂ V]
184 
185 /-- An automorphism that acts through an actual automorphism of H and
186 preserves its prescribed central character supplies an implementer. Its
187 existence follows from the literal common trace profile, not from a chosen
188 cyclic extension or a presumed target equivalence. -/
189 theorem implementer_of_actual_profile
190     (H : Subgroup P) (θ : H →* ℂˣ)
191     (ρ : Representation ℂ P V) [IsIrreducible ρ]
192     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
193     (hz : ∀ p : P, p ∉ H → Representation.character ρ p = 0)
194     (α : MulAut P) (ζ : MulAut H)
195     (hαH : ∀ h : H, α (h : P) = (ζ h : P))
196     (hθ : ∀ h : H, θ (ζ h) = θ h) :
197     ∃ A : V ≃ₗ[ℂ] V, ∀ p v, A (ρ p v) = ρ (α p) (A v) := by
198   let σ := ρ.comp α.toMonoidHom
199   let : IsIrreducible σ :=
200     (QuotientRepresentation.irreducible_comp_iff α.toMonoidHom α.surjective ρ).mpr
201       inferInstance
202   have hσ : ∀ h : H, σ h = (θ h : ℂ) • LinearMap.id := by
203     intro h
204     change ρ (α (h : P)) = _
205     rw [hαH, hρ, hθ]
206   have hzσ : ∀ p : P, p ∉ H → Representation.character σ p = 0 := by
207     intro p hp
208     change Representation.character ρ (α p) = 0
209     apply hz
210     intro ha
211     obtain ⟨h, hh⟩ := ζ.surjective ⟨α p, ha⟩
212     have he : α (h : P) = α p := (hαH h).trans (congrArg Subtype.val hh)
213     exact hp ((α.injective he) ▸ h.property)
214   obtain ⟨U⟩ := equiv_of_common_profile H θ ρ σ hρ hσ hz hzσ
215   exact ⟨U.toLinearEquiv, U.toIntertwiningMap.isIntertwining⟩
216 
217 /-- Exact cyclic canonical-generator existence from actual finite
218 central-character and trace data. Finite dimensionality is derived. -/
219 theorem canonical_generator_of_actual_profile
220     (H : Subgroup P) (θ : H →* ℂˣ)
221     (ρ : Representation ℂ P V) [IsIrreducible ρ]
222     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
223     (hz : ∀ p : P, p ∉ H → Representation.character ρ p = 0)
224     (α : MulAut P) (ζ : MulAut H)
225     (hαH : ∀ h : H, α (h : P) = (ζ h : P))
226     (hθ : ∀ h : H, θ (ζ h) = θ h)
227     (n : ℕ) (hn : 0 < n) (hα : α ^ n = 1)
228     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
229     ∃! A : V ≃ₗ[ℂ] V, A ^ n = 1 ∧ LinearEquiv.det A = 1 ∧
230       ∀ p v, A (ρ p v) = ρ (α p) (A v) := by
231   let : FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional ρ
232   obtain ⟨A, hA⟩ := implementer_of_actual_profile H θ ρ hρ hz α ζ hαH hθ
233   exact normalized_generator_existsUnique ρ α A hA n hn hα hcop
234 
235 variable {k X : Type*} [Field k] [AddCommGroup X] [Module k X]
236 
237 /-- The trace condition itself follows from the original nondegenerate
238 commutator form. No implementer or action normalization is assumed. -/
239 theorem canonical_generator_of_actual_form
240     (H : Subgroup P) [H.Normal] (θ : H →* ℂˣ)
241     (τ : (P ⧸ H) ≃* Multiplicative X)
242     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
243     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
244     (hform : ∀ p q : P, ψ (B (HeisenbergCharacterProfile111.coordinate H τ p)
245       (HeisenbergCharacterProfile111.coordinate H τ q)) =
246       HeisenbergCharacterProfile111.characterCommutator H τ θ p q)
247     (ρ : Representation ℂ P V) [IsIrreducible ρ]
248     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
249     (α : MulAut P) (ζ : MulAut H)
250     (hαH : ∀ h : H, α (h : P) = (ζ h : P))
251     (hθ : ∀ h : H, θ (ζ h) = θ h)
252     (n : ℕ) (hn : 0 < n) (hα : α ^ n = 1)
253     (hcop : Nat.Coprime n (Module.finrank ℂ V)) :
254     ∃! A : V ≃ₗ[ℂ] V, A ^ n = 1 ∧ LinearEquiv.det A = 1 ∧
255       ∀ p v, A (ρ p v) = ρ (α p) (A v) :=
256   canonical_generator_of_actual_profile H θ ρ hρ
257     (HeisenbergCharacterProfile111.trace_support_of_nondegenerate_form
258       H τ θ B ψ hψ hnd hform ρ hρ) α ζ hαH hθ n hn hα hcop
259 
260 end ActualCharacter
261 
262 section CyclicActions
263 variable {C P V : Type*} [Group C] [Group P]
264   [AddCommGroup V] [Module ℂ V]
265 
266 /-- The corrected generator defines an honest action of the original cyclic
267 group C. Its relation is checked against the actual order of c. -/
268 def cyclicAction (c : C) (hgen : ∀ g : C, ∃ m : ℕ, g = c ^ m)
269     (A : V ≃ₗ[ℂ] V) (hA : A ^ orderOf c = 1) : C →* (V ≃ₗ[ℂ] V) :=
270   monoidHomOfForallMemZpowers
271     (fun g => by
272       obtain ⟨m, hm⟩ := hgen g
273       exact Subgroup.mem_zpowers_iff.mpr ⟨(m : ℤ), by simpa using hm.symm⟩)
274     (orderOf_dvd_of_pow_eq_one hA)
275 
276 @[simp] theorem cyclicAction_generator (c : C)
277     (hgen : ∀ g : C, ∃ m : ℕ, g = c ^ m)
278     (A : V ≃ₗ[ℂ] V) (hA : A ^ orderOf c = 1) :
279     cyclicAction c hgen A hA c = A := by
280   exact monoidHomOfForallMemZpowers_apply_gen _ _
281 
282 variable [FiniteDimensional ℂ V]
283 
284 /-- The cyclic canonical extension exists as a homomorphism on the original
285 group C, rather than only as a relation for one generator. -/
286 theorem canonical_action_of_implementer
287     (ρ : Representation ℂ P V) [IsIrreducible ρ]
288     (Ω : C →* MulAut P) (c : C) (hgen : ∀ g : C, ∃ m : ℕ, g = c ^ m)
289     (hn : 0 < orderOf c) (hcop : Nat.Coprime (orderOf c) (Module.finrank ℂ V))
290     (A : V ≃ₗ[ℂ] V) (hA : ∀ p v, A (ρ p v) = ρ (Ω c p) (A v)) :
291     ∃! Λ : C →* (V ≃ₗ[ℂ] V),
292       (∀ g, LinearEquiv.det (Λ g) = 1) ∧
293       (∀ g p v, Λ g (ρ p v) = ρ (Ω g p) (Λ g v)) := by
294   have hΩ : (Ω c) ^ orderOf c = 1 := by rw [← map_pow, pow_orderOf_eq_one, map_one]
295   obtain ⟨B, hBn, hdB, hB⟩ := normalized_generator_exists ρ (Ω c) A hA
296     (orderOf c) hn hΩ hcop
297   let Λ := cyclicAction c hgen B hBn
298   have hΛc : Λ c = B := cyclicAction_generator c hgen B hBn
299   have hdet : ∀ g, LinearEquiv.det (Λ g) = 1 := by
300     intro g
301     obtain ⟨m, rfl⟩ := hgen g
302     rw [map_pow, map_pow, hΛc, hdB, one_pow]
303   have himp : ∀ g p v, Λ g (ρ p v) = ρ (Ω g p) (Λ g v) := by
304     intro g p v
305     obtain ⟨m, rfl⟩ := hgen g
306     rw [map_pow, map_pow, hΛc]
307     exact implements_pow ρ (Ω c) B hB m p v
308   refine ⟨Λ, ⟨hdet, himp⟩, ?_⟩
309   intro Λ' hΛ'
310   have hΛ'n : Λ' c ^ orderOf c = 1 := by rw [← map_pow, pow_orderOf_eq_one, map_one]
311   have he : Λ' c = Λ c := (normalized_generator_unique ρ (Ω c) (Λ' c) B
312     (hΛ'.2 c) hB (orderOf c) hΛ'n hBn (hΛ'.1 c) hdB hcop).trans hΛc.symm
313   ext g
314   obtain ⟨m, rfl⟩ := hgen g
315   rw [map_pow, map_pow, he]
316 
317 end CyclicActions
318 
319 section CanonicalActualAction
320 variable {C P V : Type*} [Group C] [Group P] [Finite P]
321   [AddCommGroup V] [Module ℂ V]
322 
323 /-- A theta-preserving actual cyclic action on the finite group supplies
324 its unique determinant-one action on the original representation carrier. -/
325 theorem canonical_action_of_actual_profile
326     (H : Subgroup P) (θ : H →* ℂˣ)
327     (ρ : Representation ℂ P V) [IsIrreducible ρ]
328     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
329     (hz : ∀ p : P, p ∉ H → Representation.character ρ p = 0)
330     (Ω : C →* MulAut P) (c : C) (hgen : ∀ g : C, ∃ m : ℕ, g = c ^ m)
331     (ζ : MulAut H) (hΩH : ∀ h : H, Ω c (h : P) = (ζ h : P))
332     (hθ : ∀ h : H, θ (ζ h) = θ h)
333     (hn : 0 < orderOf c) (hcop : Nat.Coprime (orderOf c) (Module.finrank ℂ V)) :
334     ∃! Λ : C →* (V ≃ₗ[ℂ] V),
335       (∀ g, LinearEquiv.det (Λ g) = 1) ∧
336       (∀ g p v, Λ g (ρ p v) = ρ (Ω g p) (Λ g v)) := by
337   let : FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional ρ
338   obtain ⟨A, hA⟩ := implementer_of_actual_profile H θ ρ hρ hz (Ω c) ζ hΩH hθ
339   exact canonical_action_of_implementer ρ Ω c hgen hn hcop A hA
340 
341 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
342 
343 /-- The original common-profile bridge becomes cyclic equivariant for the
344 newly constructed canonical actions. Neither action nor a target bridge is
345 an input. This is a finite comparison, not an identification with an
346 arithmetic beta-extension whose normalization has not been checked. -/
347 theorem canonical_equivariant_bridge_of_actual_profile
348     (H : Subgroup P) (θ : H →* ℂˣ)
349     (ρ : Representation ℂ P V) (σ : Representation ℂ P W)
350     [IsIrreducible ρ] [IsIrreducible σ]
351     (hρ : ∀ h : H, ρ h = (θ h : ℂ) • LinearMap.id)
352     (hσ : ∀ h : H, σ h = (θ h : ℂ) • LinearMap.id)
353     (hzρ : ∀ p : P, p ∉ H → Representation.character ρ p = 0)
354     (hzσ : ∀ p : P, p ∉ H → Representation.character σ p = 0)
355     (Ω : C →* MulAut P) (c : C) (hgen : ∀ g : C, ∃ m : ℕ, g = c ^ m)
356     (ζ : MulAut H) (hΩH : ∀ h : H, Ω c (h : P) = (ζ h : P))
357     (hθ : ∀ h : H, θ (ζ h) = θ h)
358     (hn : 0 < orderOf c) (hcop : Nat.Coprime (orderOf c) (Module.finrank ℂ V)) :
359     ∃ (Λρ : C →* (V ≃ₗ[ℂ] V)) (Λσ : C →* (W ≃ₗ[ℂ] W))
360       (U : Representation.Equiv ρ σ),
361       (∀ g, LinearEquiv.det (Λρ g) = 1) ∧
362       (∀ g, LinearEquiv.det (Λσ g) = 1) ∧
363       (∀ g p v, Λρ g (ρ p v) = ρ (Ω g p) (Λρ g v)) ∧
364       (∀ g p w, Λσ g (σ p w) = σ (Ω g p) (Λσ g w)) ∧
365       (∀ g v, U (Λρ g v) = Λσ g (U v)) := by
366   let : FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional ρ
367   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional σ
368   obtain ⟨U⟩ := equiv_of_common_profile H θ ρ σ hρ hσ hzρ hzσ
369   have hdim : Module.finrank ℂ V = Module.finrank ℂ W := U.toLinearEquiv.finrank_eq
370   obtain ⟨Λρ, hΛρ, _⟩ := canonical_action_of_actual_profile H θ ρ hρ hzρ Ω c hgen ζ hΩH
371     hθ hn hcop
372   obtain ⟨Λσ, hΛσ, _⟩ := canonical_action_of_actual_profile H θ σ hσ hzσ Ω c hgen ζ hΩH
373     hθ hn (hdim ▸ hcop)
374   refine ⟨Λρ, Λσ, U, hΛρ.1, hΛσ.1, hΛρ.2, hΛσ.2, ?_⟩
375   apply cyclic_equivariant_of_generator Λρ Λσ c hgen U.toLinearEquiv
376   apply generator_equivariant_of_det_coprime ρ σ U.toLinearEquiv
377     U.toIntertwiningMap.isIntertwining (Ω c) (Λρ c) (Λσ c) (hΛρ.2 c) (hΛσ.2 c)
378     (orderOf c)
379   · rw [← map_pow, pow_orderOf_eq_one, map_one]
380   · rw [← map_pow, pow_orderOf_eq_one, map_one]
381   · exact (hΛρ.1 c).trans (hΛσ.1 c).symm
382   · exact hcop
383 
384 end CanonicalActualAction
385 
386 end PaperXI.CyclicNormalization113

Back to source controls