English
Equality expressing that the composition of maps with identity on the left matches the composition on the right after translating through functoriality.
Русский
Согласование композиций отображений с тождественным слева совпадает с правой композицией после перехода по функториальности.
LaTeX
$$$\\\\mathrm{map}\\\\(\\\\mathrm{id}_G,\\\\mathrm{comp φ ψ}) n = \\\\mathrm{map}\\\\(\\\\mathrm{id}_G, φ) n \\\\circ \\\\mathrm{map}\\\\(\\\\id_G, ψ) n$$$
Lean4
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map sending `x : H × H × H → A` to
`(g₁, g₂, g₃ : G × G × G) ↦ φ (x (f g₁, f g₂, f g₃))`. -/
noncomputable abbrev cochainsMap₃ : ModuleCat.of k (H × H × H → A) ⟶ ModuleCat.of k (G × G × G → B) :=
ModuleCat.ofHom <| φ.hom.hom.compLeft (G × G × G) ∘ₗ LinearMap.funLeft k A (Prod.map f (Prod.map f f))
