ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule

7 Theorems | 1 Definition

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.

imports

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

Imported by

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients

Theorem CompletedGroupAlgebra.exists_openAddSubgroup_subset_open_nhds_zero

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

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

Show Lean proof

Theorem CompletedGroupAlgebra.exists_openAddSubgroup_forall_smul_mem

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

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

Show Lean proof

Definition CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples

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

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

Theorem CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples_open

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 Lean proof

Theorem CompletedGroupAlgebra.submoduleGeneratedByScalarMultiples_subset

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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.profiniteModule_isLinearTopology

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

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

Show Lean proof

Theorem CompletedGroupAlgebra.finite_quotient_of_openSubmodule

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

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).

Show Lean proof

Theorem CompletedGroupAlgebra.quotient_openSubmodule_isDiscreteModule

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)

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

Show Lean proof

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenSubmodule

Declarations