NYLL
Module

Construction.lean

Nyll.ProCGroups.FreeProC.Construction
2 declarations indexed from sourceView source ↗

Module documentation

Constructing free pro-C groups of finite rank

Complete the abstract free group, then take its pro-C residual quotient. The constructed source carries the universal property, rather than assuming one.

Imports7
Imported by3

Declarations

def

finiteFreeProCSource

L27 ↗
ProCGroups.FreeProC.finiteFreeProCSource
Documentation

A free pro-C group on a finite basis, constructed from the abstract free group.

Source context 2 commands

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

namespace ProCGroups.FreeProC
universe u
Lean source · statement
def finiteFreeProCSource
    (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C)
    (hHer : FiniteGroupClass.Hereditary C)
    (X : Type u) [Finite X] :
    EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C
theorem

exists_finiteFreeProCSource_surjection

L44 ↗
ProCGroups.FreeProC.exists_finiteFreeProCSource_surjection
Documentation

A group generated by at most d elements is a quotient of the constructed free source.

Source context 2 commands

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

namespace ProCGroups.FreeProC
universe u
Lean source · statement
theorem exists_finiteFreeProCSource_surjection
    (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C)
    (hHer : FiniteGroupClass.Hereditary C)
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : ProC.HasOpenNormalBasisInClass C G) {d : ℕ}
    (hd : FiniteGeneration.TopologicallyGeneratedByAtMost d G) :
    ∃ ψ : (finiteFreeProCSource C hForm hHer (ULift.{u} (Fin d))).carrier →ₜ* G,
      Function.Surjective ψ

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