AdicMatrixGroups.lean

1 import PaperXII.InverseLimitRepresentations
2 import PaperX.RepresentationTopology
3 import Mathlib.Topology.Algebra.Group.Matrix
4 
5 /-! The actual adic matrix-group comparison for the reconstruction part of 10.5.
6 Precision n means R / I^n; precision zero is the trivial quotient, and the
7 first residual quotient occurs at precision one. -/
8 set_option autoImplicit false
9 namespace PaperXII.AdicMatrixGroups
10 
11 open ContinuousMonoidHom Matrix
12 
13 variable {R : Type} [CommRing R] (I : Ideal R)
14 variable {ι : Type} [Fintype ι] [DecidableEq ι]
15 
16 /-- The literal ideal-power quotient, with a dedicated name to specify its discrete topology. -/
17 def Coeff (n : ℕ) := R ⧸ I ^ n
18 
19 instance coeffCommRing (n : ℕ) : CommRing (Coeff I n) :=
20   inferInstanceAs (CommRing (R ⧸ I ^ n))
21 
22 instance coeffTopologicalSpace (n : ℕ) : TopologicalSpace (Coeff I n) := ⊥
23 
24 instance coeffDiscreteTopology (n : ℕ) : DiscreteTopology (Coeff I n) := ⟨rfl⟩
25 
26 /-- The actual quotient homomorphism. -/
27 def quotientMap (n : ℕ) : R →+* Coeff I n := Ideal.Quotient.mk (I ^ n)
28 
29 /-- Adjacent reduction on coefficient rings. -/
30 def coefficientStep (n : ℕ) : Coeff I (n + 1) →+* Coeff I n :=
31   Ideal.Quotient.factorPow I (Nat.le_succ n)
32 
33 /-- Adjacent reduction on actual general linear groups, with its discrete continuity proof. -/
34 def step (n : ℕ) : GL ι (Coeff I (n + 1)) →ₜ* GL ι (Coeff I n) where
35   __ := GeneralLinearGroup.map (coefficientStep I n)
36   continuous_toFun := continuous_of_discreteTopology.generalLinearGroup_map
37 
38 /-- The previously defined compatible-tuple inverse-limit group for the quotient matrix groups. -/
39 def Limit : Subgroup (∀ n, GL ι (Coeff I n)) :=
40   InverseLimitRepresentations.limit (step (ι := ι) I)
41 
42 /-- Reduction of an integral invertible matrix to one finite precision. -/
43 def reduce (n : ℕ) : GL ι R →* GL ι (Coeff I n) :=
44   GeneralLinearGroup.map (quotientMap I n)
45 
46 /-- The canonical homomorphism from GL over the coefficient ring to the limit. -/
47 def toLimit : GL ι R →* Limit (ι := ι) I where
48   toFun A := ⟨fun n ↦ reduce I n A, fun n ↦ by
49     apply Units.ext
50     ext i j
51     exact rfl⟩
52   map_one' := by apply Subtype.ext; funext n; exact map_one (reduce I n)
53   map_mul' A B := by apply Subtype.ext; funext n; exact map_mul (reduce I n) A B
54 
55 /-- Coordinates of the limit form an actual compatible matrix representation of the limit group. -/
56 def coordinateFamily : PaperX.RepresentationLimits.Family R I (Limit (ι := ι) I) ι where
57   maps n :=
58     { toFun g := (g.val n).val
59       map_one' := rfl
60       map_mul' _ _ := rfl }
61   compatible := by
62     intro j k hjk
63     ext g a b
64     apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
65       (fun _ _ h ↦ Ideal.pow_le_pow_right h)
66       (fun n ↦ (g.val n).val a b) ?_ hjk).symm
67     intro n
68     exact (congrArg (fun A : GL ι (Coeff I n) ↦ A.val a b) (g.property n)).symm
69 
70 /-- Lift the coordinate representation entrywise, including its inverses. -/
71 noncomputable def lift [IsAdicComplete I R] : Limit (ι := ι) I →* GL ι R :=
72   PaperX.RepresentationLimits.unitRepresentation I (coordinateFamily I)
73 
74 /-- Every reduction of the lifted matrix is the prescribed matrix. -/
75 theorem reduce_lift [IsAdicComplete I R] (g : Limit (ι := ι) I) (n : ℕ) :
76     reduce I n (lift I g) = g.val n := by
77   apply Units.ext
78   exact congrArg (fun ρ ↦ ρ g)
79     (PaperX.RepresentationLimits.reconstruct_reduces I (coordinateFamily I) n)
80 
81 /-- Separatedness detects equality of invertible matrices at all precisions. -/
82 theorem ext_of_reductions [IsHausdorff I R] {A B : GL ι R}
83     (h : ∀ n, reduce I n A = reduce I n B) : A = B := by
84   apply Units.ext
85   apply PaperX.RepresentationLimits.matrix_ext I
86   intro n
87   exact congrArg Units.val (h n)
88 
89 /-- Reducing after lifting returns the original tuple. -/
90 theorem toLimit_lift [IsAdicComplete I R] (g : Limit (ι := ι) I) :
91     toLimit I (lift I g) = g := by
92   apply Subtype.ext
93   funext n
94   exact reduce_lift I g n
95 
96 /-- Lifting the reductions returns the original integral matrix. -/
97 theorem lift_toLimit [IsAdicComplete I R] (A : GL ι R) :
98     lift I (toLimit I A) = A := by
99   apply ext_of_reductions I
100   intro n
101   exact reduce_lift I (toLimit I A) n
102 
103 /-- The matrix-group isomorphism is proved from adic completeness. -/
104 noncomputable def groupEquiv [IsAdicComplete I R] : GL ι R ≃* Limit (ι := ι) I where
105   toFun := toLimit I
106   invFun := lift I
107   left_inv := lift_toLimit I
108   right_inv := toLimit_lift I
109   map_mul' := (toLimit I).map_mul
110 
111 /-- Coordinate matrix representations are continuous into the discrete finite-precision rings. -/
112 theorem coordinateFamily_continuous (n : ℕ) :
113     PaperX.RepresentationTopology.FiniteRepContinuous ((coordinateFamily (ι := ι) I).maps n) := by
114   intro i j
115   apply (PaperX.RepresentationTopology.finiteContinuous_iff _).mpr
116   have hn : Continuous (fun g : Limit (ι := ι) I ↦ g.val n) :=
117     (continuous_apply n).comp continuous_subtype_val
118   have hm : Continuous (fun g : Limit (ι := ι) I ↦ (g.val n).val) :=
119     Units.continuous_val.comp hn
120   exact (continuous_apply j).comp ((continuous_apply i).comp hm)
121 
122 /-- The lifting homomorphism is continuous for the actual I-adic topology on R. -/
123 theorem lift_continuous [IsAdicComplete I R] :
124     let _ : TopologicalSpace R := I.adicTopology
125     Continuous (lift (ι := ι) I) := by
126   let _ : TopologicalSpace R := I.adicTopology
127   have hc := PaperX.RepresentationTopology.reconstructed_continuous I
128     (coordinateFamily (ι := ι) I) (coordinateFamily_continuous I)
129   apply Units.continuous_iff.mpr
130   constructor
131   · exact hc
132   · exact hc.comp continuous_inv
133 
134 /-- Reduction is continuous from the adic coefficient topology to the discrete quotient. -/
135 theorem quotientMap_continuous (n : ℕ) :
136     let _ : TopologicalSpace R := I.adicTopology
137     Continuous (quotientMap I n) := by
138   let _ : TopologicalSpace R := I.adicTopology
139   exact (PaperX.RepresentationTopology.finiteContinuous_iff _).mp
140     (PaperX.RepresentationTopology.reductions_of_continuous I (fun x : R ↦ x)
141       continuous_id n)
142 
143 /-- The canonical homomorphism to the inverse limit is continuous. -/
144 theorem toLimit_continuous :
145     let _ : TopologicalSpace R := I.adicTopology
146     Continuous (toLimit (ι := ι) I) := by
147   let _ : TopologicalSpace R := I.adicTopology
148   apply Continuous.subtype_mk
149   apply continuous_pi
150   intro n
151   exact (quotientMap_continuous I n).generalLinearGroup_map
152 
153 /-- The proved group isomorphism is also a homeomorphism. -/
154 noncomputable def homeomorph [IsAdicComplete I R] :
155     let _ : TopologicalSpace R := I.adicTopology
156     GL ι R ≃ₜ Limit (ι := ι) I := by
157   let _ : TopologicalSpace R := I.adicTopology
158   exact
159     { toEquiv := (groupEquiv I).toEquiv
160       continuous_toFun := toLimit_continuous I
161       continuous_invFun := lift_continuous I }
162 
163 end PaperXII.AdicMatrixGroups

Back to source controls