All.lean
Nyll.ProCGroups.Abelian.All
0 declarations indexed from sourceView source ↗
Module documentation
Abelian constructions
This aggregate module exposes topological abelianization, its functoriality, and its compatibility with inverse limits.
Imports24
- Nyll.ProCGroups.Abelian.PrimeQuotients
- Nyll.ProCGroups.Abelian.AbelianModPower
- Nyll.ProCGroups.Abelian.SubgroupCommutator
- Nyll.ProCGroups.Abelian.Transfer
- Nyll.ProCGroups.Abelian.PrimaryDetection
- Nyll.ProCGroups.Abelian.CharacterDetection
- Nyll.ProCGroups.Abelian.FiniteInvariantQuotients
- Nyll.ProCGroups.Abelian.TopologicalAbelianization
- Nyll.ProCGroups.Abelian.TopologicalAbelianizationKernel
- Nyll.ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
- Nyll.ProCGroups.Abelian.TopologicalAbelianizationLimits
- Nyll.ProCGroups.Abelian.PrimeExponentCharacters
- Nyll.ProCGroups.Abelian.PrimePowerCharacters
- Nyll.ProCGroups.Abelian.TopologicalAbelianizationQuotientFaithfulness
- Nyll.ProCGroups.Abelian.PrimaryTorsion
- Nyll.ProCGroups.Abelian.PowerQuotientAction
- Nyll.ProCGroups.Abelian.FiniteBidual
- Nyll.ProCGroups.Abelian.ProfiniteBidual
- Nyll.ProCGroups.Abelian.FullTateModule
- Nyll.ProCGroups.Abelian.FullTateCharacters
- Nyll.ProCGroups.Abelian.RestrictedTateModule
- Nyll.ProCGroups.Abelian.ProfiniteCharacterCriterion
- Nyll.ProCGroups.Abelian.FiniteCharacterCriterion
- Nyll.ProCGroups.Abelian.RootsOfUnityCharacterCriterion
Imported by1
This module has no indexed declarations. Its imports and full source are available here.