ActualELatticeTopology60.lean

1 import PaperXI.LatticeCongruenceTopology60
2 import PaperXI.ActualELatticeScalarPeriod60
3 
4 /-!
5 # Compact open topology for the literal extension-field lattice type group
6 
7 The exact Block59 lattice groups are realized in actual `GL_d(K)` through
8 finite continuous coordinates on `E^n`. Compactness, openness, and the open
9 kernel of actual residue reduction are proved. No identification with the
10 simple-character group of an arbitrary stratum is asserted.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.ActualELatticeTopology60
15 open Matrix ValuativeRel Topology
16 open ActualELatticeResidue59 ActualELatticeTypeGroup59 ActualELatticeNormalizer59
17 open ActualELatticeFreeness59 ActualELatticeQuotient59 ActualELatticeScalarPeriod60
18 open LatticeMatrixTopology60 LatticeCongruenceTopology60
19 
20 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
21   [IsNonarchimedeanLocalField K] [Field E] [ValuativeRel E] [TopologicalSpace E]
22   [IsNonarchimedeanLocalField E] [Algebra K E]
23 variable (n d : Type*) [Fintype n] [DecidableEq n] [Fintype d] [DecidableEq d]
24 
25 local instance : T2Space K := ActualIntegralGeneralLinear.field_t2Space K
26 local instance : T2Space E := ActualIntegralGeneralLinear.field_t2Space E
27 
28 /-- A local field has nontrivial punctured neighborhoods at zero. -/
29 theorem field_nhdsNE_neBot : Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ) := by
30   let := IsTopologicalAddGroup.rightUniformSpace K
31   have := isUniformAddGroup_of_addCommGroup (G := K)
32   let : (Valued.v (R := K)).RankOne :=
33     { hom' := ValuativeRel.IsRankLeOne.nonempty.some.emb (R := K).comp
34         MonoidWithZeroHom.ValueGroup₀.embedding
35       strictMono' := ValuativeRel.IsRankLeOne.nonempty.some.strictMono.comp
36         MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
37   open scoped Valued in
38     infer_instance
39 
40 /-- Every actual finite basis gives continuous coordinates under the compatible extension topology. -/
41 def coordinatesOfBasis (hK : Continuous (algebraMap K E)) (b : Module.Basis d K (n → E)) :
42     (n → E) ≃L[K] (d → K) := by
43   let := IsTopologicalAddGroup.rightUniformSpace K
44   have := isUniformAddGroup_of_addCommGroup (G := K)
45   let : (Valued.v (R := K)).RankOne :=
46     { hom' := ValuativeRel.IsRankLeOne.nonempty.some.emb (R := K).comp
47         MonoidWithZeroHom.ValueGroup₀.embedding
48       strictMono' := ValuativeRel.IsRankLeOne.nonempty.some.strictMono.comp
49         MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
50   let : ContinuousSMul K E := continuousSMul_of_algebraMap K E hK
51   let : FiniteDimensional K (n → E) := Module.Finite.of_basis b
52   open scoped Valued in
53     exact b.equivFun.toContinuousLinearEquiv
54 
55 /-- Scalar multiplication gives a literal algebra embedding into actual matrices. -/
56 def scalarMatrixEmbedding (e : (n → E) ≃L[K] (d → K)) : E →ₐ[K] Matrix d d K :=
57   LinearMap.toMatrixAlgEquiv'.toAlgHom.comp
58     ((e.toLinearEquiv.conjAlgEquiv K).toAlgHom.comp (Algebra.lsmul K K (n → E)))
59 
60 omit [Fintype n] [DecidableEq n] in
61 /-- The literal integral extension-field lattice is compact. -/
62 theorem integralLattice_compact : IsCompact (integralLattice E n : Set (n → E)) :=
63   isCompact_pi_infinite (fun _ => IsNonarchimedeanLocalField.isCompact_closedBall E 1)
64 
65 omit [DecidableEq n] in
66 /-- The literal integral extension-field lattice is open. -/
67 theorem integralLattice_open : IsOpen (integralLattice E n : Set (n → E)) := by
68   change IsOpen {v : n → E | ∀ i, v i ∈ (valuation E).integer}
69   simp only [Set.ofPred_forall]
70   exact isOpen_iInter_of_finite fun i => (valuation E).isOpen_integer.preimage (continuous_apply i)
71 
72 omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Fintype n] [DecidableEq n] in
73 /-- Every integer translate in the actual chain is compact. -/
74 theorem latticeChain_compact (i : ℤ) : IsCompact (latticeChain K E n i : Set (n → E)) := by
75   let a : E := (ActualLocalUnitDecomposition.uniformizer E : E) ^ (-i)
76   have ha : a ≠ 0 := zpow_ne_zero _ (ActualLocalUnitDecomposition.uniformizer_ne_zero E)
77   have h := (Homeomorph.smulOfNeZero a ha : (n → E) ≃ₜ (n → E)).isCompact_preimage.mpr
78     (integralLattice_compact E n)
79   convert h using 1
80   ext v
81   exact Iff.of_eq (congrArg (fun w => w ∈ integralLattice E n)
82     (uniformizerAction_zpow_apply K E n (-i) v))
83 
84 omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [DecidableEq n] in
85 /-- Every integer translate in the actual chain is open. -/
86 theorem latticeChain_open (i : ℤ) : IsOpen (latticeChain K E n i : Set (n → E)) := by
87   have h := (integralLattice_open E n).preimage
88     (continuous_const_smul ((ActualLocalUnitDecomposition.uniformizer E : E) ^ (-i)))
89   convert h using 1
90   ext v
91   exact Iff.of_eq (congrArg (fun w => w ∈ integralLattice E n)
92     (uniformizerAction_zpow_apply K E n (-i) v))
93 
94 /-- The exact Block59 type group in actual finite `K`-matrix coordinates. -/
95 def matrixType (e : (n → E) ≃L[K] (d → K)) : Subgroup (GeneralLinearGroup d K) :=
96   (typeGroup K E n).comap (coordinateAut e).toMonoidHom
97 
98 /-- The exact Block59 first congruence group in the same coordinates. -/
99 def matrixCongruence (e : (n → E) ≃L[K] (d → K)) : Subgroup (GeneralLinearGroup d K) :=
100   LatticeCongruenceTopology60.congruence e (latticeChain K E n)
101 
102 variable [Nonempty d]
103 
104 /-- Openness uses a proved base-field scalar period, not a supplied period or ramification index. -/
105 theorem matrixCongruence_open (e : (n → E) ≃L[K] (d → K))
106     (hK : Continuous (algebraMap K E)) :
107     IsOpen (matrixCongruence K E n d e : Set (GeneralLinearGroup d K)) := by
108   let ι := scalarMatrixEmbedding K E n d e
109   have hι := ActualEmbeddedUniformizer58.algebraEmbedding_continuous K E d ι hK
110   obtain ⟨c, r, hr, hp⟩ := exists_chain_period K E n ι hι
111   exact LatticeCongruenceTopology60.congruence_open e (latticeChain K E n)
112     (latticeChain_compact K E n) (latticeChain_open K E n) c r hr hp
113 
114 /-- The actual type group is open because it contains the proved open first congruence group. -/
115 theorem matrixType_open (e : (n → E) ≃L[K] (d → K))
116     (hK : Continuous (algebraMap K E)) :
117     IsOpen (matrixType K E n d e : Set (GeneralLinearGroup d K)) := by
118   apply Subgroup.isOpen_mono (H₁ := matrixCongruence K E n d e)
119   · intro g hg
120     exact (show ActualELatticeTypeGroup59.congruence K E n ≤ typeGroup K E n from le_sup_right) hg
121   · exact matrixCongruence_open K E n d e hK
122 
123 /-- Compactness follows inside the actual compact integral-lattice stabilizer. -/
124 theorem matrixType_compact (e : (n → E) ≃L[K] (d → K))
125     (hK : Continuous (algebraMap K E)) :
126     IsCompact (matrixType K E n d e : Set (GeneralLinearGroup d K)) := by
127   let : ContinuousSMul K E := continuousSMul_of_algebraMap K E hK
128   let : Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ) := field_nhdsNE_neBot K
129   have hc := stabilizer_compact_of_open e (integralLattice E n)
130     (integralLattice_compact E n) (integralLattice_open E n)
131   apply hc.of_isClosed_subset ((matrixType K E n d e).isClosed_of_isOpen (matrixType_open K E n d e hK))
132   intro g hg
133   apply (mem_stabilizer_iff e (integralLattice E n) g).mpr
134   have h : coordinateAut e g ∈ chainStabilizer (latticeChain K E n) :=
135     typeGroup_le_stabilizer K E n hg
136   simpa only [latticeChain_zero] using h 0
137 
138 /-- The exact first congruence group is compact as a closed subgroup of the compact type group. -/
139 theorem matrixCongruence_compact (e : (n → E) ≃L[K] (d → K))
140     (hK : Continuous (algebraMap K E)) :
141     IsCompact (matrixCongruence K E n d e : Set (GeneralLinearGroup d K)) := by
142   apply (matrixType_compact K E n d e hK).of_isClosed_subset
143     ((matrixCongruence K E n d e).isClosed_of_isOpen (matrixCongruence_open K E n d e hK))
144   intro g hg
145   exact (show ActualELatticeTypeGroup59.congruence K E n ≤ typeGroup K E n from le_sup_right) hg
146 
147 /-- The compact/open result for any actual finite basis, with coordinate continuity derived. -/
148 theorem compact_open_of_basis (hK : Continuous (algebraMap K E))
149     (b : Module.Basis d K (n → E)) :
150     IsCompact (matrixType K E n d (coordinatesOfBasis K E n d hK b) : Set (GeneralLinearGroup d K)) ∧
151     IsOpen (matrixType K E n d (coordinatesOfBasis K E n d hK b) : Set (GeneralLinearGroup d K)) :=
152   ⟨matrixType_compact K E n d _ hK, matrixType_open K E n d _ hK⟩
153 
154 /-- Finite-extension coordinates require no supplied basis or continuity of coordinates. -/
155 def finiteExtensionCoordinates [FiniteDimensional K E] (hK : Continuous (algebraMap K E)) :
156     (n → E) ≃L[K] (Fin (Module.finrank K (n → E)) → K) :=
157   coordinatesOfBasis K E n _ hK (Module.finBasis K (n → E))
158 
159 omit [Fintype d] [DecidableEq d] [Nonempty d] in
160 /-- Every genuine finite continuous extension realizes the literal type group compact openly. -/
161 theorem finiteExtension_compact_open [FiniteDimensional K E] [Nonempty n]
162     (hK : Continuous (algebraMap K E)) :
163     IsCompact (matrixType K E n (Fin (Module.finrank K (n → E)))
164       (finiteExtensionCoordinates K E n hK) : Set (GeneralLinearGroup (Fin (Module.finrank K (n → E))) K)) ∧
165     IsOpen (matrixType K E n (Fin (Module.finrank K (n → E)))
166       (finiteExtensionCoordinates K E n hK) : Set (GeneralLinearGroup (Fin (Module.finrank K (n → E))) K)) := by
167   let : Nonempty (Fin (Module.finrank K (n → E))) := ⟨⟨0, Module.finrank_pos⟩⟩
168   exact ⟨matrixType_compact K E n _ _ hK, matrixType_open K E n _ _ hK⟩
169 
170 end PaperXI.ActualELatticeTopology60

Back to source controls