RepresentationClasses.lean

1 import PaperX.RepresentationLimits
2 
3 /-! Actual matrix representations modulo change of basis.  The equivalence
4 relation uses invertible matrices, and coefficient maps reduce those matrices.
5 Finite coefficients give finite individual conjugacy classes even when the
6 source group is infinite. -/
7 set_option autoImplicit false
8 namespace PaperX.RepresentationClasses
9 open PaperX.RepresentationLimits
10 variable {R : Type*} [CommRing R] {G : Type*} [Group G]
11   {ι : Type*} [Fintype ι] [DecidableEq ι]
12 
13 /-- Conjugation by an actual invertible matrix. -/
14 def conjugate (u : (Matrix ι ι R)ˣ) (ρ : MatrixRep R G ι) : MatrixRep R G ι where
15   toFun g := (u : Matrix ι ι R) * ρ g * (↑(u⁻¹) : Matrix ι ι R)
16   map_one' := by simp
17   map_mul' g h := by simp [map_mul, mul_assoc]
18 
19 @[simp] theorem conjugate_apply (u : (Matrix ι ι R)ˣ)
20     (ρ : MatrixRep R G ι) (g : G) :
21     conjugate u ρ g = (u : Matrix ι ι R) * ρ g * (↑(u⁻¹) : Matrix ι ι R) := rfl
22 
23 @[simp] theorem conjugate_one (ρ : MatrixRep R G ι) : conjugate 1 ρ = ρ := by
24   apply MonoidHom.ext
25   intro g
26   simp [conjugate]
27 
28 @[simp] theorem conjugate_mul (u v : (Matrix ι ι R)ˣ)
29     (ρ : MatrixRep R G ι) : conjugate (u * v) ρ = conjugate u (conjugate v ρ) := by
30   apply MonoidHom.ext
31   intro g
32   simp [conjugate, mul_assoc]
33 
34 /-- Equality after a single invertible change of basis. -/
35 def Conjugate (ρ σ : MatrixRep R G ι) : Prop :=
36   ∃ u : (Matrix ι ι R)ˣ, conjugate u ρ = σ
37 
38 theorem conjugate_refl (ρ : MatrixRep R G ι) : Conjugate ρ ρ :=
39   ⟨1, conjugate_one ρ⟩
40 
41 theorem conjugate_symm {ρ σ : MatrixRep R G ι} (h : Conjugate ρ σ) : Conjugate σ ρ := by
42   obtain ⟨u, rfl⟩ := h
43   exact ⟨u⁻¹, by rw [← conjugate_mul]; simp⟩
44 
45 theorem conjugate_trans {ρ σ τ : MatrixRep R G ι}
46     (h : Conjugate ρ σ) (k : Conjugate σ τ) : Conjugate ρ τ := by
47   obtain ⟨u, rfl⟩ := h
48   obtain ⟨v, rfl⟩ := k
49   exact ⟨v * u, conjugate_mul v u ρ⟩
50 
51 def conjugacySetoid (R : Type*) [CommRing R] (G : Type*) [Group G]
52     (ι : Type*) [Fintype ι] [DecidableEq ι] : Setoid (MatrixRep R G ι) where
53   r := Conjugate
54   iseqv := ⟨conjugate_refl, conjugate_symm, conjugate_trans⟩
55 
56 /-- Isomorphism classes of finite free matrix representations. -/
57 def ClassRep (R : Type*) [CommRing R] (G : Type*) [Group G]
58     (ι : Type*) [Fintype ι] [DecidableEq ι] := Quotient (conjugacySetoid R G ι)
59 
60 def classOf (ρ : MatrixRep R G ι) : ClassRep R G ι := Quotient.mk _ ρ
61 
62 @[simp] theorem classOf_eq {ρ σ : MatrixRep R G ι} :
63     classOf ρ = classOf σ ↔ Conjugate ρ σ := Quotient.eq
64 
65 theorem classOf_surjective : Function.Surjective (classOf (R := R) (G := G) (ι := ι)) :=
66   Quotient.mk_surjective
67 
68 /-- A change of coefficients reduces the actual basis matrix. -/
69 theorem changeCoefficients_conjugate {S : Type*} [CommRing S] (f : R →+* S)
70     (u : (Matrix ι ι R)ˣ) (ρ : MatrixRep R G ι) :
71     changeCoefficients f (conjugate u ρ) =
72       conjugate (Units.map f.mapMatrix.toMonoidHom u) (changeCoefficients f ρ) := by
73   apply MonoidHom.ext
74   intro g
75   change f.mapMatrix ((u : Matrix ι ι R) * ρ g * (↑(u⁻¹) : Matrix ι ι R)) = _
76   simp only [map_mul]
77   rfl
78 
79 theorem changeCoefficients_conjugacy {S : Type*} [CommRing S] (f : R →+* S)
80     {ρ σ : MatrixRep R G ι} (h : Conjugate ρ σ) :
81     Conjugate (changeCoefficients f ρ) (changeCoefficients f σ) := by
82   obtain ⟨u, hu⟩ := h
83   refine ⟨Units.map f.mapMatrix.toMonoidHom u, ?_⟩
84   rw [← changeCoefficients_conjugate, hu]
85 
86 def changeClassCoefficients {S : Type*} [CommRing S] (f : R →+* S) :
87     ClassRep R G ι → ClassRep S G ι :=
88   Quotient.map (changeCoefficients f) (fun _ _ h => changeCoefficients_conjugacy f h)
89 
90 @[simp] theorem changeClassCoefficients_classOf {S : Type*} [CommRing S]
91     (f : R →+* S) (ρ : MatrixRep R G ι) :
92     changeClassCoefficients f (classOf ρ) = classOf (changeCoefficients f ρ) := rfl
93 
94 variable (I : Ideal R)
95 
96 def reduceClass (c : ClassRep R G ι) (k : ℕ) : ClassRep (R ⧸ I ^ k) G ι :=
97   changeClassCoefficients (Ideal.Quotient.mk (I ^ k)) c
98 
99 def transitionClass {j k : ℕ} (h : j ≤ k) :
100     ClassRep (R ⧸ I ^ k) G ι → ClassRep (R ⧸ I ^ j) G ι :=
101   changeClassCoefficients (Ideal.Quotient.factorPow I h)
102 
103 @[simp] theorem reduceClass_classOf (ρ : MatrixRep R G ι) (k : ℕ) :
104     reduceClass I (classOf ρ) k = classOf (reduce I ρ k) := rfl
105 
106 @[simp] theorem transitionClass_classOf {j k : ℕ} (h : j ≤ k)
107     (ρ : MatrixRep (R ⧸ I ^ k) G ι) :
108     transitionClass I h (classOf ρ) = classOf (transition I h ρ) := rfl
109 
110 @[simp] theorem transitionClass_reduceClass (c : ClassRep R G ι)
111     {j k : ℕ} (h : j ≤ k) : transitionClass I h (reduceClass I c k) = reduceClass I c j := by
112   obtain ⟨ρ, rfl⟩ := classOf_surjective c
113   simp
114 
115 @[simp] theorem transitionClass_self {k : ℕ} (c : ClassRep (R ⧸ I ^ k) G ι) :
116     transitionClass I (Nat.le_refl k) c = c := by
117   obtain ⟨ρ, rfl⟩ := classOf_surjective c
118   simp
119 
120 /-- Individual classes are finite over a finite coefficient ring.  No finiteness
121 or finite generation of the source group is needed. -/
122 theorem finite_class_fiber [Finite R] (c : ClassRep R G ι) :
123     Finite {ρ : MatrixRep R G ι // classOf ρ = c} := by
124   obtain ⟨σ, rfl⟩ := classOf_surjective c
125   let F : (Matrix ι ι R)ˣ → {ρ : MatrixRep R G ι // classOf ρ = classOf σ} :=
126     fun u => ⟨conjugate u σ, classOf_eq.mpr (conjugate_symm ⟨u, rfl⟩)⟩
127   apply Finite.of_surjective F
128   intro ρ
129   obtain ⟨u, hu⟩ := conjugate_symm (classOf_eq.mp ρ.property)
130   exact ⟨u, Subtype.ext hu⟩
131 
132 end PaperX.RepresentationClasses

Back to source controls