Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients
1import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule
3/-!
4# Finite quotients of profinite modules
6Open submodules of a profinite module have finite quotients and separate continuous linear maps.
7This file packages open submodules and supplies quotient-continuity and finite-refinement
8criteria.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15universe u v w z
17/--
18In Lemma 5.1.1(b), linear-topology interface, a profinite module with a linear topology has a
19basis of open finite-index submodules at zero.
20-/
21theorem profiniteModule_hasFiniteIndexSubmoduleBasis_of_linearTopology
22 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
23 [TopologicalSpace M] [Module Λ M] [IsLinearTopology Λ M]
24 [IsTopologicalAddGroup M] [CompactSpace M] :
25 HasFiniteIndexSubmoduleBasis Λ M := by
26 letI : ContinuousAdd M := inferInstance
27 intro U hU
28 rcases ((IsLinearTopology.hasBasis_open_submodule Λ).mem_iff.mp hU) with
29 ⟨N, hNopen, hNU⟩
30 exact ⟨N, hNopen, hNU,
31 finite_quotient_of_openSubmodule Λ M N hNopen⟩
33/--
34In Lemma 5.1.1(b), finite-index submodules form a neighborhood basis at zero in a profinite
35module.
36-/
37theorem profiniteModule_hasFiniteIndexSubmoduleBasis
38 (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
39 [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ] [CompactSpace Λ]
40 [IsTopologicalAddGroup M] [ContinuousSMul Λ M] [CompactSpace M] [T2Space M]
41 [TotallyDisconnectedSpace M] :
42 HasFiniteIndexSubmoduleBasis Λ M := by
43 letI : IsLinearTopology Λ M := profiniteModule_isLinearTopology Λ M
44 exact profiniteModule_hasFiniteIndexSubmoduleBasis_of_linearTopology Λ M
46/-- Open submodule quotients separate points of a profinite module. -/
47theorem profiniteModule_ext_of_openSubmoduleQuotients
48 {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
49 [AddCommGroup N] [TopologicalSpace N] [Module R N]
50 [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
51 [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
52 {x y : N}
53 (h : ∀ W : Submodule R N, IsOpen (W : Set N) → Submodule.mkQ W x = Submodule.mkQ W y) :
54 x = y := by
55 by_contra hxy
56 let O : Set N := ({x - y} : Set N)ᶜ
57 have hd0 : x - y ≠ 0 := by
58 intro hd
59 exact hxy (sub_eq_zero.mp hd)
60 have hOopen : IsOpen O := isClosed_singleton.isOpen_compl
61 have h0O : (0 : N) ∈ O := by
62 change (0 : N) ≠ x - y
63 exact hd0.symm
64 rcases profiniteModule_hasFiniteIndexSubmoduleBasis R N O (hOopen.mem_nhds h0O) with
65 ⟨W, hWopen, hWO, _hfinite⟩
66 have hq := h W hWopen
67 rw [Submodule.mkQ_apply, Submodule.mkQ_apply] at hq
68 have hdiff : x - y ∈ W := (Submodule.Quotient.eq W).1 hq
69 exact (hWO hdiff) (by simp only [Set.mem_singleton_iff])
71/-- Open submodules of a profinite module. -/
72abbrev ProfiniteModuleOpenSubmodule
73 (R : Type u) (N : Type v) [Ring R] [AddCommGroup N] [Module R N]
74 [TopologicalSpace N] : Type _ :=
75 {W : Submodule R N // IsOpen (W : Set N)}
77/-- Open submodule quotients detect continuity of maps into a profinite module. -/
78theorem continuous_of_forall_openSubmodule_quotient_continuous
79 {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
80 [AddCommGroup N] [TopologicalSpace N] [Module R N]
81 [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
82 [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
83 {Y : Type z} [TopologicalSpace Y] {F : Y → N}
84 (hF : ∀ W : Submodule R N, IsOpen (W : Set N) →
85 Continuous fun y : Y => Submodule.mkQ W (F y)) :
86 Continuous F := by
87 letI : ContinuousAdd N := inferInstance
88 rw [continuous_iff_continuousAt]
89 intro y
90 rw [continuousAt_def]
91 intro A hA
92 rcases mem_nhds_iff.mp hA with ⟨O, hOA, hOopen, hFO⟩
93 let U0 : Set N := {z | F y + z ∈ O}
94 have hU0 : U0 ∈ 𝓝 (0 : N) := by
95 apply IsOpen.mem_nhds
96 · exact hOopen.preimage (continuous_const.add continuous_id)
97 · simp only [Set.mem_setOf_eq, add_zero, hFO, U0]
98 rcases profiniteModule_hasFiniteIndexSubmoduleBasis R N U0 hU0 with
99 ⟨W, hWopen, hWU, _hfinite⟩
100 let hdisc : IsDiscreteModule R (N ⧸ W) :=
101 quotient_openSubmodule_isDiscreteModule R N W hWopen
102 letI : DiscreteTopology (N ⧸ W) := hdisc.2
103 let q : Y → N ⧸ W := fun z => Submodule.mkQ W (F z)
104 let B : Set (N ⧸ W) := {Submodule.mkQ W (F y)}
105 have hqcont : Continuous q := hF W hWopen
106 have hpreOpen : IsOpen (q ⁻¹' B) := (isOpen_discrete B).preimage hqcont
107 have hypre : y ∈ q ⁻¹' B := by
108 simp only [Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff, q, B]
109 refine Filter.mem_of_superset (hpreOpen.mem_nhds hypre) ?_
110 intro z hz
111 apply hOA
112 have hquot : Submodule.mkQ W (F z) = Submodule.mkQ W (F y) := by
113 simpa [q, B] using hz
114 rw [Submodule.mkQ_apply, Submodule.mkQ_apply] at hquot
115 have hdiff : F z - F y ∈ W := (Submodule.Quotient.eq W).1 hquot
116 have hU : F z - F y ∈ U0 := hWU hdiff
117 change F y + (F z - F y) ∈ O at hU
118 simpa [sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using hU
120/-- A finite family of open submodules has an open submodule contained in all of them. -/
121theorem exists_openSubmodule_le_finset
122 {R : Type u} (N : Type v) [Ring R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
123 (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
124 ∃ K : ProfiniteModuleOpenSubmodule (R := R) N,
125 ∀ W ∈ s, K.1 ≤ W.1 := by
126 classical
127 refine Finset.induction_on s ?empty ?insert
128 · refine ⟨⟨⊤, isOpen_univ⟩, ?_⟩
129 simp only [Finset.notMem_empty, top_le_iff, IsEmpty.forall_iff, implies_true]
130 · intro W s hWs ih
131 rcases ih with ⟨K, hK⟩
132 refine ⟨⟨K.1 ⊓ W.1, K.2.inter W.2⟩, ?_⟩
133 intro V hV
134 rw [Finset.mem_insert] at hV
135 rcases hV with hVW | hVs
136 · subst V
137 exact inf_le_right
138 · exact inf_le_left.trans (hK V hVs)
140end CompletedGroupAlgebra