Source: ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality
1import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Surjectivity
2import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
3import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike
5/-!
6# Completed Group Algebra / All Finite Functoriality
8This aggregate exports functoriality of the all-finite completed group algebra for continuous group
9homomorphisms: inverse-image quotient indices, finite-stage and completed algebra maps, group-like
10compatibility, surjectivity, and naturality of the comparison with \(C\)-indexed completions.
11-/