LatticeCongruenceTopology60.lean

1 import PaperXI.LatticeMatrixTopology60
2 import PaperXI.PeriodicLatticeReduction60
3 
4 /-!
5 # Topology of the full periodic-lattice congruence group
6 
7 The infinite definition is preserved literally. A base-field scalar period
8 proves openness by finite reduction, while compactness follows from the zero
9 lattice stabilizer. The ambient group is actual `GL_d(K)`.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.LatticeCongruenceTopology60
14 open Matrix Topology ActualELatticeNormalizer59 LatticeMatrixTopology60 PeriodicLatticeReduction60
15 variable {K V d : Type*} [Field K] [TopologicalSpace K] [IsTopologicalRing K]
16   [T2Space K] [Fintype d] [DecidableEq d]
17   [AddCommGroup V] [Module K V] [TopologicalSpace V] [IsTopologicalAddGroup V]
18   [T2Space V]
19 
20 /-- The matrix group is identified with the actual linear automorphism group. -/
21 def coordinateAut (e : V ≃L[K] (d → K)) :
22     GeneralLinearGroup d K ≃* (V ≃ₗ[K] V) :=
23   (GeneralLinearGroup.toLin.trans
24     (LinearMap.GeneralLinearGroup.congrLinearEquiv e.toLinearEquiv.symm)).trans
25     (LinearMap.GeneralLinearGroup.generalLinearEquiv K V)
26 
27 omit [IsTopologicalRing K] [T2Space K] [IsTopologicalAddGroup V] [T2Space V] in
28 @[simp] theorem coordinateAut_apply (e : V ≃L[K] (d → K))
29     (g : GeneralLinearGroup d K) (v : V) :
30     coordinateAut e g v = matrixAction e (g : Matrix d d K) v := rfl
31 
32 /-- The matrix subgroup is the exact preimage of the literal full-chain subgroup. -/
33 def congruence (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V) :
34     Subgroup (GeneralLinearGroup d K) :=
35   (firstCongruence L).comap (coordinateAut e).toMonoidHom
36 
37 omit [IsTopologicalRing K] [T2Space K] [IsTopologicalAddGroup V] [T2Space V] in
38 theorem mem_stabilizer_iff (e : V ≃L[K] (d → K)) (L : AddSubgroup V)
39     (g : GeneralLinearGroup d K) :
40     g ∈ stabilizer e L ↔ ∀ v, coordinateAut e g v ∈ L ↔ v ∈ L := by
41   constructor
42   · rintro ⟨hg, hi⟩ v
43     constructor
44     · intro hv
45       have h := hi _ hv
46       change coordinateAut e g⁻¹ (coordinateAut e g v) ∈ L at h
47       rw [map_inv] at h
48       exact (coordinateAut e g).symm_apply_apply v ▸ h
49     · exact hg v
50   · intro h
51     constructor
52     · exact fun v hv => (h v).mpr hv
53     · intro v hv
54       apply (h (coordinateAut e g⁻¹ v)).mp
55       rw [map_inv]
56       change (coordinateAut e g) ((coordinateAut e g).symm v) ∈ L
57       simpa only [LinearEquiv.apply_symm_apply] using hv
58 
59 /-- The exact one-level condition in actual matrix coordinates. -/
60 def levelSet (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V) (i : ℤ) :
61     Set (GeneralLinearGroup d K) :=
62   {g | levelCondition L (coordinateAut e g) i}
63 
64 omit [IsTopologicalRing K] [T2Space K] [IsTopologicalAddGroup V] [T2Space V] in
65 theorem levelSet_eq (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V) (i : ℤ) :
66     levelSet e L i = (stabilizer e (L i) : Set (GeneralLinearGroup d K)) ∩
67       {g | ∀ v ∈ L i, matrixAction e (g : Matrix d d K) v - v ∈ L (i + 1)} := by
68   ext g
69   exact and_congr (mem_stabilizer_iff e (L i) g).symm Iff.rfl
70 
71 omit [T2Space K] [T2Space V] in
72 theorem levelSet_closed (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V) (i : ℤ)
73     (hi : IsClosed (L i : Set V)) (hj : IsClosed (L (i + 1) : Set V)) :
74     IsClosed (levelSet e L i) := by
75   rw [levelSet_eq]
76   apply IsClosed.inter
77   · exact ((preserving_closed e (L i) hi).preimage Units.continuous_val).inter
78       ((preserving_closed e (L i) hi).preimage Units.continuous_coe_inv)
79   · simp only [Set.ofPred_forall]
80     apply isClosed_iInter
81     intro v
82     apply isClosed_iInter
83     intro _
84     apply hj.preimage
85     exact ((matrixAction_continuous e).comp
86       (Units.continuous_val.prodMk continuous_const)).sub continuous_const
87 
88 omit [T2Space K] [T2Space V] in
89 theorem levelSet_open (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V) (i : ℤ)
90     (hi : IsCompact (L i : Set V)) (hoi : IsOpen (L i : Set V))
91     (hoj : IsOpen (L (i + 1) : Set V)) : IsOpen (levelSet e L i) := by
92   rw [levelSet_eq]
93   apply IsOpen.inter (stabilizer_open e (L i) hi hoi)
94   let f : GeneralLinearGroup d K → C(V, V) := fun g =>
95     ⟨fun v => matrixAction e (g : Matrix d d K) v - v,
96       ((matrixAction_continuous e).comp (continuous_const.prodMk continuous_id)).sub continuous_id⟩
97   have hf : Continuous f := by
98     apply ContinuousMap.continuous_of_continuous_uncurry
99     exact ((matrixAction_continuous e).comp
100       ((Units.continuous_val.comp continuous_fst).prodMk continuous_snd)).sub continuous_snd
101   exact (ContinuousMap.isOpen_setOfPred_mapsTo hi hoj).preimage hf
102 
103 omit [T2Space K] in
104 /-- Compactness of all levels makes literal full-chain congruence closed. -/
105 theorem congruence_closed (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V)
106     (hL : ∀ i, IsCompact (L i : Set V)) :
107     IsClosed (congruence e L : Set (GeneralLinearGroup d K)) := by
108   have he : (congruence e L : Set (GeneralLinearGroup d K)) = ⋂ i, levelSet e L i := by
109     ext g
110     simp only [Set.mem_iInter, levelSet, Set.mem_ofPred_eq]
111     constructor
112     · intro h i
113       exact ⟨h.1 i, h.2 i⟩
114     · intro h
115       exact ⟨fun i => (h i).1, fun i => (h i).2⟩
116   rw [he]
117   exact isClosed_iInter fun i => levelSet_closed e L i (hL i).isClosed (hL (i + 1)).isClosed
118 
119 /-- A basis in level zero bounds the entire congruence group compactly. -/
120 theorem congruence_compact (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V)
121     (hL : ∀ i, IsCompact (L i : Set V))
122     (hb : ∀ j, e.symm (Pi.single j 1) ∈ L 0) :
123     IsCompact (congruence e L : Set (GeneralLinearGroup d K)) := by
124   apply (stabilizer_compact e (L 0) (hL 0) hb).of_isClosed_subset (congruence_closed e L hL)
125   intro g hg
126   exact (mem_stabilizer_iff e (L 0) g).mpr (hg.1 0)
127 
128 omit [T2Space K] [T2Space V] in
129 /-- A positive base-field period makes the literal full-chain congruence open. -/
130 theorem congruence_open (e : V ≃L[K] (d → K)) (L : ℤ → AddSubgroup V)
131     (hLc : ∀ i, IsCompact (L i : Set V)) (hLo : ∀ i, IsOpen (L i : Set V))
132     (c : Kˣ) (r : ℕ) (hr : 0 < r)
133     (hperiod : ∀ i v, (c : K) • v ∈ L (i + (r : ℤ)) ↔ v ∈ L i) :
134     IsOpen (congruence e L : Set (GeneralLinearGroup d K)) := by
135   have he : (congruence e L : Set (GeneralLinearGroup d K)) =
136       ⋂ j : Fin r, levelSet e L (j.val : ℤ) := by
137     ext g
138     simp only [Set.mem_iInter, levelSet, Set.mem_ofPred_eq]
139     exact mem_firstCongruence_iff_fin L c r hr hperiod (coordinateAut e g)
140   rw [he]
141   exact isOpen_iInter_of_finite fun j => levelSet_open e L j.val (hLc j.val) (hLo j.val)
142     (hLo (j.val + 1))
143 
144 end PaperXI.LatticeCongruenceTopology60

Back to source controls