ModuleQuasifree.lean
Nyll.ProCGroups.FreeProC.Characterization.Quasifree
3 declarations indexed from sourceView source ↗ Module documentation
Pro C Groups / Free pro-C / Characterization / Quasifree
This module formulates quasifree proper-solution growth and its cardinal monotonicity consequences.
Declarations
ProCGroups.FreeProC.Characterization.HasTopologicalGeneratingSetOfCardinality
DocumentationA topological group has a topological generating set of cardinality \(\kappa\).
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Cardinal
namespace ProCGroups.FreeProC.Characterization
universe u
ProCGroups.FreeProC.Characterization.HasQuasifreeProperSolutionProperty
DocumentationA group has the quasifree proper-solution property at rank \(\kappa\) for finite split \(C\)-embedding problems.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Cardinal
namespace ProCGroups.FreeProC.Characterization
universe u
ProCGroups.FreeProC.Characterization.IsQuasifreeOfRank
DocumentationQuasifreeness at infinite rank \(\kappa\). The rank field is deliberately topological: in profinite contexts an abstract generating set is too weak and does not control the closed subgroup generated by the chosen family. The lifting field records the standard proper-solution condition for finite split embedding problems.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Cardinal
namespace ProCGroups.FreeProC.Characterization
universe u