All.lean
Nyll.ProCGroups.InverseSystems.All
0 declarations indexed from sourceView source ↗
Module documentation
Inverse systems
This aggregate module exposes inverse systems of topological groups, categorical and profinite limits, exactness and factorization results, quotient systems, and stagewise comparison isomorphisms.
Imports15
- Nyll.ProCGroups.InverseSystems.Basic
- Nyll.ProCGroups.InverseSystems.CategoricalLimits
- Nyll.ProCGroups.InverseSystems.CofinalityAndDensity
- Nyll.ProCGroups.InverseSystems.CompatibilityAndSurjectivity
- Nyll.ProCGroups.InverseSystems.CountableModels
- Nyll.ProCGroups.InverseSystems.Exactness
- Nyll.ProCGroups.InverseSystems.FiniteStageFactorization
- Nyll.ProCGroups.InverseSystems.ProfiniteLimits
- Nyll.ProCGroups.InverseSystems.ProfiniteSpace
- Nyll.ProCGroups.InverseSystems.ProjectionImageSystems
- Nyll.ProCGroups.InverseSystems.Quotients
- Nyll.ProCGroups.InverseSystems.StagewiseIso
- Nyll.ProCGroups.InverseSystems.Utilities
- Nyll.ProCGroups.InverseSystems.GroupSystemRestriction
- Nyll.ProCGroups.InverseSystems.CofinalGroups
Imported by1
This module has no indexed declarations. Its imports and full source are available here.