Module

FiniteRankSourceData.lean

Nyll.ProCGroups.FreeProC.FiniteRankSourceData

2 declarations indexed from sourceView source ↗

Module documentation

Finite-rank free pro-C source data

This module packages a finite-rank epimorphically free pro-\(C\) group as the canonical source-data structure and records the cardinality of its lifted finite basis.

Imports1

Nyll.ProCGroups.FreeProC.FiniteBasis

Imported by2

def

finiteRank_epimorphicallyFreeProCSourceData

L25 ↗

CrowellExactSequence.finiteRank_epimorphicallyFreeProCSourceData

Documentation

Package a finite-rank epimorphically free pro-\(\Sigma\) group using the canonical ProCGroups source-data structure.

Source context 4 commands

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

namespace CrowellExactSequence
universe u
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]

Lean source · statement

def finiteRank_epimorphicallyFreeProCSourceData
    {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
    (hFree : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
      (Fin r) F X) :
    ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
      (ProCGroups.FiniteGroupClass.sigmaGroup sigma)

theorem

finiteRank_epimorphicallyFreeProCSourceData_basis_card

L88 ↗

CrowellExactSequence.finiteRank_epimorphicallyFreeProCSourceData_basis_card