InvariantPolynomial.lean

1 import PaperXI.InertiaFixed
2 import PaperXI.CyclicPolynomial
3 
4 /-! The local polynomial is attached to Frobenius restricted to the actual
5 invariant subspace. Its determinant meaning is proved before its evaluation. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.InvariantPolynomial
9 open Polynomial
10 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.InertiaFixed
11 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
12 
13 def operatorPolynomial [FiniteDimensional K V] (F : Module.End K V) : K[X] :=
14   F.charpoly.reverse
15 
16 theorem operatorPolynomial_eq_det [FiniteDimensional K V] (F : Module.End K V)
17     {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K V) :
18     operatorPolynomial F = Matrix.det (1 - (X : K[X]) • (LinearMap.toMatrix b b F).map C) := by
19   rw [operatorPolynomial, ← LinearMap.charpoly_toMatrix F b, Matrix.reverse_charpoly]
20   rfl
21 
22 theorem operatorPolynomial_of_subsingleton [FiniteDimensional K V] [Subsingleton V]
23     (F : Module.End K V) : operatorPolynomial F = 1 := by
24   have hF : F = 0 := Subsingleton.elim _ _
25   simp [operatorPolynomial, hF, Module.finrank_zero_of_subsingleton, Polynomial.reverse]
26 
27 variable {W : Type*} [AddCommGroup W] [Module K W]
28 
29 theorem operatorPolynomial_conj [FiniteDimensional K V] [FiniteDimensional K W]
30     (e : V ≃ₗ[K] W) (F : Module.End K V) :
31     operatorPolynomial (e.conj F) = operatorPolynomial F := by
32   simp [operatorPolynomial]
33 
34 variable {U : Type*} [AddCommGroup U] [Module ℂ U]
35 variable {M : ℕ} [NeZero M]
36 
37 /-- Frobenius and its inverse act on the actual Mathlib invariant subspace. -/
38 def fixedFrobenius (ρ : Action (K := ℂ) (V := U) (M := M))
39     (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
40     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) :
41     ρ.invariants ≃ₗ[ℂ] ρ.invariants where
42   toFun v := ⟨F v, fixed_forward ρ F q h v.property⟩
43   invFun v := ⟨F.symm v, fixed_backward ρ F q h v.property⟩
44   left_inv v := by ext; simp
45   right_inv v := by ext; simp
46   map_add' v w := by ext; simp
47   map_smul' c v := by ext; simp
48 
49 theorem fixedFrobenius_apply (ρ : Action (K := ℂ) (V := U) (M := M))
50     (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
51     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (v : ρ.invariants) :
52     (fixedFrobenius ρ F q h v : U) = F v := rfl
53 
54 /-- This definition uses the restricted operator, with no case split on a label. -/
55 def localPolynomial [FiniteDimensional ℂ U]
56     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
57     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) : ℂ[X] :=
58   operatorPolynomial (fixedFrobenius ρ F q h).toLinearMap
59 
60 theorem localPolynomial_eq_det [FiniteDimensional ℂ U]
61     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
62     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
63     {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℂ ρ.invariants) :
64     localPolynomial ρ F q h = Matrix.det
65       (1 - (X : ℂ[X]) • (LinearMap.toMatrix b b (fixedFrobenius ρ F q h).toLinearMap).map C) :=
66   operatorPolynomial_eq_det _ b
67 
68 theorem fixed_conj_of_top (ρ : Action (K := ℂ) (V := U) (M := M))
69     (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
70     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (htop : ρ.invariants = ⊤) :
71     (LinearEquiv.ofTop ρ.invariants htop).conj (fixedFrobenius ρ F q h).toLinearMap =
72       F.toLinearMap := by
73   ext v
74   simp [LinearEquiv.conj_apply_apply, fixedFrobenius]
75 
76 theorem localPolynomial_of_top [FiniteDimensional ℂ U]
77     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
78     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (htop : ρ.invariants = ⊤) :
79     localPolynomial ρ F q h = operatorPolynomial F.toLinearMap := by
80   rw [localPolynomial, ← operatorPolynomial_conj (LinearEquiv.ofTop ρ.invariants htop),
81     fixed_conj_of_top]
82 
83 theorem localPolynomial_of_bot [FiniteDimensional ℂ U]
84     (ρ : Action (K := ℂ) (V := U) (M := M)) (F : U ≃ₗ[ℂ] U) (q : (ZMod M)ˣ)
85     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (hbot : ρ.invariants = ⊥) :
86     localPolynomial ρ F q h = 1 := by
87   have : Subsingleton ρ.invariants := Submodule.subsingleton_iff_eq_bot.mpr hbot
88   exact operatorPolynomial_of_subsingleton _
89 
90 end PaperXI.InvariantPolynomial

Back to source controls