All.lean
Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.All
0 declarations indexed from sourceView source ↗
Module documentation
Completed Group Algebra / All Finite Functoriality
This aggregate exports functoriality of the all-finite completed group algebra for continuous group homomorphisms: inverse-image quotient indices, finite-stage and completed algebra maps, group-like compatibility, surjectivity, and naturality of the comparison with \(C\)-indexed completions.
Imports6
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
- Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
Imported by1
This module has no indexed declarations. Its imports and full source are available here.