CompletedGroupAlgebra.completedGroupAlgebraMap_surjective_of_surjective
A surjective continuous homomorphism of profinite groups induces a surjective map on completed group algebras.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]Lean source · statement
theorem completedGroupAlgebraMap_surjective_of_surjective
[CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
(φ : G →* H) (hφ : Continuous φ)
(hφsurj : Function.Surjective φ) :
Function.Surjective (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)