InducedCycleInvariants.lean

1 import PaperXI.CyclicInducedWrap
2 import PaperXI.CycleCoordinates
3 
4 /-! Frobenius invariants of genuine degree-kernel induction. The basis and its
5 closing scalar are constructed from the inducing character. No cyclic matrix,
6 characteristic polynomial or return-map certificate is assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.InducedCycleInvariants
10 open Polynomial PaperXI.CyclicInduced
11 open scoped Classical
12 variable {G : Type*} [Group G]
13 variable (δ : G →* Multiplicative ℤ) (φ : G)
14 variable (hφ : δ φ = Multiplicative.ofAdd (1 : ℤ)) (n : ℕ) [NeZero n]
15 variable (ξ : TameDegree.degreeSubgroup δ n →* ℂˣ)
16 
17 /-- Residues as bounded integers; the forward map is the literal natural cast. -/
18 def indexEquiv : Fin n ≃ ZMod n where
19   toFun i := (i.val : ZMod n)
20   invFun j := ⟨j.val, j.val_lt⟩
21   left_inv i := by apply Fin.ext; simp [Nat.mod_eq_of_lt i.isLt]
22   right_inv j := by simp
23 
24 /-- The actual induced basis with a `Fin n` index for cyclic polynomial theorems. -/
25 def basis : Module.Basis (Fin n) ℂ (DegreeIndSpace δ n ξ) :=
26   (degreeBasis δ φ hφ n ξ).reindex (indexEquiv n).symm
27 
28 @[simp] theorem basis_apply (i : Fin n) :
29     basis δ φ hφ n ξ i = degreeBasis δ φ hφ n ξ (i.val : ZMod n) := by
30   simp [basis, indexEquiv]
31 
32 /-- The whole return scalar belongs to the full inducing character. -/
33 def returnScalar : ℂˣ := ξ (degreePeriod φ δ hφ)
34 
35 include hφ in
36 /-- The dimension of this induction does not require regularity. -/
37 theorem dimension : Module.finrank ℂ (DegreeIndSpace δ n ξ) = n := by
38   simpa using Module.finrank_eq_card_basis (basis δ φ hφ n ξ)
39 
40 /-- The actual Frobenius operator advances every non-wrapping basis vector. -/
41 theorem step (i : Fin n) (hi : i.val + 1 < n) :
42     degreeInduced δ n ξ φ (basis δ φ hφ n ξ i) =
43       basis δ φ hφ n ξ ⟨i.val + 1, hi⟩ := by
44   rw [basis_apply, basis_apply]
45   have hv : (i.val : ZMod n).val + 1 < n := by
46     simpa [ZMod.val_natCast, Nat.mod_eq_of_lt i.isLt] using hi
47   simpa [Nat.cast_add, Nat.cast_one] using
48     degreeBasis_phi_of_lt φ δ hφ ξ (i.val : ZMod n) hv
49 
50 /-- The wrapping step carries `ξ(φ^n)`, including degree one. -/
51 theorem closing_step (hn : 0 < n) :
52     degreeInduced δ n ξ φ (basis δ φ hφ n ξ ⟨n - 1, by omega⟩) =
53       (returnScalar δ φ hφ n ξ : ℂ) • basis δ φ hφ n ξ ⟨0, hn⟩ := by
54   rw [basis_apply, basis_apply]
55   have hl : ((n - 1 : ℕ) : ZMod n).val + 1 = n := by
56     rw [ZMod.val_natCast, Nat.mod_eq_of_lt (by omega : n - 1 < n)]
57     omega
58   simpa [returnScalar] using degreeBasis_phi_of_last φ δ hφ ξ ((n - 1 : ℕ) : ZMod n) hl
59 
60 /-- A cyclic orbit basis is a conclusion of the literal induction formulas. -/
61 theorem basis_powers (hn : 0 < n) (i : Fin n) :
62     basis δ φ hφ n ξ i = (degreeInduced δ n ξ φ ^ (i : ℕ))
63       (basis δ φ hφ n ξ ⟨0, hn⟩) :=
64   CycleCoordinates.basis_eq_powers _ hn (basis δ φ hφ n ξ)
65     (step δ φ hφ n ξ) i
66 
67 include hφ in
68 /-- Finite dimension is derived from the constructed induced basis. -/
69 theorem finiteSpace : FiniteDimensional ℂ (DegreeIndSpace δ n ξ) :=
70   Module.Finite.of_basis (basis δ φ hφ n ξ)
71 
72 variable [FiniteDimensional ℂ (DegreeIndSpace δ n ξ)]
73 
74 /-- The Frobenius characteristic polynomial and determinant of actual induction. -/
75 theorem cycle_invariants :
76     (degreeInduced δ n ξ φ).charpoly = X ^ n - C (returnScalar δ φ hφ n ξ : ℂ) ∧
77     (degreeInduced δ n ξ φ).det = (-1) ^ (n - 1) * (returnScalar δ φ hφ n ξ : ℂ) := by
78   exact CycleCoordinates.cycle_formula _ (Nat.pos_of_ne_zero (NeZero.ne n))
79     (basis δ φ hφ n ξ) (step δ φ hφ n ξ) _
80     (closing_step δ φ hφ n ξ (Nat.pos_of_ne_zero (NeZero.ne n)))
81 
82 /-- Read the return value from an intrinsic polynomial coefficient. -/
83 theorem returnScalar_from_charpoly :
84     (returnScalar δ φ hφ n ξ : ℂ) = -((degreeInduced δ n ξ φ).charpoly.coeff 0) := by
85   rw [(cycle_invariants δ φ hφ n ξ).1]
86   simp [Ne.symm (NeZero.ne n)]
87 
88 /-- The ambient determinant polynomial is not yet the inertia-fixed polynomial. -/
89 theorem ambient_polynomial :
90     Matrix.det (1 - (X : ℂ[X]) •
91       (LinearMap.toMatrix (basis δ φ hφ n ξ) (basis δ φ hφ n ξ)
92         (degreeInduced δ n ξ φ)).map C) =
93       1 - C (returnScalar δ φ hφ n ξ : ℂ) * X ^ n := by
94   exact CycleCoordinates.cycle_local_polynomial _ (Nat.pos_of_ne_zero (NeZero.ne n))
95     (basis δ φ hφ n ξ) (step δ φ hφ n ξ) _
96     (closing_step δ φ hφ n ξ (Nat.pos_of_ne_zero (NeZero.ne n)))
97 
98 /-- The full return operator is scalar, not just its action on one seed. -/
99 theorem return_operator :
100     degreeInduced δ n ξ φ ^ n =
101       (returnScalar δ φ hφ n ξ : ℂ) • LinearMap.id := by
102   have h := (degreeInduced δ n ξ φ).aeval_self_charpoly
103   rw [(cycle_invariants δ φ hφ n ξ).1] at h
104   simpa only [map_sub, map_pow, aeval_X, aeval_C, Algebra.algebraMap_eq_smul_one,
105     Module.End.one_eq_id, sub_eq_zero] using h
106 
107 end PaperXI.InducedCycleInvariants

Back to source controls