LatticeMatrixTopology60.lean

1 import PaperXI.ActualELatticeQuotient59
2 import Mathlib.Topology.CompactOpen
3 import Mathlib.Topology.Algebra.Module.FiniteDimension
4 
5 /-!
6 # Compact open lattice stabilizers in actual matrix coordinates
7 
8 A finite continuous basis transports a literal compact open additive lattice
9 into the given local field's matrix group. Compactness uses a basis contained
10 in the lattice. No equality with a simple-character group is asserted.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.LatticeMatrixTopology60
15 open Matrix Topology
16 
17 variable {K V d : Type*} [Field K] [TopologicalSpace K] [IsTopologicalRing K]
18   [T2Space K] [Fintype d] [DecidableEq d]
19   [AddCommGroup V] [Module K V] [TopologicalSpace V] [T2Space V]
20 
21 /-- Actual matrix action in the supplied finite continuous coordinates. -/
22 def matrixAction (e : V ≃L[K] (d → K)) (M : Matrix d d K) (v : V) : V :=
23   e.symm (M *ᵥ e v)
24 
25 omit [T2Space K] [DecidableEq d] [T2Space V] in
26 @[fun_prop] theorem matrixAction_continuous (e : V ≃L[K] (d → K)) :
27     Continuous (fun p : Matrix d d K × V => matrixAction e p.1 p.2) := by
28   unfold matrixAction
29   apply e.symm.continuous.comp
30   apply continuous_pi
31   intro i
32   simp only [Matrix.mulVec, dotProduct]
33   fun_prop
34 
35 /-- The actual endomorphism monoid preserving the literal lattice. -/
36 def preserving (e : V ≃L[K] (d → K)) (L : AddSubgroup V) : Submonoid (Matrix d d K) where
37   carrier := {M | ∀ v ∈ L, matrixAction e M v ∈ L}
38   one_mem' := by intro v hv; simpa [matrixAction] using hv
39   mul_mem' := by
40     intro M N hM hN v hv
41     have h := hM (matrixAction e N v) (hN v hv)
42     simpa [matrixAction, Matrix.mulVec_mulVec] using h
43 
44 /-- The stabilizer is the unit group of the literal preserving monoid. -/
45 def stabilizer (e : V ≃L[K] (d → K)) (L : AddSubgroup V) :
46     Subgroup (GeneralLinearGroup d K) := (preserving e L).units
47 
48 omit [T2Space K] [T2Space V] in
49 /-- Preserving a closed lattice is a closed condition on actual matrices. -/
50 theorem preserving_closed (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
51     (hL : IsClosed (L : Set V)) : IsClosed (preserving e L : Set (Matrix d d K)) := by
52   change IsClosed {M : Matrix d d K | ∀ v, v ∈ L → matrixAction e M v ∈ L}
53   simp only [Set.ofPred_forall]
54   apply isClosed_iInter
55   intro v
56   apply isClosed_iInter
57   intro _
58   exact hL.preimage ((matrixAction_continuous e).comp (continuous_id.prodMk continuous_const))
59 
60 omit [T2Space K] [T2Space V] in
61 /-- Compact-open continuity makes preservation of a compact open lattice open. -/
62 theorem preserving_open (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
63     (hc : IsCompact (L : Set V)) (ho : IsOpen (L : Set V)) :
64     IsOpen (preserving e L : Set (Matrix d d K)) := by
65   let f : Matrix d d K → C(V, V) := fun M =>
66     ⟨matrixAction e M, (matrixAction_continuous e).comp (continuous_const.prodMk continuous_id)⟩
67   have hf : Continuous f := ContinuousMap.continuous_of_continuous_uncurry f
68     (matrixAction_continuous e)
69   exact (ContinuousMap.isOpen_setOfPred_mapsTo hc ho).preimage hf
70 
71 omit [T2Space K] in
72 /-- A basis inside the lattice gives a compact set containing all preserving matrices. -/
73 theorem preserving_compact (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
74     (hc : IsCompact (L : Set V))
75     (hb : ∀ i, e.symm (Pi.single i 1) ∈ L) :
76     IsCompact (preserving e L : Set (Matrix d d K)) := by
77   let C : Set (d → K) := e '' (L : Set V)
78   have hC : IsCompact C := hc.image e.continuous
79   have hP : IsCompact (Set.pi Set.univ (fun _ : d => C)) := isCompact_univ_pi (fun _ => hC)
80   have hT : IsCompact (Matrix.transpose '' Set.pi Set.univ (fun _ : d => C)) :=
81     hP.image continuous_id.matrix_transpose
82   apply hT.of_isClosed_subset (preserving_closed e L hc.isClosed)
83   intro M hM
84   refine ⟨Mᵀ, ?_, Matrix.transpose_transpose M⟩
85   intro i _
86   refine ⟨matrixAction e M (e.symm (Pi.single i 1)), hM _ (hb i), ?_⟩
87   simp only [matrixAction, ContinuousLinearEquiv.apply_symm_apply, Matrix.mulVec_single_one]
88   rfl
89 
90 omit [IsTopologicalRing K] [T2Space K] [T2Space V] in
91 /-- Every finite basis can be uniformly moved into an open lattice by a nonzero base scalar. -/
92 theorem exists_scaled_basis [ContinuousSMul K V] [Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ)]
93     (e : V ≃L[K] (d → K)) (L : AddSubgroup V) (ho : IsOpen (L : Set V)) :
94     ∃ c : Kˣ, ∀ i, (c : K) • e.symm (Pi.single i 1) ∈ L := by
95   have he : ∀ᶠ c : K in nhds (0 : K), ∀ i, c • e.symm (Pi.single i 1) ∈ L := by
96     rw [Filter.eventually_all]
97     intro i
98     exact (continuous_id.smul continuous_const).continuousAt.preimage_mem_nhds
99       (ho.mem_nhds (by simp))
100   have he' : ∀ᶠ c : K in nhdsWithin (0 : K) {0}ᶜ, ∀ i, c • e.symm (Pi.single i 1) ∈ L :=
101     he.filter_mono nhdsWithin_le_nhds
102   have hn : ∀ᶠ c : K in nhdsWithin (0 : K) {0}ᶜ, c ≠ 0 := by
103     exact Filter.Eventually.mono (self_mem_nhdsWithin : {0}ᶜ ∈ nhdsWithin (0 : K) {0}ᶜ)
104       (fun _ h => h)
105   obtain ⟨c, hc, hci⟩ := (hn.and he').exists
106   exact ⟨Units.mk0 c hc, hci⟩
107 
108 omit [T2Space K] in
109 /-- Openness supplies the required bounded basis, so no integral-basis premise remains. -/
110 theorem preserving_compact_of_open [ContinuousSMul K V]
111     [Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ)]
112     (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
113     (hc : IsCompact (L : Set V)) (ho : IsOpen (L : Set V)) :
114     IsCompact (preserving e L : Set (Matrix d d K)) := by
115   obtain ⟨c, hb⟩ := exists_scaled_basis e L ho
116   let C : Set (d → K) := (fun v : V => e ((↑c⁻¹ : K) • v)) '' (L : Set V)
117   have hC : IsCompact C := hc.image (e.continuous.comp (continuous_const.smul continuous_id))
118   have hP : IsCompact (Set.pi Set.univ (fun _ : d => C)) := isCompact_univ_pi (fun _ => hC)
119   have hT : IsCompact (Matrix.transpose '' Set.pi Set.univ (fun _ : d => C)) :=
120     hP.image continuous_id.matrix_transpose
121   apply hT.of_isClosed_subset (preserving_closed e L hc.isClosed)
122   intro M hM
123   refine ⟨Mᵀ, ?_, Matrix.transpose_transpose M⟩
124   intro i _
125   refine ⟨matrixAction e M ((c : K) • e.symm (Pi.single i 1)), hM _ (hb i), ?_⟩
126   simp only [matrixAction, map_smul, ContinuousLinearEquiv.apply_symm_apply, Matrix.mulVec_smul,
127     Matrix.mulVec_single_one, smul_smul, Units.inv_mul, one_smul]
128   rfl
129 
130 /-- The literal lattice stabilizer is compact in actual `GL_d(K)`. -/
131 theorem stabilizer_compact (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
132     (hc : IsCompact (L : Set V))
133     (hb : ∀ i, e.symm (Pi.single i 1) ∈ L) :
134     IsCompact (stabilizer e L : Set (GeneralLinearGroup d K)) :=
135   Submonoid.units_isCompact (preserving_compact e L hc hb)
136 
137 omit [T2Space K] [T2Space V] in
138 /-- The same literal stabilizer is open in actual `GL_d(K)`. -/
139 theorem stabilizer_open (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
140     (hc : IsCompact (L : Set V)) (ho : IsOpen (L : Set V)) :
141     IsOpen (stabilizer e L : Set (GeneralLinearGroup d K)) :=
142   Submonoid.isOpen_units (preserving_open e L hc ho)
143 
144 /-- Every compact open additive lattice has compact matrix stabilizer. -/
145 theorem stabilizer_compact_of_open [ContinuousSMul K V]
146     [Filter.NeBot (nhdsWithin (0 : K) {0}ᶜ)]
147     (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
148     (hc : IsCompact (L : Set V)) (ho : IsOpen (L : Set V)) :
149     IsCompact (stabilizer e L : Set (GeneralLinearGroup d K)) :=
150   Submonoid.units_isCompact (preserving_compact_of_open e L hc ho)
151 
152 end PaperXI.LatticeMatrixTopology60

Back to source controls