CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
import
- Mathlib.Topology.Algebra.LinearTopology
- CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
theorem exists_openAddSubgroup_subset_open_nhds_zero
{M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
[CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
{U : Set M} (hUopen : IsOpen U) (h0U : (0 : M) ∈ U) :
∃ H : OpenAddSubgroup M, (H : Set M) ⊆ UA compact Hausdorff totally disconnected additive group has arbitrarily small open additive subgroups at zero.
Show proof
by
rcases ((nhds_basis_clopen (0 : M)).mem_iff.mp (hUopen.mem_nhds h0U)) with
⟨W, hW, hWU⟩
rcases IsTopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhds_of_zero hW.2 hW.1 with
⟨H, hH⟩
exact ⟨H, hH.trans hWU⟩Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem exists_openAddSubgroup_forall_smul_mem
{Λ : Type u} {M : Type v} [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
[TopologicalSpace M] [Module Λ M] [CompactSpace Λ] [IsTopologicalAddGroup M]
[CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M] [ContinuousSMul Λ M]
(A : OpenAddSubgroup M) :
∃ V : OpenAddSubgroup M, ∀ lam : Λ, ∀ v : M, v ∈ V → lam • v ∈ AAround zero there is an open additive subgroup whose scalar multiples all land in a given open additive subgroup.
Show proof
by
let T : Set (Λ × M) := {p | p.1 • p.2 ∈ (A : Set M)}
have hTopen : IsOpen T := by
exact (OpenAddSubgroup.isOpen A).preimage continuous_smul
have hcontains : (Set.univ : Set Λ) ×ˢ ({0} : Set M) ⊆ T := by
rintro ⟨lam, m⟩ ⟨_hlam, hm⟩
rw [Set.mem_singleton_iff] at hm
change m = 0 at hm
change lam • m ∈ A
rw [hm]
simp only [smul_zero, zero_mem]
rcases generalized_tube_lemma (s := (Set.univ : Set Λ)) isCompact_univ
(t := ({0} : Set M)) isCompact_singleton hTopen hcontains with
⟨_W, V, _hWopen, hVopen, hWuniv, h0V, hWV⟩
have hzeroV : (0 : M) ∈ V := h0V (by simp only [Set.mem_singleton_iff])
rcases exists_openAddSubgroup_subset_open_nhds_zero hVopen hzeroV with ⟨H, hH⟩
refine ⟨H, ?_⟩
intro lam v hv
show (lam, v) ∈ T
exact hWV ⟨hWuniv trivial, hH hv⟩Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□def submoduleGeneratedByScalarMultiples
(Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [Module Λ M]
(V : AddSubgroup M) : Submodule Λ M where
carrier := AddSubgroup.closure {x : M | ∃ lam : Λ, ∃ v : M, v ∈ V ∧ x = lam • v}
zero_mem' := by
exact AddSubgroup.zero_mem _
add_mem' := by
intro x y hx hy
exact AddSubgroup.add_mem _ hx hy
smul_mem' := by
intro lam x hx
change lam • x ∈
AddSubgroup.closure {x : M | ∃ mu : Λ, ∃ v : M, v ∈ V ∧ x = mu • v}
induction hx using AddSubgroup.closure_induction with
| mem y hy =>
rcases hy with ⟨mu, v, hv, rfl⟩
exact AddSubgroup.subset_closure ⟨lam * mu, v, hv, by simp only [mul_smul]⟩
| zero =>
simp only [smul_zero, zero_mem]
| add x y _ _ hx hy =>
simpa [smul_add] using AddSubgroup.add_mem _ hx hy
| neg x _ hx =>
simpa using AddSubgroup.neg_mem _ hxThe submodule generated by all scalar multiples of an open additive subgroup.
theorem submoduleGeneratedByScalarMultiples_open
(Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [TopologicalSpace M]
[Module Λ M] [ContinuousAdd M] (V : OpenAddSubgroup M) :
IsOpen (submoduleGeneratedByScalarMultiples Λ M V : Set M)The submodule generated by scalar multiples of an open additive subgroup is open.
Show proof
by
let N := submoduleGeneratedByScalarMultiples Λ M V
have hVsub : (V : Set M) ⊆ (N : Set M) := by
intro v hv
exact AddSubgroup.subset_closure ⟨1, v, hv, by simp only [one_smul]⟩
exact N.toAddSubgroup.isOpen_of_mem_nhds
(Filter.mem_of_superset ((OpenAddSubgroup.isOpen V).mem_nhds (zero_mem V)) hVsub)Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem submoduleGeneratedByScalarMultiples_subset
(Λ : Type u) (M : Type v) [Ring Λ] [AddCommGroup M] [Module Λ M]
(V A : AddSubgroup M)
(hVA : ∀ lam : Λ, ∀ v : M, v ∈ V → lam • v ∈ A) :
(submoduleGeneratedByScalarMultiples Λ M V : Set M) ⊆ (A : Set M)To bound the scalar-multiple generated submodule, it suffices to bound each generator.
Show proof
by
intro x hx
change x ∈ A
induction hx using AddSubgroup.closure_induction with
| mem y hy =>
rcases hy with ⟨lam, v, hv, rfl⟩
exact hVA lam v hv
| zero =>
exact zero_mem A
| add x y _ _ hx hy =>
exact AddSubgroup.add_mem A hx hy
| neg x _ hx =>
exact AddSubgroup.neg_mem A hxProof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem profiniteModule_isLinearTopology
(Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
[TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M) :
IsLinearTopology Λ MIn Lemma 5.1.1(b), linear-topology part, the topology of a profinite module is linear.
Show proof
by
letI : IsTopologicalRing Λ := hM.1.1
letI : CompactSpace Λ := hM.1.2.1
letI : IsTopologicalAddGroup M := hM.2.1
letI : ContinuousAdd M := inferInstance
letI : ContinuousSMul Λ M := hM.2.2.1
letI : CompactSpace M := hM.2.2.2.1
letI : T2Space M := hM.2.2.2.2.1
letI : TotallyDisconnectedSpace M := hM.2.2.2.2.2
rw [isLinearTopology_iff_hasBasis_open_submodule]
refine Filter.hasBasis_iff.mpr ?_
intro U
constructor
· intro hU
rcases mem_nhds_iff.mp hU with ⟨O, hOU, hOopen, h0O⟩
rcases exists_openAddSubgroup_subset_open_nhds_zero hOopen h0O with ⟨A, hAO⟩
rcases exists_openAddSubgroup_forall_smul_mem (Λ := Λ) A with ⟨V, hV⟩
let N := submoduleGeneratedByScalarMultiples Λ M V.toAddSubgroup
have hNopen : IsOpen (N : Set M) :=
submoduleGeneratedByScalarMultiples_open Λ M V
have hNA : (N : Set M) ⊆ (A : Set M) :=
submoduleGeneratedByScalarMultiples_subset Λ M V.toAddSubgroup A.toAddSubgroup hV
exact ⟨N, hNopen, hNA.trans (hAO.trans hOU)⟩
· rintro ⟨N, hNopen, hNU⟩
exact Filter.mem_of_superset (hNopen.mem_nhds (zero_mem N)) hNUProof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem finite_quotient_of_openSubmodule
(Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
[TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
(N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
Nonempty (Fintype (M ⧸ N))Show proof
by
letI : IsTopologicalAddGroup M := hM.2.1
letI : ContinuousAdd M := inferInstance
letI : CompactSpace M := hM.2.2.2.1
haveI : Finite (M ⧸ N) :=
AddSubgroup.quotient_finite_of_isOpen N.toAddSubgroup hN
exact ⟨Fintype.ofFinite (M ⧸ N)⟩Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem quotient_openSubmodule_isDiscreteModule
(Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
[TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
(N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
IsDiscreteModule Λ (M ⧸ N)The quotient by an open submodule is a discrete topological module.
Show proof
by
letI : IsTopologicalRing Λ := hM.1.1
letI : IsTopologicalAddGroup M := hM.2.1
letI : ContinuousAdd M := inferInstance
letI : ContinuousSMul Λ M := hM.2.2.1
haveI : DiscreteTopology (M ⧸ N) :=
QuotientAddGroup.discreteTopology (N := N.toAddSubgroup) hN
exact ⟨⟨hM.1.1, inferInstance, inferInstance⟩, inferInstance⟩Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□theorem quotient_openSubmodule_finiteDiscrete
(Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
[TopologicalSpace M] [Module Λ M] (hM : IsProfiniteModule Λ M)
(N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
IsDiscreteModule Λ (M ⧸ N) ∧ Nonempty (Fintype (M ⧸ N))Open submodule quotients are finite discrete modules.
Show proof
⟨quotient_openSubmodule_isDiscreteModule Λ M hM N hN,
finite_quotient_of_openSubmodule Λ M hM N hN⟩Proof. Work at zero in the additive topological group underlying the module. Compactness, Hausdorffness, and total disconnectedness give arbitrarily small open additive subgroups, and continuity of scalar multiplication lets one shrink to a subgroup stable under the relevant scalars. The submodule generated by scalar multiples is therefore open and contained in the prescribed neighborhood, while quotienting by an open submodule gives a finite discrete module.
□