English
The chain map associated to the composition g∘f equals the composition of the chain maps: chainsMap(g∘f) (φ ≫ map ψ) = chainsMap f φ ≫ chainsMap g ψ.
Русский
Отображение цепей для композиции совпадает с композицией отображений цепей.
LaTeX
$$chainsMap (g ∘ f) (φ ≫ (Action.res _ f).map ψ) = chainsMap f φ ≫ chainsMap g ψ$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the chain map sending `∑ aᵢ·gᵢ : Gⁿ →₀ A` to `∑ φ(aᵢ)·(f ∘ gᵢ) : Hⁿ →₀ B`. -/
@[simps! -isSimp f f_hom]
noncomputable def chainsMap : inhomogeneousChains A ⟶ inhomogeneousChains B
where
f i := ModuleCat.ofHom <| mapRange.linearMap φ.hom.hom ∘ₗ lmapDomain A k (f ∘ ·)
comm' i j
(hij : _ = _) := by
subst hij
ext
simpa [Fin.comp_contractNth, map_add, inhomogeneousChains.d] using
congr(single _ $((hom_comm_apply φ (_)⁻¹ _).symm))
