CyclicInducedWrap.lean

1 import PaperXI.CyclicInducedDegree
2 
3 /-! Explicit wrap coefficients in the Frobenius-indexed induced basis. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CyclicInduced
7 open scoped Classical
8 variable {G : Type*} [Group G] {n : ℕ} [NeZero n]
9 variable (d : G →* Multiplicative (ZMod n)) (φ : G)
10 variable (hφ : d φ = Multiplicative.ofAdd (1 : ZMod n))
11 variable (χ : d.ker →* ℂˣ)
12 
13 /-- The scalar coefficient is represented by the discrepancy in integer representatives. -/
14 theorem cyclicWeight_phi_value (j : ZMod n) :
15     cyclicWeight d φ hφ χ φ j =
16       χ ⟨φ ^ ((j.val : ℤ) + 1 - ((j + 1).val : ℤ)), by
17         apply Multiplicative.toAdd.injective
18         simp [map_zpow, hφ, toAdd_zpow, zsmul_eq_mul]⟩ := by
19   apply congrArg χ
20   apply Subtype.ext
21   change φ ^ (-((d φ * Multiplicative.ofAdd j).toAdd.val : ℤ)) * φ *
22     (φ ^ (-((d (cyclicRep φ (d φ * Multiplicative.ofAdd j) * φ))⁻¹).toAdd.val : ℤ))⁻¹ =
23       φ ^ ((j.val : ℤ) + 1 - ((j + 1).val : ℤ))
24   have hd : d (cyclicRep φ (d φ * Multiplicative.ofAdd j) * φ) =
25       (Multiplicative.ofAdd j)⁻¹ := by
26     rw [map_mul, cyclicRep_degree d φ hφ]
27     simp
28   rw [hd, inv_inv, hφ]
29   change φ ^ (-((1 + j).val : ℤ)) * φ * (φ ^ (-(j.val : ℤ)))⁻¹ =
30     φ ^ ((j.val : ℤ) + 1 - ((j + 1).val : ℤ))
31   rw [← zpow_neg, neg_neg]
32   rw [← zpow_add_one, ← zpow_add]
33   congr 1
34   rw [add_comm (1 : ZMod n) j]
35   omega
36 
37 /-- A full cycle is an element of the inducing subgroup. -/
38 def period : d.ker :=
39   ⟨φ ^ (n : ℤ), by
40     apply Multiplicative.toAdd.injective
41     simp [hφ]⟩
42 
43 /-- The integer discrepancy vanishes before the last residue. -/
44 theorem val_succ_of_lt (j : ZMod n) (hj : j.val + 1 < n) :
45     (j + 1).val = j.val + 1 := by
46   have he : j + 1 = ((j.val + 1 : ℕ) : ZMod n) := by simp
47   rw [he, ZMod.val_natCast, Nat.mod_eq_of_lt hj]
48 
49 /-- At the last residue the successor returns to zero. -/
50 theorem val_succ_of_last (j : ZMod n) (hj : j.val + 1 = n) :
51     (j + 1).val = 0 := by
52   have he : j + 1 = ((j.val + 1 : ℕ) : ZMod n) := by simp
53   rw [he, hj]
54   simp
55 
56 /-- Non-wrapping Frobenius steps have scalar one. -/
57 theorem cyclicWeight_phi_of_lt (j : ZMod n) (hj : j.val + 1 < n) :
58     cyclicWeight d φ hφ χ φ j = 1 := by
59   rw [cyclicWeight_phi_value]
60   calc χ _ = χ 1 := by
61          apply congrArg χ
62          apply Subtype.ext
63          change φ ^ ((j.val : ℤ) + 1 - ((j + 1).val : ℤ)) = 1
64          rw [val_succ_of_lt j hj]
65          simp
66        _ = 1 := map_one χ
67 
68 /-- The unique wrap step carries the actual value of the inducing character at `φ^n`. -/
69 theorem cyclicWeight_phi_of_last (j : ZMod n) (hj : j.val + 1 = n) :
70     cyclicWeight d φ hφ χ φ j = χ (period d φ hφ) := by
71   rw [cyclicWeight_phi_value]
72   apply congrArg χ
73   apply Subtype.ext
74   change φ ^ ((j.val : ℤ) + 1 - ((j + 1).val : ℤ)) = φ ^ (n : ℤ)
75   rw [val_succ_of_last j hj]
76   congr 1
77   omega
78 
79 section Degree
80 variable (ν : G →* Multiplicative ℤ)
81 variable (hν : ν φ = Multiplicative.ofAdd (1 : ℤ))
82 variable (ξ : TameDegree.degreeSubgroup ν n →* ℂˣ)
83 
84 /-- The source's full Frobenius period, as an actual subgroup element. -/
85 def degreePeriod : TameDegree.degreeSubgroup ν n :=
86   period (TameDegree.degreeMod ν n) φ (degreeMod_phi ν φ hν n)
87 
88 omit [NeZero n] in
89 @[simp] theorem degreePeriod_coe : (degreePeriod φ ν hν (n := n) : G) = φ ^ (n : ℤ) := rfl
90 
91 /-- Before wrap, the source Frobenius basis coefficient equals one. -/
92 theorem degreeWeight_phi_of_lt (j : ZMod n) (hj : j.val + 1 < n) :
93     degreeWeight ν φ hν n ξ φ j = 1 :=
94   cyclicWeight_phi_of_lt (TameDegree.degreeMod ν n) φ (degreeMod_phi ν φ hν n) ξ j hj
95 
96 /-- At wrap, the source basis coefficient is exactly the period character value. -/
97 theorem degreeWeight_phi_of_last (j : ZMod n) (hj : j.val + 1 = n) :
98     degreeWeight ν φ hν n ξ φ j = ξ (degreePeriod φ ν hν) :=
99   cyclicWeight_phi_of_last (TameDegree.degreeMod ν n) φ (degreeMod_phi ν φ hν n) ξ j hj
100 
101 /-- Explicit shift along the non-wrapping part of the induced basis. -/
102 theorem degreeBasis_phi_of_lt (j : ZMod n) (hj : j.val + 1 < n) :
103     degreeInduced ν n ξ φ (degreeBasis ν φ hν n ξ j) =
104       degreeBasis ν φ hν n ξ (j + 1) := by
105   rw [degreeBasis_action_phi, degreeWeight_phi_of_lt φ ν hν ξ j hj]
106   simp
107 
108 /-- Explicit closing step of the induced basis, including the case `n = 1`. -/
109 theorem degreeBasis_phi_of_last (j : ZMod n) (hj : j.val + 1 = n) :
110     degreeInduced ν n ξ φ (degreeBasis ν φ hν n ξ j) =
111       (ξ (degreePeriod φ ν hν) : ℂ) • degreeBasis ν φ hν n ξ 0 := by
112   rw [degreeBasis_action_phi, degreeWeight_phi_of_last φ ν hν ξ j hj]
113   have he : j + 1 = (0 : ZMod n) := by
114     apply ZMod.val_injective
115     simpa using val_succ_of_last j hj
116   rw [he]
117 end Degree
118 
119 end PaperXI.CyclicInduced

Back to source controls