ActualELatticeResidue59.lean

1 import PaperXI.ActualIntegralGeneralLinear
2 import PaperXI.ActualLocalUnitDecomposition
3 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
4 
5 /-!
6 # Literal residue action on an extension-field lattice
7 
8 The group and the congruence kernel below are the actual integral matrices on
9 `E^n`, viewed as `K`-linear operators. The next lattice is multiplication of the
10 integral lattice by the chosen actual uniformizer.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.ActualELatticeResidue59
15 open Matrix ValuativeRel
16 
17 variable (K E : Type*) [Field K] [Field E] [Algebra K E]
18 variable (n : Type*) [Fintype n] [DecidableEq n]
19 
20 def restrictScalarMatrix : GeneralLinearGroup n E →* ((n → E) ≃ₗ[K] (n → E)) where
21   toFun g := (GeneralLinearGroup.toLin g).toLinearEquiv.restrictScalars K
22   map_one' := by ext v i; simp
23   map_mul' g h := by ext v i; simp
24 
25 @[simp] theorem restrictScalarMatrix_apply (g : GeneralLinearGroup n E) (v : n → E) :
26     restrictScalarMatrix K E n g v = (g : Matrix n n E) *ᵥ v := rfl
27 
28 theorem restrictScalarMatrix_injective : Function.Injective (restrictScalarMatrix K E n) := by
29   intro g h he
30   apply GeneralLinearGroup.ext
31   intro i j
32   have hv := congrArg (fun f : ((n → E) ≃ₗ[K] (n → E)) => f (Pi.single j 1) i) he
33   simpa [Matrix.mulVec, dotProduct, Pi.single_apply] using hv
34 
35 variable [ValuativeRel E]
36 
37 def integralMatrix : GeneralLinearGroup n 𝒪[E] →* ((n → E) ≃ₗ[K] (n → E)) :=
38   (restrictScalarMatrix K E n).comp (ActualIntegralGeneralLinear.embedding E n)
39 
40 theorem integralMatrix_injective : Function.Injective (integralMatrix K E n) :=
41   (restrictScalarMatrix_injective K E n).comp
42     (ActualIntegralGeneralLinear.embedding_injective E n)
43 
44 def integralLattice : AddSubgroup (n → E) where
45   carrier := {v | ∀ i, v i ∈ (valuation E).integer}
46   zero_mem' := by intro i; exact (valuation E).integer.zero_mem
47   add_mem' := by intro v w hv hw i; exact (valuation E).integer.add_mem (hv i) (hw i)
48   neg_mem' := by intro v hv i; exact (valuation E).integer.neg_mem (hv i)
49 
50 omit [Fintype n] [DecidableEq n] in
51 @[simp] theorem mem_integralLattice (v : n → E) :
52     v ∈ integralLattice E n ↔ ∀ i, v i ∈ (valuation E).integer := Iff.rfl
53 
54 omit [Algebra K E] [Fintype n] [DecidableEq n] in
55 theorem integralLattice_coe (v : n → 𝒪[E]) :
56     (fun i => (v i : E)) ∈ integralLattice E n := fun i => (v i).property
57 
58 @[simp] theorem integralMatrix_coe (g : GeneralLinearGroup n 𝒪[E]) (v : n → 𝒪[E]) :
59     integralMatrix K E n g (fun i => (v i : E)) =
60       fun i => (((g : Matrix n n 𝒪[E]) *ᵥ v) i : E) := by
61   ext i
62   simp [integralMatrix, Matrix.mulVec, dotProduct]
63 
64 theorem integralMatrix_preserves (g : GeneralLinearGroup n 𝒪[E]) (v : n → E)
65     (hv : v ∈ integralLattice E n) : integralMatrix K E n g v ∈ integralLattice E n := by
66   let w : n → 𝒪[E] := fun i => ⟨v i, hv i⟩
67   change integralMatrix K E n g (fun i => (w i : E)) ∈ integralLattice E n
68   rw [integralMatrix_coe]
69   exact integralLattice_coe E n _
70 
71 variable [TopologicalSpace E] [IsNonarchimedeanLocalField E]
72 
73 /-- The actual next lattice is multiplication by the chosen `E`-uniformizer. -/
74 def nextLattice : AddSubgroup (n → E) :=
75   (integralLattice E n).map
76     ((ActualLocalUnitDecomposition.uniformizer E : E) • (LinearMap.id : (n → E) →ₗ[E] (n → E))).toAddMonoidHom
77 
78 omit [Fintype n] [DecidableEq n] in
79 @[simp] theorem mem_nextLattice (v : n → E) :
80     v ∈ nextLattice E n ↔ ∃ w ∈ integralLattice E n,
81       (ActualLocalUnitDecomposition.uniformizer E : E) • w = v := Iff.rfl
82 
83 omit [Algebra K E] [Fintype n] [DecidableEq n] in
84 theorem coe_mem_nextLattice_iff (v : n → 𝒪[E]) :
85     (fun i => (v i : E)) ∈ nextLattice E n ↔
86       ∀ i, v i ∈ IsLocalRing.maximalIdeal 𝒪[E] := by
87   classical
88   rw [mem_nextLattice]
89   have hπ := (IsDiscreteValuationRing.irreducible_iff_uniformizer
90     (ActualLocalUnitDecomposition.uniformizer E)).mp
91       (ActualLocalUnitDecomposition.uniformizer_irreducible E)
92   constructor
93   · rintro ⟨w, hw, he⟩ i
94     rw [hπ, Ideal.mem_span_singleton]
95     refine ⟨⟨w i, hw i⟩, ?_⟩
96     apply Subtype.ext
97     exact (congrFun he i).symm
98   · intro hv
99     have hd : ∀ i, ∃ w : 𝒪[E], v i = ActualLocalUnitDecomposition.uniformizer E * w := by
100       intro i
101       have hi := hv i
102       rw [hπ, Ideal.mem_span_singleton] at hi
103       obtain ⟨w, hw⟩ := hi
104       exact ⟨w, hw⟩
105     choose w hw using hd
106     refine ⟨fun i => (w i : E), integralLattice_coe E n w, ?_⟩
107     ext i
108     exact congrArg (fun x : 𝒪[E] => (x : E)) (hw i).symm
109 
110 /-- Congruence on the actual lattice is exactly entrywise residue reduction. -/
111 theorem reduction_kernel_iff (g : GeneralLinearGroup n 𝒪[E]) :
112     g ∈ (ActualResidueGeneralLinear.reduction E n).ker ↔
113       ∀ v ∈ integralLattice E n,
114         integralMatrix K E n g v - v ∈ nextLattice E n := by
115   classical
116   rw [ActualIntegralGeneralLinear.mem_reduction_kernel]
117   constructor
118   · intro hg v hv
119     let w : n → 𝒪[E] := fun i => ⟨v i, hv i⟩
120     change integralMatrix K E n g (fun i => (w i : E)) - (fun i => (w i : E)) ∈ _
121     rw [integralMatrix_coe]
122     change (fun i => ((((g : Matrix n n 𝒪[E]) *ᵥ w - w) i) : E)) ∈ _
123     rw [coe_mem_nextLattice_iff]
124     intro i
125     have he : ((g : Matrix n n 𝒪[E]) *ᵥ w - w) i =
126         ∑ j, (g i j - (1 : Matrix n n 𝒪[E]) i j) * w j := by
127       simp [Matrix.mulVec, dotProduct, sub_mul, Finset.sum_sub_distrib, Matrix.one_apply]
128     rw [he]
129     exact Ideal.sum_mem _ fun j _ => Ideal.mul_mem_right _ _ (hg i j)
130   · intro hg i j
131     let w : n → 𝒪[E] := Pi.single j 1
132     have hv := hg (fun i => (w i : E)) (integralLattice_coe E n w)
133     rw [integralMatrix_coe] at hv
134     change (fun i => ((((g : Matrix n n 𝒪[E]) *ᵥ w - w) i) : E)) ∈ _ at hv
135     rw [coe_mem_nextLattice_iff] at hv
136     simpa [w, Matrix.mulVec, dotProduct, Matrix.one_apply, Pi.single_apply, eq_comm] using hv i
137 
138 /-- The concrete integral matrix image among `K`-linear automorphisms. -/
139 def integralImage : Subgroup ((n → E) ≃ₗ[K] (n → E)) := (integralMatrix K E n).range
140 
141 def integralImageEquiv : GeneralLinearGroup n 𝒪[E] ≃* integralImage K E n :=
142   MonoidHom.ofInjective (integralMatrix_injective K E n)
143 
144 def residueAction : integralImage K E n →* GeneralLinearGroup n 𝓀[E] :=
145   (ActualResidueGeneralLinear.reduction E n).comp (integralImageEquiv K E n).symm.toMonoidHom
146 
147 theorem residueAction_surjective : Function.Surjective (residueAction K E n) :=
148   (ActualResidueGeneralLinear.reduction_surjective E n).comp
149     (integralImageEquiv K E n).symm.surjective
150 
151 /-- The literal finite residue group of this actual extension-field lattice. -/
152 def residueQuotientEquiv :
153     integralImage K E n ⧸ (residueAction K E n).ker ≃* GeneralLinearGroup n 𝓀[E] :=
154   QuotientGroup.quotientKerEquivOfSurjective (residueAction K E n)
155     (residueAction_surjective K E n)
156 
157 end PaperXI.ActualELatticeResidue59

Back to source controls