CyclicInducedBasis.lean

1 import PaperXI.CyclicInducedCoordinates
2 import Mathlib.Data.ZMod.Basic
3 import Mathlib.Algebra.Group.TypeTags.Finite
4 
5 /-! The Frobenius-indexed basis of an actual induction from a cyclic degree kernel. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CyclicInduced
9 open scoped Classical
10 variable {G : Type*} [Group G] {n : ℕ} [NeZero n]
11 variable (d : G →* Multiplicative (ZMod n)) (φ : G)
12 variable (hφ : d φ = Multiplicative.ofAdd (1 : ZMod n))
13 
14 /-- Negative Frobenius powers represent the covariant-function cosets. -/
15 def cyclicRep (q : Multiplicative (ZMod n)) : G :=
16   φ ^ (-(q.toAdd.val : ℤ))
17 
18 include hφ in
19 theorem cyclicRep_degree (q : Multiplicative (ZMod n)) :
20     d (cyclicRep φ q) = q⁻¹ := by
21   apply Multiplicative.toAdd.injective
22   simp [cyclicRep, map_zpow, hφ, toAdd_zpow, zsmul_eq_mul]
23 
24 omit [NeZero n] in
25 @[simp] theorem cyclicRep_one : cyclicRep φ (1 : Multiplicative (ZMod n)) = 1 := by
26   simp [cyclicRep]
27 
28 variable (χ : d.ker →* ℂˣ)
29 /-- The actual induced basis indexed by residues, with representatives `φ^(-j.val)`. -/
30 def cyclicBasis : Module.Basis (ZMod n) ℂ (IndSpace d χ) :=
31   (basis d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ).reindex Multiplicative.toAdd
32 
33 /-- Actual monomial coefficient in the residue-indexed basis. -/
34 def cyclicWeight (g : G) (j : ZMod n) : ℂˣ :=
35   weight d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ g (Multiplicative.ofAdd j)
36 
37 @[simp] theorem cyclicBasis_apply (j : ZMod n) :
38     cyclicBasis d φ hφ χ j =
39       basis d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ (Multiplicative.ofAdd j) := by
40   rfl
41 
42 /-- Every group element translates the Frobenius index by its actual degree. -/
43 theorem cyclicBasis_action (g : G) (j : ZMod n) :
44     induced d χ g (cyclicBasis d φ hφ χ j) =
45       (cyclicWeight d φ hφ χ g j : ℂ) •
46       cyclicBasis d φ hφ χ (j + (d g).toAdd) := by
47   simpa [cyclicBasis_apply, cyclicWeight, add_comm, ofAdd_add, mul_comm] using
48     basis_action d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ g (Multiplicative.ofAdd j)
49 
50 /-- Conjugated inertia character `h ↦ χ(φ⁻ʲ h φʲ)`. -/
51 def cyclicCharacter (j : ZMod n) : d.ker →* ℂˣ :=
52   conjugateCharacter d (cyclicRep φ) χ (Multiplicative.ofAdd j)
53 
54 @[simp] theorem cyclicCharacter_apply (j : ZMod n) (h : d.ker) :
55     cyclicCharacter d φ χ j h =
56       χ ⟨φ ^ (-(j.val : ℤ)) * (h : G) * φ ^ (j.val : ℤ), by
57         have hh : d h = 1 := h.property
58         simp [MonoidHom.mem_ker, hh, map_zpow, zpow_neg]⟩ := by
59   apply congrArg χ
60   apply Subtype.ext
61   simp [conjugate, cyclicRep, zpow_neg]
62 
63 /-- The subgroup character acts diagonally by the expected Frobenius conjugates. -/
64 theorem cyclicBasis_action_kernel (h : d.ker) (j : ZMod n) :
65     induced d χ h (cyclicBasis d φ hφ χ j) =
66       (cyclicCharacter d φ χ j h : ℂ) • cyclicBasis d φ hφ χ j := by
67   exact basis_action_kernel d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ h
68     (Multiplicative.ofAdd j)
69 
70 /-- The zeroth line carries the original character. -/
71 theorem cyclicBasis_action_zero (h : d.ker) :
72     induced d χ h (cyclicBasis d φ hφ χ 0) =
73       (χ h : ℂ) • cyclicBasis d φ hφ χ 0 := by
74   exact basis_action_origin d (cyclicRep φ) (cyclicRep_degree d φ hφ) χ
75     (cyclicRep_one φ) h
76 
77 /-- Frobenius itself advances the residue by one. -/
78 theorem cyclicBasis_action_phi (j : ZMod n) :
79     induced d χ φ (cyclicBasis d φ hφ χ j) =
80       (cyclicWeight d φ hφ χ φ j : ℂ) • cyclicBasis d φ hφ χ (j + 1) := by
81   simpa [hφ] using cyclicBasis_action d φ hφ χ φ j
82 
83 end PaperXI.CyclicInduced

Back to source controls