Module

OpenSubmodule.lean

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule

8 declarations indexed from sourceView source ↗

Module documentation

Open submodules of profinite modules

This file constructs open submodules inside identity neighborhoods using scalar multiples of open additive subgroups. It proves the resulting linear topology and the finiteness and discreteness of open-submodule quotients.

Imports2

Mathlib.Topology.Algebra.LinearTopology
Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions

Imported by2

theorem

exists_openAddSubgroup_subset_open_nhds_zero

L28 ↗

CompletedGroupAlgebra.exists_openAddSubgroup_subset_open_nhds_zero

Documentation

A compact Hausdorff totally disconnected additive group has arbitrarily small open additive subgroups at zero.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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) ⊆ U

theorem

exists_openAddSubgroup_forall_smul_mem

L43 ↗

CompletedGroupAlgebra.exists_openAddSubgroup_forall_smul_mem

Documentation

Around zero there is an open additive subgroup whose scalar multiples all land in a given open additive subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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 ∈ A

def

submoduleGeneratedByScalarMultiples

L70 ↗

CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples

Documentation

The submodule generated by all scalar multiples of an open additive subgroup.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · full declaration

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 _ hx

theorem

submoduleGeneratedByScalarMultiples_open

L95 ↗

CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples_open

Documentation

The submodule generated by scalar multiples of an open additive subgroup is open.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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)

theorem

submoduleGeneratedByScalarMultiples_subset

L110 ↗

CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples_subset

Documentation

Bounds on every generator imply the corresponding bound on the scalar-multiple generated submodule.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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)

theorem

profiniteModule_isLinearTopology

L129 ↗

CompletedGroupAlgebra.profiniteModule_isLinearTopology

Documentation

In Lemma 5.1.1(b), linear-topology part, the topology of a profinite module is linear.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

theorem profiniteModule_isLinearTopology
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ] [CompactSpace Λ]
    [IsTopologicalAddGroup M] [ContinuousSMul Λ M] [CompactSpace M] [T2Space M]
    [TotallyDisconnectedSpace M] :
    IsLinearTopology Λ M

theorem

finite_quotient_of_openSubmodule

L156 ↗

CompletedGroupAlgebra.finite_quotient_of_openSubmodule

Documentation

An open submodule of a compact topological additive group has finite quotient. This is the finite-quotient step used in Lemma 5.1.1(b).

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

theorem finite_quotient_of_openSubmodule
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsTopologicalAddGroup M] [CompactSpace M]
    (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
    Nonempty (Fintype (M ⧸ N))

theorem

quotient_openSubmodule_isDiscreteModule

L166 ↗

CompletedGroupAlgebra.quotient_openSubmodule_isDiscreteModule

Documentation

The quotient by an open submodule is a discrete topological module.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

theorem quotient_openSubmodule_isDiscreteModule
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ]
    [IsTopologicalAddGroup M] [ContinuousSMul Λ M]
    (N : Submodule Λ M) (hN : IsOpen (N : Set M)) :
    IsDiscreteModule Λ (M ⧸ N)

Module documentation

Open submodules of profinite modules

Declarations