Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients
ProCGroups/CompletedGroupAlgebra/ProfiniteModules/Basic/FiniteQuotients

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.FiniteQuotients

5 Theorems | 1 Abbreviation

Open submodules of a profinite module have finite quotients and separate continuous linear maps. This file packages open submodules and supplies quotient-continuity and finite-refinement criteria.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.profiniteModule_hasFiniteIndexSubmoduleBasis_of_linearTopology 
theorem profiniteModule_hasFiniteIndexSubmoduleBasis_of_linearTopology
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsLinearTopology Λ M]
    [IsTopologicalAddGroup M] [CompactSpace M] :
    HasFiniteIndexSubmoduleBasis Λ M

In Lemma 5.1.1(b), linear-topology interface, a profinite module with a linear topology has a basis of open finite-index submodules at zero.

Show Lean proof
Theorem CompletedGroupAlgebra.profiniteModule_hasFiniteIndexSubmoduleBasis 
theorem profiniteModule_hasFiniteIndexSubmoduleBasis
    (Λ : 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] :
    HasFiniteIndexSubmoduleBasis Λ M

In Lemma 5.1.1(b), finite-index submodules form a neighborhood basis at zero in a profinite module.

Show Lean proof
Theorem CompletedGroupAlgebra.profiniteModule_ext_of_openSubmoduleQuotients 
theorem profiniteModule_ext_of_openSubmoduleQuotients
    {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
    [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
    [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
    {x y : N}
    (h : ∀ W : Submodule R N, IsOpen (W : Set N) → Submodule.mkQ W x = Submodule.mkQ W y) :
    x = y

Open submodule quotients separate points of a profinite module.

Show Lean proof
Abbreviation CompletedGroupAlgebra.ProfiniteModuleOpenSubmodule 
abbrev ProfiniteModuleOpenSubmodule
    (R : Type u) (N : Type v) [Ring R] [AddCommGroup N] [Module R N]
    [TopologicalSpace N] : Type _ :=
  {W : Submodule R N // IsOpen (W : Set N)}

Open submodules of a profinite module.

Theorem CompletedGroupAlgebra.continuous_of_forall_openSubmodule_quotient_continuous 
theorem continuous_of_forall_openSubmodule_quotient_continuous
    {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
    [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
    [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
    {Y : Type z} [TopologicalSpace Y] {F : Y → N}
    (hF : ∀ W : Submodule R N, IsOpen (W : Set N) →
      Continuous fun y : Y => Submodule.mkQ W (F y)) :
    Continuous F

Open submodule quotients detect continuity of maps into a profinite module.

Show Lean proof
Theorem CompletedGroupAlgebra.exists_openSubmodule_le_finset 
theorem exists_openSubmodule_le_finset
    {R : Type u} (N : Type v) [Ring R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
    (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
    ∃ K : ProfiniteModuleOpenSubmodule (R := R) N,
      ∀ W ∈ s, K.1 ≤ W.1

A finite family of open submodules has an open submodule contained in all of them.

Show Lean proof