CompletedGroupAlgebra.completedGroupAlgebraMap_comp
Lemma 5.3.5(e), composition law for the completed-group-algebra functor.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
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]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]Lean source · statement
theorem completedGroupAlgebraMap_comp
[CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
(φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
(completedGroupAlgebraMap (G := H) (H := K) R ψ hψ).comp
(completedGroupAlgebraMap (G := G) (H := H) R φ hφ) =
completedGroupAlgebraMap (G := G) (H := K) R (ψ.comp φ) (hψ.comp hφ)