Module

Construction.lean

Nyll.ProCGroups.Completion.Construction

3 declarations indexed from sourceView source ↗

Module documentation

Constructing pro-C completions

The pro-C completion is the quotient of the profinite completion by its pro-C residual core. Its universal property follows from the two actual quotient maps.

Imports10

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.DenseEmbedding
Mathlib.Topology.Order
Nyll.ProCGroups.Completion.UniversalProperty
Nyll.ProCGroups.ProC.Category.Basic
Nyll.ProCGroups.ProC.MaximalQuotients.ResidualCore
Nyll.ProCGroups.ProC.MaximalQuotients.ResidualQuotient
Nyll.ProCGroups.ProC.MaximalQuotients.UniversalProperty
Nyll.ProCGroups.ProC.Quotients.ClosedNormal

Imported by2

def

proCCompletion

L32 ↗

ProCGroups.Completion.proCCompletion

Documentation

The pro-C residual quotient of the profinite completion of an abstract group.

Source context 3 commands

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

namespace ProCGroups.Completion
open ProCGroups.ProC
universe u

Lean source · statement

def proCCompletion
    (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C)
    (G : Type u) [Group G] : ProCGrp C

def

proCCompletionMap

L44 ↗

ProCGroups.Completion.proCCompletionMap

Documentation

The canonical map from a discrete group to its constructed pro-C completion.

Source context 3 commands

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

namespace ProCGroups.Completion
open ProCGroups.ProC
universe u

Lean source · full declaration

def proCCompletionMap
    (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C)
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    G →ₜ* proCCompletion C hForm G where
  toMonoidHom :=
    (QuotientGroup.mk' (proCResidualCore C
      (ProfiniteGrp.ProfiniteCompletion.completion (GrpCat.of G)))).comp
      (ProfiniteGrp.ProfiniteCompletion.eta (GrpCat.of G)).hom
  continuous_toFun := continuous_of_discreteTopology

theorem

proCCompletion_isProCCompletion

L55 ↗

ProCGroups.Completion.proCCompletion_isProCCompletion

Documentation

The residual quotient of the profinite completion has the pro-C universal property.

Source context 3 commands

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

namespace ProCGroups.Completion
open ProCGroups.ProC
universe u

Lean source · statement

theorem proCCompletion_isProCCompletion
    (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C)
    (hHer : FiniteGroupClass.Hereditary C)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [DiscreteTopology G] :
    IsProCCompletion C G (proCCompletion C hForm G)
      (proCCompletionMap C hForm G)

Module documentation

Constructing pro-C completions

Declarations

proCCompletion

proCCompletionMap

proCCompletion_isProCCompletion