Module

Generators.lean

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Generators

12 declarations indexed from sourceView source ↗

Module documentation

Generating sets converging to zero

This file defines sets and maps converging to zero through open submodules and relates them to one-point extensions and dense additive generation. Every profinite module is shown to admit an appropriate generating set.

Imports2

Imported by2

def

SetConvergesToZero

L25 ↗

CompletedGroupAlgebra.SetConvergesToZero

Documentation

A subset converges to zero in the all-but-finitely-many-elements sense used in the book.

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

def SetConvergesToZero {M : Type v} [TopologicalSpace M] [Zero M] (S : Set M) : Prop

def

MapConvergesToZero

L32 ↗

CompletedGroupAlgebra.MapConvergesToZero

Documentation

A map from an arbitrary index type converges to zero along the cofinite filter. This is the map-level version used in Lemma 5.2.5(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

def MapConvergesToZero {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M]
    (f : S → M) : Prop

theorem

setConvergesToZero_range

L37 ↗

CompletedGroupAlgebra.MapConvergesToZero.setConvergesToZero_range

Documentation

A map converging to zero has image set converging to 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 MapConvergesToZero.setConvergesToZero_range
    {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
    (hf : MapConvergesToZero f) :
    SetConvergesToZero (Set.range f)

theorem

mapConvergesToZero_of_injective

L50 ↗

CompletedGroupAlgebra.SetConvergesToZero.mapConvergesToZero_of_injective

Documentation

An injective parametrization of a set converging to zero is a map converging to 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 SetConvergesToZero.mapConvergesToZero_of_injective
    {S : Type u} {M : Type v} [TopologicalSpace M] [Zero M] {f : S → M}
    (hfconv : SetConvergesToZero (Set.range f)) (hfinj : Function.Injective f) :
    MapConvergesToZero f

theorem

subtype_val

L75 ↗

CompletedGroupAlgebra.SetConvergesToZero.subtype_val

Documentation

The inclusion of a set converging to zero, viewed as a parametrized map, converges to 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 · full declaration

theorem SetConvergesToZero.subtype_val
    {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M}
    (hS : SetConvergesToZero S) :
    MapConvergesToZero (fun s : S => (s : M)) := by
  have hrange : Set.range (fun s : S => (s : M)) = S := by
    ext x
    constructor
    · rintro ⟨s, rfl⟩
      exact s.2
    · intro hx
      exact ⟨⟨x, hx⟩, rfl⟩
  have hRangeConv : SetConvergesToZero (Set.range fun s : S => (s : M)) := by
    simpa [hrange] using hS
  exact hRangeConv.mapConvergesToZero_of_injective Subtype.val_injective

theorem

continuous_onePoint_zero_extension_iff_mapConvergesToZero

L94 ↗

CompletedGroupAlgebra.continuous_onePoint_zero_extension_iff_mapConvergesToZero

Documentation

A map from a discrete set converges to zero if and only if its zero-extension to the one-point compactification is continuous.

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

theorem continuous_onePoint_zero_extension_iff_mapConvergesToZero
    {S : Type u} {M : Type v} [TopologicalSpace S] [DiscreteTopology S]
    [TopologicalSpace M] [Zero M] {f : S → M} :
    Continuous (fun x : OnePoint S => x.elim 0 f) ↔ MapConvergesToZero f := by
  rw [OnePoint.continuous_iff_from_discrete]
  rfl

theorem

finite_setConvergesToZero

L102 ↗

CompletedGroupAlgebra.finite_setConvergesToZero

Documentation

Finite subsets converge to zero in the all-but-finitely-many-elements sense used in the book.

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_setConvergesToZero
    {M : Type v} [TopologicalSpace M] [Zero M] {S : Set M} (hS : S.Finite) :
    SetConvergesToZero S

def

HasGeneratingSetConvergingToZero

L109 ↗

CompletedGroupAlgebra.HasGeneratingSetConvergingToZero

Documentation

A set of topological module generators converging to 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

def HasGeneratingSetConvergingToZero (Λ : Type u) (M : Type v) [Ring Λ]
    [TopologicalSpace M] [AddCommGroup M] [Module Λ M] : Prop

theorem

finiteGeneratingSet_convergesToZero

L117 ↗

CompletedGroupAlgebra.finiteGeneratingSet_convergesToZero

Documentation

A finite dense generating set is a generating set converging to zero. This gives the finite-generated special case of Lemma 5.1.1(c).

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 finiteGeneratingSet_convergesToZero
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
    [Module Λ M] {S : Set M}
    (hgen : closure (Submodule.span Λ S : Set M) = Set.univ) (hS : S.Finite) :
    HasGeneratingSetConvergingToZero Λ M

theorem

hasGeneratingSetConvergingToZero_of_dense_addSubgroup

L125 ↗

CompletedGroupAlgebra.hasGeneratingSetConvergingToZero_of_dense_addSubgroup

Documentation

A dense additive generating set is also a dense module generating set.

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 hasGeneratingSetConvergingToZero_of_dense_addSubgroup
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M] [AddCommGroup M]
    [Module Λ M] {S : Set M}
    (hspan : closure (((AddSubgroup.closure S : AddSubgroup M) : Set M)) = Set.univ)
    (hconv : SetConvergesToZero S) :
    HasGeneratingSetConvergingToZero Λ M

def

multiplicativeHomeomorph

L149 ↗

CompletedGroupAlgebra.multiplicativeHomeomorph

Documentation

The multiplicative homeomorphism identifies the additive profinite-module structure with its multiplicative notation.

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 multiplicativeHomeomorph (M : Type*) [TopologicalSpace M] : M ≃ₜ Multiplicative M where
  toEquiv := Multiplicative.ofAdd
  continuous_toFun := continuous_ofAdd
  continuous_invFun := continuous_toAdd

theorem

profiniteModule_hasGeneratingSetConvergingToZero

L155 ↗

CompletedGroupAlgebra.profiniteModule_hasGeneratingSetConvergingToZero

Documentation

In Lemma 5.1.1(c), every profinite module has a generating set converging to 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 profiniteModule_hasGeneratingSetConvergingToZero
    (Λ : 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] :
    HasGeneratingSetConvergingToZero Λ M

Module documentation

Generating sets converging to zero

Declarations