ClassInvariants.lean

1 import PaperX.RepresentationClasses
2 import PaperX.RepresentationTopology
3 
4 /-! Characteristic polynomials, trivial subgroup actions and actual finite-level
5 continuity are invariant under the matrix conjugacy used in representation
6 classes.  In particular one continuous representative suffices for every frame. -/
7 set_option autoImplicit false
8 namespace PaperX.ClassInvariants
9 open PaperX.RepresentationLimits PaperX.RepresentationClasses
10 open PaperX.RepresentationTopology
11 open scoped Topology
12 variable {R : Type*} [CommRing R] {G : Type*} [Group G]
13   {ι : Type*} [Fintype ι] [DecidableEq ι]
14 
15 @[simp] theorem charpoly_conjugate (u : (Matrix ι ι R)ˣ)
16     (ρ : MatrixRep R G ι) (g : G) : (conjugate u ρ g).charpoly = (ρ g).charpoly := by
17   change ((u : Matrix ι ι R) * ρ g * (↑(u⁻¹) : Matrix ι ι R)).charpoly = _
18   rw [Matrix.charpoly_mul_comm, ← mul_assoc]
19   simp
20 
21 @[simp] theorem det_conjugate (u : (Matrix ι ι R)ˣ)
22     (ρ : MatrixRep R G ι) (g : G) : (conjugate u ρ g).det = (ρ g).det := by
23   change ((u : Matrix ι ι R) * ρ g * (↑(u⁻¹) : Matrix ι ι R)).det = _
24   exact Matrix.det_units_conj u (ρ g)
25 
26 theorem charpoly_conjugacy {ρ σ : MatrixRep R G ι} (h : Conjugate ρ σ) (g : G) :
27     (ρ g).charpoly = (σ g).charpoly := by
28   obtain ⟨u, hu⟩ := h
29   rw [← hu, charpoly_conjugate]
30 
31 /-- The characteristic polynomial of the actual conjugacy class. -/
32 noncomputable def classCharpoly (c : ClassRep R G ι) (g : G) : Polynomial R :=
33   Quotient.lift (fun ρ : MatrixRep R G ι => (ρ g).charpoly)
34     (fun _ _ h => charpoly_conjugacy h g) c
35 
36 @[simp] theorem classCharpoly_classOf (ρ : MatrixRep R G ι) (g : G) :
37     classCharpoly (classOf ρ) g = (ρ g).charpoly := rfl
38 
39 theorem classCharpoly_changeCoefficients {S : Type*} [CommRing S] (f : R →+* S)
40     (c : ClassRep R G ι) (g : G) :
41     classCharpoly (changeClassCoefficients f c) g = (classCharpoly c g).map f := by
42   obtain ⟨ρ, rfl⟩ := classOf_surjective c
43   change (Matrix.map (ρ g) f).charpoly = (ρ g).charpoly.map f
44   exact Matrix.charpoly_map _ _
45 
46 /-- Triviality on a specified subgroup is unchanged by change of basis. -/
47 theorem trivial_conjugacy {ρ σ : MatrixRep R G ι} (h : Conjugate ρ σ) (H : Subgroup G) :
48     (∀ g, g ∈ H → ρ g = 1) ↔ (∀ g, g ∈ H → σ g = 1) := by
49   have forward : ∀ {τ υ : MatrixRep R G ι}, Conjugate τ υ →
50       (∀ g, g ∈ H → τ g = 1) → (∀ g, g ∈ H → υ g = 1) := by
51     intro τ υ ht hu g hg
52     obtain ⟨u, he⟩ := ht
53     rw [← he, conjugate_apply, hu g hg]
54     simp
55   exact ⟨forward h, forward (conjugate_symm h)⟩
56 
57 def ClassTrivial (H : Subgroup G) (c : ClassRep R G ι) : Prop :=
58   Quotient.lift (fun ρ : MatrixRep R G ι => ∀ g, g ∈ H → ρ g = 1)
59     (fun _ _ h => propext (trivial_conjugacy h H)) c
60 
61 @[simp] theorem classTrivial_classOf (H : Subgroup G) (ρ : MatrixRep R G ι) :
62     ClassTrivial H (classOf ρ) ↔ ∀ g, g ∈ H → ρ g = 1 := Iff.rfl
63 
64 variable [TopologicalSpace G]
65 
66 /-- A finite family of locally constant entries is locally constant as a matrix. -/
67 theorem finiteRepContinuous_matrix (ρ : MatrixRep R G ι) (h : FiniteRepContinuous ρ) :
68     FiniteContinuous ρ := by
69   intro x
70   have he : ∀ᶠ y in 𝓝 x, ∀ i j, ρ y i j = ρ x i j :=
71     Filter.eventually_all.mpr (fun i => Filter.eventually_all.mpr (fun j => h i j x))
72   exact he.mono (fun _ hy => funext (fun i => funext (hy i)))
73 
74 theorem finiteRepContinuous_conjugate (u : (Matrix ι ι R)ˣ)
75     {ρ : MatrixRep R G ι} (h : FiniteRepContinuous ρ) :
76     FiniteRepContinuous (conjugate u ρ) := by
77   intro i j x
78   filter_upwards [finiteRepContinuous_matrix ρ h x] with y hy
79   simp only [conjugate_apply, hy]
80 
81 theorem finiteRepContinuous_conjugacy {ρ σ : MatrixRep R G ι} (h : Conjugate ρ σ) :
82     FiniteRepContinuous ρ ↔ FiniteRepContinuous σ := by
83   have forward : ∀ {τ υ : MatrixRep R G ι}, Conjugate τ υ →
84       FiniteRepContinuous τ → FiniteRepContinuous υ := by
85     intro τ υ ht hc
86     obtain ⟨u, he⟩ := ht
87     rw [← he]
88     exact finiteRepContinuous_conjugate u hc
89   exact ⟨forward h, forward (conjugate_symm h)⟩
90 
91 theorem finiteContinuous_of_classOf_eq {ρ σ : MatrixRep R G ι}
92     (h : classOf ρ = classOf σ) (hc : FiniteRepContinuous σ) : FiniteRepContinuous ρ :=
93   (finiteRepContinuous_conjugacy (classOf_eq.mp h)).mpr hc
94 
95 /-- Actual continuity of a class is independent of its chosen matrix frame. -/
96 def ClassContinuous (c : ClassRep R G ι) : Prop :=
97   Quotient.lift (fun ρ : MatrixRep R G ι => FiniteRepContinuous ρ)
98     (fun _ _ h => propext (finiteRepContinuous_conjugacy h)) c
99 
100 @[simp] theorem classContinuous_classOf (ρ : MatrixRep R G ι) :
101     ClassContinuous (classOf ρ) ↔ FiniteRepContinuous ρ := Iff.rfl
102 
103 end PaperX.ClassInvariants

Back to source controls