ActualELatticeTypeGroup59.lean

1 import PaperXI.ActualELatticeNormalizer59
2 import PaperXI.ActualELatticeResidue59
3 
4 /-!
5 # The actual lattice-product type group
6 
7 The lattice and its first congruence subgroup are literal subgroups of
8 `Aut_K(E^n)`. The centralizer integral matrices normalize congruence, and their
9 intersection with congruence is exactly their residue kernel.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualELatticeTypeGroup59
14 open Matrix ValuativeRel
15 open ActualELatticeNormalizer59 ActualELatticeResidue59
16 
17 variable (K E : Type*) [Field K] [Field E] [Algebra K E]
18 variable (n : Type*) [Fintype n] [DecidableEq n]
19 variable [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
20 
21 /-- Actual multiplication by the chosen extension-field uniformizer. -/
22 def uniformizerAction : (n → E) ≃ₗ[K] (n → E) :=
23   (LinearEquiv.smulOfNeZero E (n → E) (ActualLocalUnitDecomposition.uniformizer E : E)
24     (ActualLocalUnitDecomposition.uniformizer_ne_zero E)).restrictScalars K
25 
26 omit [Fintype n] [DecidableEq n] in
27 @[simp] theorem uniformizerAction_apply (v : n → E) :
28     uniformizerAction K E n v = (ActualLocalUnitDecomposition.uniformizer E : E) • v := rfl
29 
30 /-- Every level is an actual scalar translate of the integral lattice. -/
31 def latticeChain : ℤ → AddSubgroup (n → E) :=
32   periodicChain (uniformizerAction K E n) (integralLattice E n)
33 
34 omit [Fintype n] [DecidableEq n] in
35 @[simp] theorem latticeChain_zero : latticeChain K E n 0 = integralLattice E n := by
36   ext v
37   simp [latticeChain, periodicChain]
38 
39 omit [Fintype n] [DecidableEq n] in
40 @[simp] theorem latticeChain_one : latticeChain K E n 1 = nextLattice E n := by
41   ext v
42   change (uniformizerAction K E n ^ (-(1 : ℤ))) v ∈ integralLattice E n ↔ _
43   rw [zpow_neg_one, mem_nextLattice]
44   constructor
45   · intro hv
46     exact ⟨(uniformizerAction K E n)⁻¹ v, hv,
47       (uniformizerAction K E n).apply_symm_apply v⟩
48   · rintro ⟨w, hw, he⟩
49     change uniformizerAction K E n w = v at he
50     rw [← he]
51     change (uniformizerAction K E n).symm (uniformizerAction K E n w) ∈ _
52     rwa [LinearEquiv.symm_apply_apply]
53 
54 omit [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
55 /-- Integral extension-linear automorphisms preserve the integral lattice. -/
56 theorem integralMatrix_preserves_iff (g : GeneralLinearGroup n 𝒪[E]) (v : n → E) :
57     integralMatrix K E n g v ∈ integralLattice E n ↔ v ∈ integralLattice E n := by
58   constructor
59   · intro hv
60     have h := integralMatrix_preserves K E n g⁻¹ _ hv
61     simpa [← LinearEquiv.mul_apply, ← map_mul] using h
62   · exact integralMatrix_preserves K E n g v
63 
64 /-- The field uniformizer centralizes the literal extension-linear matrices. -/
65 theorem integralMatrix_commute (g : GeneralLinearGroup n 𝒪[E]) :
66     Commute (integralMatrix K E n g) (uniformizerAction K E n) := by
67   apply LinearEquiv.ext
68   intro v
69   change ((GeneralLinearGroup.toLin (ActualIntegralGeneralLinear.embedding E n g)).toLinearEquiv)
70       ((ActualLocalUnitDecomposition.uniformizer E : E) • v) = _
71   exact map_smul _ _ _
72 
73 /-- Hence integral extension-linear matrices preserve every chain level. -/
74 theorem integralMatrix_mem_stabilizer (g : GeneralLinearGroup n 𝒪[E]) :
75     integralMatrix K E n g ∈ chainStabilizer (latticeChain K E n) := by
76   intro i v
77   change (uniformizerAction K E n ^ (-i)) (integralMatrix K E n g v) ∈ integralLattice E n ↔ _
78   have hc := (integralMatrix_commute K E n g).zpow_right (-i)
79   rw [← LinearEquiv.mul_apply, ← hc.eq, LinearEquiv.mul_apply]
80   exact integralMatrix_preserves_iff K E n g _
81 
82 /-- The literal adjacent-lattice congruence group in `Aut_K(E^n)`. -/
83 def congruence : Subgroup ((n → E) ≃ₗ[K] (n → E)) :=
84   firstCongruence (latticeChain K E n)
85 
86 /-- Integral extension-linear matrices normalize the actual congruence group. -/
87 theorem integralImage_normalizes : integralImage K E n ≤
88     Subgroup.normalizer (congruence K E n : Set ((n → E) ≃ₗ[K] (n → E))) := by
89   rintro g ⟨h, rfl⟩
90   exact stabilizer_normalizes_firstCongruence (latticeChain K E n)
91     (integralMatrix_mem_stabilizer K E n h)
92 
93 /-- First congruence for an extension-linear matrix is exactly residue identity. -/
94 theorem integralMatrix_mem_congruence_iff (g : GeneralLinearGroup n 𝒪[E]) :
95     integralMatrix K E n g ∈ congruence K E n ↔
96       g ∈ (ActualResidueGeneralLinear.reduction E n).ker := by
97   rw [reduction_kernel_iff K E n]
98   constructor
99   · intro hg v hv
100     have h := hg.2 0 v (by simpa using hv)
101     simpa using h
102   · intro hg
103     refine ⟨integralMatrix_mem_stabilizer K E n g, ?_⟩
104     intro i v hv
105     have hi : (uniformizerAction K E n ^ (-i)) v ∈ integralLattice E n := hv
106     have h := hg _ hi
107     have hc := (integralMatrix_commute K E n g).zpow_right (-i)
108     have he : integralMatrix K E n g ((uniformizerAction K E n ^ (-i)) v) -
109         (uniformizerAction K E n ^ (-i)) v =
110         (uniformizerAction K E n ^ (-i)) (integralMatrix K E n g v - v) := by
111       rw [map_sub, ← LinearEquiv.mul_apply, hc.eq, LinearEquiv.mul_apply]
112     rw [he, ← latticeChain_one K E n] at h
113     have ht := (periodicChain_shift (uniformizerAction K E n) (integralLattice E n)
114       i 1 ((uniformizerAction K E n ^ (-i)) (integralMatrix K E n g v - v))).mpr h
115     have hcancel : (uniformizerAction K E n ^ i)
116         ((uniformizerAction K E n ^ (-i)) (integralMatrix K E n g v - v)) =
117         integralMatrix K E n g v - v := by
118       rw [← LinearEquiv.mul_apply, ← zpow_add, add_neg_cancel, zpow_zero]
119       rfl
120     rw [hcancel] at ht
121     simpa only [latticeChain, add_comm 1 i] using ht
122 
123 /-- On the literal integral image, the congruence intersection is the residue kernel. -/
124 theorem congruence_subgroupOf_integralImage :
125     (congruence K E n).subgroupOf (integralImage K E n) = (residueAction K E n).ker := by
126   ext g
127   obtain ⟨h, rfl⟩ := (integralImageEquiv K E n).surjective g
128   change integralMatrix K E n h ∈ congruence K E n ↔ _
129   rw [integralMatrix_mem_congruence_iff]
130   simp [residueAction]
131 
132 /-- The actual centralizer-integral-times-congruence subgroup. -/
133 def typeGroup : Subgroup ((n → E) ≃ₗ[K] (n → E)) :=
134   integralImage K E n ⊔ congruence K E n
135 
136 end PaperXI.ActualELatticeTypeGroup59

Back to source controls