FoxDifferential.primePowerCompletedGroupAlgebraMap_of
The completed prime-power group-algebra map sends the group-like element of g to the group-like element of ψ g.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [Fact (0 < ℓ)] inLean source · statement
theorem primePowerCompletedGroupAlgebraMap_of
(ψ : ContinuousMonoidHom G H) (g : G) :
primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g) =
primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g)