DenseFrobenius.lean

1 import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
2 import Mathlib.Topology.Algebra.Group.Matrix
3 import Mathlib.Topology.Algebra.ContinuousMonoidHom
4 import Mathlib.Topology.Separation.Hausdorff
5 
6 /-! Dense Frobenius conjugacy classes determine the actual characteristic polynomial
7 of a continuous matrix representation. Coefficient continuity is proved from the
8 principal-minor formula; no topology on a polynomial space is assumed. -/
9 set_option autoImplicit false
10 
11 namespace PaperXII.DenseFrobenius
12 
13 open Matrix
14 
15 variable {R X Γ Ω ι : Type*} [CommRing R] [TopologicalSpace R]
16     [IsTopologicalRing R] [TopologicalSpace X] [Fintype ι] [DecidableEq ι]
17 
18 /-- Every characteristic-polynomial coefficient is a continuous function of the matrix. -/
19 theorem continuous_charpoly_coeff {A : X → Matrix ι ι R} (hA : Continuous A) (k : ℕ) :
20     Continuous (fun x ↦ (A x).charpoly.coeff k) := by
21   classical
22   cases subsingleton_or_nontrivial R with
23   | inl hR =>
24     exact continuous_of_const (fun _ _ ↦ Subsingleton.elim _ _)
25   | inr hR =>
26     by_cases hk : k ≤ Fintype.card ι
27     · have hformula (x : X) :=
28         Matrix.charpoly_coeff_eq_sum_minors (A x) (Fintype.card ι - k) (Nat.sub_le _ _)
29       have hind : Fintype.card ι - (Fintype.card ι - k) = k := Nat.sub_sub_self hk
30       simp only [hind] at hformula
31       simp_rw [hformula]
32       refine continuous_const.mul (continuous_finsetSum _ fun s _ ↦ ?_)
33       exact (hA.matrix_submatrix Subtype.val Subtype.val).matrix_det
34     · have hzero (x : X) : (A x).charpoly.coeff k = 0 :=
35         Polynomial.coeff_eq_zero_of_natDegree_lt (by
36           rw [Matrix.charpoly_natDegree_eq_dim]
37           exact Nat.lt_of_not_ge hk)
38       simp_rw [hzero]
39       exact continuous_const
40 
41 variable [Group Γ]
42 
43 /-- The actual union of conjugacy classes of the declared good Frobenius elements. -/
44 def conjugacySaturation (frob : Ω → Γ) (good : Ω → Prop) : Set Γ :=
45   {g | ∃ v, good v ∧ ∃ h, g = h * frob v * h⁻¹}
46 
47 /-- Each good Frobenius lies in its conjugacy saturation. -/
48 theorem frobenius_mem_saturation (frob : Ω → Γ) (good : Ω → Prop)
49     (v : Ω) (hv : good v) : frob v ∈ conjugacySaturation frob good := by
50   exact ⟨v, hv, 1, by simp⟩
51 
52 /-- Increasing the good set increases the union of Frobenius conjugacy classes. -/
53 theorem conjugacySaturation_mono (frob : Ω → Γ) {good₁ good₂ : Ω → Prop}
54     (hgood : ∀ v, good₁ v → good₂ v) :
55     conjugacySaturation frob good₁ ⊆ conjugacySaturation frob good₂ := by
56   rintro g ⟨v, hv, h, heq⟩
57   exact ⟨v, hgood v hv, h, heq⟩
58 
59 variable [TopologicalSpace Γ]
60 
61 omit [IsTopologicalRing R] in
62 /-- Actual conjugation in the source group leaves a representation's characteristic polynomial fixed. -/
63 theorem charpoly_conjugate (ρ : Γ →ₜ* GL ι R) (g h : Γ) :
64     (ρ (h * g * h⁻¹)).val.charpoly = (ρ g).val.charpoly := by
65   rw [map_mul, map_mul, map_inv]
66   change ((ρ h).val * (ρ g).val * ((ρ h)⁻¹).val).charpoly = _
67   simpa only [Matrix.coe_units_inv] using
68     Matrix.charpoly_units_conj (ρ h) (ρ g).val
69 
70 /-- Continuity of each polynomial coefficient follows from continuity of the actual representation. -/
71 theorem continuous_rep_charpoly_coeff (ρ : Γ →ₜ* GL ι R) (k : ℕ) :
72     Continuous (fun g ↦ (ρ g).val.charpoly.coeff k) :=
73   continuous_charpoly_coeff (Units.continuous_val.comp ρ.continuous) k
74 
75 omit [IsTopologicalRing R] in
76 /-- Equality on good Frobenius elements gives equality on their entire conjugacy saturation. -/
77 theorem charpoly_eq_on_saturation (ρ σ : Γ →ₜ* GL ι R)
78     (frob : Ω → Γ) (good : Ω → Prop)
79     (hpoly : ∀ v, good v → (ρ (frob v)).val.charpoly = (σ (frob v)).val.charpoly) :
80     Set.EqOn (fun g ↦ (ρ g).val.charpoly) (fun g ↦ (σ g).val.charpoly)
81       (conjugacySaturation frob good) := by
82   rintro g ⟨v, hv, h, rfl⟩
83   dsimp only
84   rw [charpoly_conjugate, charpoly_conjugate, hpoly v hv]
85 
86 /-- A dense set of good Frobenius conjugacy classes determines every characteristic polynomial. -/
87 theorem charpoly_eq_of_dense_frobenius [T2Space R] (ρ σ : Γ →ₜ* GL ι R)
88     (frob : Ω → Γ) (good : Ω → Prop)
89     (hdense : Dense (conjugacySaturation frob good))
90     (hpoly : ∀ v, good v → (ρ (frob v)).val.charpoly = (σ (frob v)).val.charpoly) :
91     ∀ g, (ρ g).val.charpoly = (σ g).val.charpoly := by
92   intro g
93   apply Polynomial.ext
94   intro k
95   have hcoeff := Continuous.ext_on hdense
96     (continuous_rep_charpoly_coeff ρ k) (continuous_rep_charpoly_coeff σ k)
97     (fun x hx ↦ congrArg (fun P : Polynomial R ↦ P.coeff k)
98       (charpoly_eq_on_saturation ρ σ frob good hpoly hx))
99   exact congrFun hcoeff g
100 
101 /-- Matching a common coefficient-field polynomial spine implies equality everywhere.
102 The ring homomorphism need not be continuous: the mapped polynomials are fixed values. -/
103 theorem common_spine_charpoly_eq [T2Space R] {L : Type*} [CommRing L]
104     (ρ σ : Γ →ₜ* GL ι R) (frob : Ω → Γ) (good : Ω → Prop)
105     (hdense : Dense (conjugacySaturation frob good))
106     (emb : L →+* R) (P : Ω → Polynomial L)
107     (hρ : ∀ v, good v → (ρ (frob v)).val.charpoly = (P v).map emb)
108     (hσ : ∀ v, good v → (σ (frob v)).val.charpoly = (P v).map emb) :
109     ∀ g, (ρ g).val.charpoly = (σ g).val.charpoly :=
110   charpoly_eq_of_dense_frobenius ρ σ frob good hdense
111     (fun v hv ↦ (hρ v hv).trans (hσ v hv).symm)
112 
113 end PaperXII.DenseFrobenius

Back to source controls