ActualELatticeQuotient59.lean

1 import PaperXI.ActualELatticeTypeGroup59
2 import PaperXI.ProductNormalizerQuotient59
3 
4 /-!
5 # Finite residue quotient of the literal extension-field lattice product
6 
7 For the actual subgroup `GL_n(O_E) U^1` in `Aut_K(E^n)`, the quotient by
8 literal adjacent-lattice congruence is `GL_n(k_E)`. Conjugation by the
9 extension-field uniformizer is the identity on this quotient.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualELatticeQuotient59
14 open Matrix ValuativeRel
15 open ActualELatticeNormalizer59 ActualELatticeResidue59 ActualELatticeTypeGroup59
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 /-- The literal congruence subgroup inside the actual product group. -/
22 def typeCongruence : Subgroup (typeGroup K E n) :=
23   (congruence K E n).subgroupOf (typeGroup K E n)
24 
25 instance typeCongruence_normal : (typeCongruence K E n).Normal :=
26   Subgroup.normal_subgroupOf_sup_of_le_normalizer (integralImage_normalizes K E n)
27 
28 /-- The entire actual quotient is the full residue general linear group. -/
29 def residueEquiv : typeGroup K E n ⧸ typeCongruence K E n ≃*
30     GeneralLinearGroup n 𝓀[E] :=
31   ProductNormalizerQuotient59.quotientEquivOfKernel
32     (integralImage K E n) (congruence K E n) (integralImage_normalizes K E n)
33     (residueAction K E n) (residueAction_surjective K E n)
34     (congruence_subgroupOf_integralImage K E n)
35 
36 /-- The actual surjective reduction map on the product group. -/
37 def reduction : typeGroup K E n →* GeneralLinearGroup n 𝓀[E] :=
38   (residueEquiv K E n).toMonoidHom.comp (QuotientGroup.mk' (typeCongruence K E n))
39 
40 theorem reduction_surjective : Function.Surjective (reduction K E n) :=
41   (residueEquiv K E n).surjective.comp (QuotientGroup.mk'_surjective _)
42 
43 @[simp] theorem reduction_kernel : (reduction K E n).ker = typeCongruence K E n := by
44   ext j
45   change residueEquiv K E n (QuotientGroup.mk' (typeCongruence K E n) j) = 1 ↔ _
46   rw [← (residueEquiv K E n).map_one, (residueEquiv K E n).injective.eq_iff]
47   exact QuotientGroup.eq_one_iff j
48 
49 /-- Finiteness is inherited from the actual finite residue field. -/
50 theorem finite_quotient : Finite (typeGroup K E n ⧸ typeCongruence K E n) :=
51   Finite.of_equiv (GeneralLinearGroup n 𝓀[E]) (residueEquiv K E n).symm.toEquiv
52 
53 /-- Scalar multiplication by the extension uniformizer centralizes the first factor. -/
54 theorem uniformizer_centralizes (g : ((n → E) ≃ₗ[K] (n → E)))
55     (hg : g ∈ integralImage K E n) :
56     uniformizerAction K E n * g = g * uniformizerAction K E n := by
57   obtain ⟨h, rfl⟩ := hg
58   exact (integralMatrix_commute K E n h).eq.symm
59 
60 omit [Fintype n] [DecidableEq n] in
61 /-- The actual uniformizer normalizes the full adjacent-lattice congruence group. -/
62 theorem uniformizer_normalizes_congruence : uniformizerAction K E n ∈
63     Subgroup.normalizer (congruence K E n : Set ((n → E) ≃ₗ[K] (n → E))) := by
64   simpa [congruence, latticeChain] using power_normalizes_firstCongruence (uniformizerAction K E n)
65     (integralLattice E n) 1
66 
67 /-- It therefore normalizes the literal lattice-product group. -/
68 theorem uniformizer_normalizes : uniformizerAction K E n ∈
69     Subgroup.normalizer (typeGroup K E n : Set ((n → E) ≃ₗ[K] (n → E))) :=
70   ProductNormalizerQuotient59.normalizes_sup
71     (integralImage K E n) (congruence K E n) (uniformizerAction K E n)
72     (uniformizer_centralizes K E n) (uniformizer_normalizes_congruence K E n)
73 
74 /-- Literal conjugation on the actual type group. -/
75 def uniformizerConjugation : MulAut (typeGroup K E n) :=
76   ProductNormalizerQuotient59.conjugation
77     (integralImage K E n) (congruence K E n) (uniformizerAction K E n)
78     (uniformizer_centralizes K E n) (uniformizer_normalizes_congruence K E n)
79 
80 /-- The actual residue matrix is unchanged by uniformizer conjugation. -/
81 theorem reduction_conjugation (j : typeGroup K E n) :
82     reduction K E n (uniformizerConjugation K E n j) = reduction K E n j := by
83   apply ProductNormalizerQuotient59.map_conjugation
84     (integralImage K E n) (congruence K E n) (uniformizerAction K E n)
85     (uniformizer_centralizes K E n) (uniformizer_normalizes_congruence K E n)
86     (integralImage_normalizes K E n) (reduction K E n)
87   exact (reduction_kernel K E n).ge
88 
89 end PaperXI.ActualELatticeQuotient59

Back to source controls