NYLL
Module

Definitions.lean

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.Definitions
12 declarations indexed from sourceView source ↗

Module documentation

Bundled profinite rings and modules

This file defines profinite rings, commutative profinite coefficient rings, and profinite modules. It also states their free-extension, discreteness, and finite-index submodule-basis properties.

Imports5
Imported by2

Declarations

structure

ProfiniteRing

L28 ↗
CompletedGroupAlgebra.ProfiniteRing
Documentation

A profinite ring object. Its standard algebraic and topological structures are stored once on the carrier.

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
structure ProfiniteRing where
  /-- The underlying profinite space. -/
  toProfinite : Profinite.{u}
  /-- The ring structure on the underlying profinite space. -/
  [ring : Ring toProfinite]
  /-- The assertion that the ring operations are continuous. -/
  [isTopologicalRing : IsTopologicalRing toProfinite]
instance

(anonymous instance)

L41 ↗
Documentation

A bundled profinite ring coerces to its underlying profinite type.

Source context 5 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
namespace ProfiniteRing
Lean source · full declaration
instance : CoeSort ProfiniteRing.{u} (Type u) where
  coe Λ := Λ.toProfinite
structure

ProfiniteCommRing

L49 ↗
CompletedGroupAlgebra.ProfiniteCommRing
Documentation

A commutative profinite ring, used as the coefficient object for completed group algebras. The completed algebra itself may be noncommutative and therefore uses ProfiniteRing. This separate bundle avoids installing a second Ring instance on ProfiniteRing.

Source context 4 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
Lean source · full declaration
structure ProfiniteCommRing where
  /-- The underlying profinite space. -/
  toProfinite : Profinite.{u}
  /-- The commutative ring structure on the underlying profinite space. -/
  [commRing : CommRing toProfinite]
  /-- The assertion that the ring operations are continuous. -/
  [isTopologicalRing : IsTopologicalRing toProfinite]
instance

(anonymous instance)

L62 ↗
Documentation

A bundled profinite commutative ring coerces to its underlying profinite type.

Source context 6 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
namespace ProfiniteCommRing
Lean source · full declaration
instance : CoeSort ProfiniteCommRing.{u} (Type u) where
  coe R := R.toProfinite
def

toProfiniteRing

L66 ↗
CompletedGroupAlgebra.ProfiniteCommRing.toProfiniteRing
Documentation

Forget commutativity while retaining the bundled profinite ring object.

Source context 6 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
namespace ProfiniteCommRing
Lean source · full declaration
def toProfiniteRing (R : ProfiniteCommRing.{u}) : ProfiniteRing.{u} where
  toProfinite := R.toProfinite
  ring := inferInstance
  isTopologicalRing := inferInstance
def

IsTopologicalModuleOver

L74 ↗
CompletedGroupAlgebra.IsTopologicalModuleOver
Documentation

A topological module over a topological ring.

Source context 5 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
Lean source · statement
def IsTopologicalModuleOver (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
    [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop
structure

ProfiniteModule

L79 ↗
CompletedGroupAlgebra.ProfiniteModule
Documentation

A profinite module object over a fixed profinite ring.

Source context 5 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
Lean source · full declaration
structure ProfiniteModule (Λ : ProfiniteRing.{u}) where
  /-- The underlying profinite space. -/
  toProfinite : Profinite.{v}
  /-- The additive commutative group structure on the underlying profinite space. -/
  [addCommGroup : AddCommGroup toProfinite]
  /-- The \(\Lambda\)-module structure on the underlying profinite space. -/
  [module : Module Λ toProfinite]
  /-- The assertion that addition and negation are continuous. -/
  [isTopologicalAddGroup : IsTopologicalAddGroup toProfinite]
  /-- The assertion that scalar multiplication by \(\Lambda\) is jointly continuous. -/
  [continuousSMul : ContinuousSMul Λ toProfinite]
instance

(anonymous instance)

L99 ↗
Documentation

A bundled profinite module coerces to its underlying profinite type.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
attribute [instance] ProfiniteModule.addCommGroup
attribute [instance] ProfiniteModule.module
attribute [instance] ProfiniteModule.isTopologicalAddGroup
attribute [instance] ProfiniteModule.continuousSMul
namespace ProfiniteModule
Lean source · full declaration
instance (Λ : ProfiniteRing.{u}) : CoeSort (ProfiniteModule.{u, v} Λ) (Type v) where
  coe M := M.toProfinite
def

HasFreeLiftTo

L104 ↗
CompletedGroupAlgebra.ProfiniteModule.HasFreeLiftTo
Documentation

The extension-and-uniqueness property from a candidate free profinite module to one bundled target. Keeping the target as an argument makes this API universe-polymorphic without ULift.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
attribute [instance] ProfiniteModule.addCommGroup
attribute [instance] ProfiniteModule.module
attribute [instance] ProfiniteModule.isTopologicalAddGroup
attribute [instance] ProfiniteModule.continuousSMul
namespace ProfiniteModule
Lean source · statement
def HasFreeLiftTo {Λ : ProfiniteRing.{u}} (M : ProfiniteModule.{u, w} Λ)
    (X : Type v) [TopologicalSpace X] (ι : X → M)
    (N : ProfiniteModule.{u, z} Λ) : Prop
def

IsFreeOn

L113 ↗
CompletedGroupAlgebra.ProfiniteModule.IsFreeOn
Documentation

Universal-property predicate for a free profinite module in a fixed ambient universe. Cross-universe targets use HasFreeLiftTo directly. The scalar, generator, and source/target modules are bundled objects, so their profiniteness is part of the statement.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
attribute [instance] ProfiniteModule.addCommGroup
attribute [instance] ProfiniteModule.module
attribute [instance] ProfiniteModule.isTopologicalAddGroup
attribute [instance] ProfiniteModule.continuousSMul
namespace ProfiniteModule
Lean source · statement
def IsFreeOn {Λ : ProfiniteRing.{u}} (M : ProfiniteModule.{u, w} Λ)
    (X : Profinite.{v}) (ι : X → M) : Prop
def

IsDiscreteModule

L122 ↗
CompletedGroupAlgebra.IsDiscreteModule
Documentation

A topological module whose underlying module topology is discrete.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
attribute [instance] ProfiniteModule.addCommGroup
attribute [instance] ProfiniteModule.module
attribute [instance] ProfiniteModule.isTopologicalAddGroup
attribute [instance] ProfiniteModule.continuousSMul
Lean source · statement
def IsDiscreteModule (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ]
    [AddCommGroup M] [TopologicalSpace M] [Module Λ M] : Prop
def

HasFiniteIndexSubmoduleBasis

L127 ↗
CompletedGroupAlgebra.HasFiniteIndexSubmoduleBasis
Documentation

Finite-index submodules form a neighborhood basis at zero.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
universe u v w z
attribute [instance] ProfiniteRing.ring ProfiniteRing.isTopologicalRing
attribute [instance] ProfiniteCommRing.commRing ProfiniteCommRing.isTopologicalRing
attribute [instance] ProfiniteModule.addCommGroup
attribute [instance] ProfiniteModule.module
attribute [instance] ProfiniteModule.isTopologicalAddGroup
attribute [instance] ProfiniteModule.continuousSMul
Lean source · statement
def HasFiniteIndexSubmoduleBasis (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace M]
    [AddCommGroup M] [Module Λ M] : Prop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.