ActualResidueGeneralLinear.lean

1 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
2 import Mathlib.NumberTheory.LocalField.Basic
3 
4 /-! Entrywise reduction of actual integral general linear groups.
5 
6 The lifting argument works over any commutative local ring: lift each entry,
7 then use the nonzero reduced determinant to prove that the lifted determinant
8 is a unit. The final declarations specialize this to the given nonarchimedean
9 local field's own ring of integers and finite residue field.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualResidueGeneralLinear
14 open Matrix ValuativeRel
15 
16 section LocalRing
17 variable (n : Type*) [Fintype n] [DecidableEq n]
18 variable (R : Type*) [CommRing R] [IsLocalRing R]
19 
20 /-- Entrywise reduction from a local ring to its residue field. -/
21 def residueMap : GeneralLinearGroup n R →*
22     GeneralLinearGroup n (IsLocalRing.ResidueField R) :=
23   GeneralLinearGroup.map (IsLocalRing.residue R)
24 
25 @[simp] theorem residueMap_apply (g : GeneralLinearGroup n R) (i j : n) :
26     residueMap n R g i j = IsLocalRing.residue R (g i j) := rfl
27 
28 /-- Lift all entries of an invertible residue matrix. Its determinant lifts to
29 an element outside the maximal ideal, hence is a unit. -/
30 theorem residueMap_surjective : Function.Surjective (residueMap n R) := by
31   intro g
32   choose s hs using (IsLocalRing.residue_surjective (R := R))
33   let A : Matrix n n R := fun i j => s (g i j)
34   have hA : A.map (IsLocalRing.residue R) = (g : Matrix n n _) := by
35     ext i j
36     exact hs (g i j)
37   have hdet : IsUnit A.det := by
38     apply (IsLocalRing.residue_ne_zero_iff_isUnit A.det).mp
39     rw [RingHom.map_det, RingHom.mapMatrix_apply, hA]
40     exact GeneralLinearGroup.det_ne_zero g
41   refine ⟨GeneralLinearGroup.mk'' A hdet, ?_⟩
42   apply GeneralLinearGroup.ext
43   intro i j
44   exact hs (g i j)
45 end LocalRing
46 
47 section ActualField
48 variable (K : Type*) [Field K] [ValuativeRel K]
49 variable (n : Type*) [Fintype n] [DecidableEq n]
50 
51 /-- The actual residue map of the given valued field's integral matrix group. -/
52 def reduction : GeneralLinearGroup n 𝒪[K] →* GeneralLinearGroup n 𝓀[K] :=
53   residueMap n 𝒪[K]
54 
55 @[simp] theorem reduction_apply (g : GeneralLinearGroup n 𝒪[K]) (i j : n) :
56     reduction K n g i j = IsLocalRing.residue 𝒪[K] (g i j) := rfl
57 
58 /-- Every invertible matrix over the actual residue field has an integral lift. -/
59 theorem reduction_surjective : Function.Surjective (reduction K n) :=
60   residueMap_surjective n 𝒪[K]
61 
62 variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
63 
64 /-- Finiteness of the actual target follows from the local-field hypotheses. -/
65 theorem finite_reduction_target : Finite (GeneralLinearGroup n 𝓀[K]) :=
66   inferInstance
67 end ActualField
68 
69 end PaperXI.ActualResidueGeneralLinear

Back to source controls