FoxDifferential.Completed.DifferentialModule.Map.GroupLike
theorem primePowerCompletedGroupAlgebraMap_of
(ψ : ContinuousMonoidHom G H) (g : G) :
primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g) =
primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g)Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
intro i
change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
(primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := G) g)) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := H) (ψ g))
rw [primePowerCompletedGroupAlgebraProjection_map,
primePowerCompletedGroupAlgebraProjection_of,
primePowerCompletedGroupAlgebraMapStage_of,
primePowerCompletedGroupAlgebraProjection_of]
rflProof. Use the completed group-algebra map induced stagewise by the relevant quotient, comap, target, or coefficient map. At each finite stage, supports are sent by the finite quotient homomorphism and coefficients are transported by the given coefficient map when present. Compatibility with refinements gives a map of inverse limits; formulas, group-like elements, augmentation, linearity, and surjectivity are checked on singleton basis elements and extended by finite support and linearity.
□