English
The map that sends an i-cochain to the corresponding i-th cochain in B, given a group homomorphism f and a morphism φ: Res(f)(A) → B, is the chain map between inhomogeneous cochains A and B.
Русский
Отображение, переводящее i-коцепу в соответствующую i-коцепу в B, задаётся групповым гомоморфизмом f и морфизмом φ: Res(f)(A) → B; это цепное отображение между неоднородными коцепами A и B.
LaTeX
$$$$ \\text{cochainsMap } f \\phi : \\text{inhomogeneousCochains}(A) \\to \\text{inhomogeneousCochains}(B). $$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the chain map sending `x : Hⁿ → A` to `(g : Gⁿ) ↦ φ (x (f ∘ g))`. -/
@[simps! -isSimp f f_hom]
noncomputable def cochainsMap : inhomogeneousCochains A ⟶ inhomogeneousCochains B
where
f i := ModuleCat.ofHom <| φ.hom.hom.compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k A (fun x : Fin i → G => (f ∘ x))
comm' i j
(hij : _ = _) := by
subst hij
ext
simpa [inhomogeneousCochains.d_hom_apply, Fin.comp_contractNth] using (hom_comm_apply φ _ _).symm
