English
Let f be a group homomorphism G →* H and φ, ψ be morphisms of representations A → Res(f)(B) and B → Res(f)(C). Then the induced map on H1 is compatible with composition, i.e. the map induced by the composite φ ≫ ψ equals the composite of the maps induced by φ and ψ, after applying the identity on G.
Русский
Пусть f : G →* H — гомоморфизм групп, а φ, ψ — морфизмы репрезентаций A → Res(f)(B) и B → Res(f)(C). Тогда отображение индуцированное на H1 совместимо с композициями: отображение, индуцированное φ ≫ ψ, равно композиции индуцированных φ и ψ, когда применено тождественное отображение на G.
LaTeX
$$$ mapShortComplexH1(\mathrm{id}_G)(\varphi \;\mathrm{\,≫\} \psi) = mapShortComplexH1(\mathrm{id}_G)\varphi \;\mathrm{\,≫\} mapShortComplexH1(\mathrm{id}_G)\psi $$$
Lean4
theorem mapShortComplexH1_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
mapShortComplexH1 (MonoidHom.id G) (φ ≫ ψ) =
mapShortComplexH1 (MonoidHom.id G) φ ≫ mapShortComplexH1 (MonoidHom.id G) ψ :=
mapShortComplexH1_comp (MonoidHom.id G) (MonoidHom.id G) _ _
