RepresentationLimits.lean

1 import PaperX.Reconstruction
2 import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
3 import Mathlib.RepresentationTheory.Basic
4 
5 /-! Actual matrix representations reconstructed from compatible finite quotients.
6 Completeness and separatedness are explicit. No companion existence is assumed
7 inside the constructions. A group homomorphism into matrices has invertible
8 images, and it is also converted to Mathlib's ordinary Representation type. -/
9 set_option autoImplicit false
10 namespace PaperX.RepresentationLimits
11 open scoped BigOperators
12 variable {R : Type*} [CommRing R] (I : Ideal R)
13 
14 /-- A compatible scalar family is realized using the already checked ring-map
15 reconstruction, applied to evaluation of the polynomial generator. -/
16 def scalarFamily (a : (k : ℕ) → R ⧸ I^k)
17     (h : ∀ {j k} (hjk : j ≤ k), Ideal.Quotient.factorPow I hjk (a k) = a j) :
18     PaperX.Reconstruction.RingFamily (Polynomial R) I where
19   maps k := Polynomial.eval₂RingHom (Ideal.Quotient.mk (I^k)) (a k)
20   compatible := by
21     intro j k hjk
22     apply Polynomial.ringHom_ext
23     · intro c
24       simp
25     · simpa using h hjk
26 
27 noncomputable def scalarLift [IsAdicComplete I R] (a : (k : ℕ) → R ⧸ I^k)
28     (h : ∀ {j k} (hjk : j ≤ k), Ideal.Quotient.factorPow I hjk (a k) = a j) : R :=
29   PaperX.Reconstruction.reconstruct I (scalarFamily I a h) Polynomial.X
30 
31 @[simp] theorem scalarLift_reduces [IsAdicComplete I R]
32     (a : (k : ℕ) → R ⧸ I^k)
33     (h : ∀ {j k} (hjk : j ≤ k), Ideal.Quotient.factorPow I hjk (a k) = a j) (k : ℕ) :
34     Ideal.Quotient.mk (I^k) (scalarLift I a h) = a k := by
35   have H := RingHom.congr_fun
36     (PaperX.Reconstruction.reconstruct_reduces I (scalarFamily I a h) k) Polynomial.X
37   simpa [scalarLift, scalarFamily] using H
38 
39 /-- Equality is detected by all finite coefficient precisions. -/
40 theorem scalar_ext [IsHausdorff I R] {a b : R}
41     (h : ∀ k, Ideal.Quotient.mk (I^k) a = Ideal.Quotient.mk (I^k) b) : a = b := by
42   exact congrFun (IsHausdorff.funext' I (f := fun _ : Unit => a)
43     (g := fun _ : Unit => b) (fun k _ => h k)) ()
44 
45 variable {G : Type*} [Group G] {ι : Type*} [Fintype ι] [DecidableEq ι]
46 
47 /-- This is an actual matrix-valued monoid homomorphism, not a family with a
48 postulated limit. Inverses follow from the source being a group. -/
49 abbrev MatrixRep (R : Type*) [CommRing R] (G : Type*) [Group G]
50     (ι : Type*) [Fintype ι] [DecidableEq ι] := G →* Matrix ι ι R
51 
52 def changeCoefficients {S : Type*} [CommRing S] (f : R →+* S)
53     (ρ : MatrixRep R G ι) : MatrixRep S G ι :=
54   f.mapMatrix.toMonoidHom.comp ρ
55 
56 @[simp] theorem changeCoefficients_apply {S : Type*} [CommRing S]
57     (f : R →+* S) (ρ : MatrixRep R G ι) (g : G) (i j : ι) :
58     changeCoefficients f ρ g i j = f (ρ g i j) := rfl
59 
60 def reduce (ρ : MatrixRep R G ι) (k : ℕ) : MatrixRep (R ⧸ I^k) G ι :=
61   changeCoefficients (Ideal.Quotient.mk (I^k)) ρ
62 
63 def transition {j k : ℕ} (h : j ≤ k) :
64     MatrixRep (R ⧸ I^k) G ι → MatrixRep (R ⧸ I^j) G ι :=
65   changeCoefficients (Ideal.Quotient.factorPow I h)
66 
67 @[simp] theorem transition_reduce (ρ : MatrixRep R G ι) {j k : ℕ} (h : j ≤ k) :
68     transition I h (reduce I ρ k) = reduce I ρ j := by
69   ext g i l
70   simp [transition, reduce]
71 
72 @[simp] theorem transition_self {k : ℕ} (ρ : MatrixRep (R ⧸ I^k) G ι) :
73     transition I (Nat.le_refl k) ρ = ρ := by
74   ext g i j
75   simp [transition]
76 
77 /-- Full compatibility, including the unique trivial precision-zero quotient. -/
78 structure Family (R : Type*) [CommRing R] (I : Ideal R)
79     (G : Type*) [Group G] (ι : Type*) [Fintype ι] [DecidableEq ι] where
80   maps : (k : ℕ) → MatrixRep (R ⧸ I^k) G ι
81   compatible : ∀ {j k} (h : j ≤ k), transition I h (maps k) = maps j
82 
83 theorem family_ext {f g : Family R I G ι} (h : f.maps = g.maps) : f = g := by
84   cases f
85   cases g
86   cases h
87   rfl
88 
89 def reduceFamily (ρ : MatrixRep R G ι) : Family R I G ι where
90   maps := reduce I ρ
91   compatible := transition_reduce I ρ
92 
93 noncomputable def liftMatrix [IsAdicComplete I R] (f : Family R I G ι) (g : G) :
94     Matrix ι ι R := fun i j => scalarLift I (fun k => f.maps k g i j)
95       (fun h => congrArg (fun ρ => ρ g i j) (f.compatible h))
96 
97 @[simp] theorem liftMatrix_reduces [IsAdicComplete I R] (f : Family R I G ι)
98     (g : G) (k : ℕ) : (liftMatrix I f g).map (Ideal.Quotient.mk (I^k)) = f.maps k g := by
99   ext i j
100   simp only [liftMatrix, Matrix.map_apply]
101   apply scalarLift_reduces
102   intro j' k' hjk
103   exact congrArg (fun ρ => ρ g i j) (f.compatible hjk)
104 
105 omit [Fintype ι] [DecidableEq ι] in
106 /-- Entrywise separatedness gives equality of actual matrices. -/
107 theorem matrix_ext [IsHausdorff I R] {A B : Matrix ι ι R}
108     (h : ∀ k, A.map (Ideal.Quotient.mk (I^k)) = B.map (Ideal.Quotient.mk (I^k))) : A = B := by
109   ext i j
110   exact scalar_ext I (fun k => congrArg (fun M => M i j) (h k))
111 
112 noncomputable def reconstruct [IsAdicComplete I R] (f : Family R I G ι) :
113     MatrixRep R G ι where
114   toFun := liftMatrix I f
115   map_one' := by
116     apply matrix_ext I
117     intro k
118     rw [liftMatrix_reduces, map_one]
119     symm
120     exact (Ideal.Quotient.mk (I^k)).mapMatrix.map_one
121   map_mul' g h := by
122     apply matrix_ext I
123     intro k
124     rw [liftMatrix_reduces, Matrix.map_mul, liftMatrix_reduces, liftMatrix_reduces,
125       map_mul]
126 
127 @[simp] theorem reconstruct_reduces [IsAdicComplete I R] (f : Family R I G ι) (k : ℕ) :
128     reduce I (reconstruct I f) k = f.maps k := by
129   ext g i j
130   exact congrArg (fun M => M i j) (liftMatrix_reduces I f g k)
131 
132 theorem reconstruct_unique [IsAdicComplete I R] (f : Family R I G ι)
133     (ρ : MatrixRep R G ι) (h : ∀ k, reduce I ρ k = f.maps k) : ρ = reconstruct I f := by
134   ext g i j
135   apply scalar_ext I
136   intro k
137   exact (congrArg (fun τ => τ g i j) (h k)).trans
138     (congrArg (fun τ => τ g i j) (reconstruct_reduces I f k)).symm
139 
140 @[simp] theorem reconstruct_reduce [IsAdicComplete I R] (ρ : MatrixRep R G ι) :
141     reconstruct I (reduceFamily I ρ) = ρ :=
142   (reconstruct_unique I _ ρ (fun _ => rfl)).symm
143 
144 @[simp] theorem reduce_reconstruct [IsAdicComplete I R] (f : Family R I G ι) :
145     reduceFamily I (reconstruct I f) = f := by
146   apply family_ext
147   funext k
148   exact reconstruct_reduces I f k
149 
150 /-- Complete inverse-limit equivalence of actual matrix representations. -/
151 noncomputable def representationEquiv [IsAdicComplete I R] :
152     MatrixRep R G ι ≃ Family R I G ι where
153   toFun := reduceFamily I
154   invFun := reconstruct I
155   left_inv := reconstruct_reduce I
156   right_inv := reduce_reconstruct I
157 
158 /-- The reconstructed matrices really are invertible, with inverse given by g^-1. -/
159 theorem reconstructed_inverse [IsAdicComplete I R] (f : Family R I G ι) (g : G) :
160     reconstruct I f g * reconstruct I f g⁻¹ = 1 ∧
161       reconstruct I f g⁻¹ * reconstruct I f g = 1 := by
162   constructor <;> simp [← map_mul]
163 
164 noncomputable def unitRepresentation [IsAdicComplete I R] (f : Family R I G ι) :
165     G →* (Matrix ι ι R)ˣ := (reconstruct I f).toHomUnits
166 
167 /-- Conversion to the ordinary representation on the finite free module. -/
168 noncomputable def linearRepresentation [IsAdicComplete I R] (f : Family R I G ι) :
169     Representation R G (ι → R) :=
170   Matrix.toLinAlgEquiv'.toAlgHom.toMonoidHom.comp (reconstruct I f)
171 
172 /-- Characteristic polynomials, not only traces, commute with finite reduction. -/
173 theorem charpoly_reduces [IsAdicComplete I R] (f : Family R I G ι) (g : G) (k : ℕ) :
174     Polynomial.map (Ideal.Quotient.mk (I^k)) (reconstruct I f g).charpoly =
175       (f.maps k g).charpoly := by
176   rw [← Matrix.charpoly_map]
177   change ((liftMatrix I f g).map _).charpoly = _
178   rw [liftMatrix_reduces]
179 
180 /-- All prescribed integral characteristic-polynomial coefficients survive the limit. -/
181 theorem charpoly_of_all_reductions [IsAdicComplete I R] (f : Family R I G ι)
182     (g : G) (P : Polynomial R)
183     (h : ∀ k, (f.maps k g).charpoly = P.map (Ideal.Quotient.mk (I^k))) :
184     (reconstruct I f g).charpoly = P := by
185   apply Polynomial.ext
186   intro n
187   apply scalar_ext I
188   intro k
189   have H := congrArg (fun p : Polynomial (R ⧸ I^k) => p.coeff n)
190     ((charpoly_reduces I f g k).trans (h k))
191   simpa using H
192 
193 end PaperX.RepresentationLimits

Back to source controls