English
For maps f and g, the map on H2 respects composition: mapShortComplexH2 (g ∘ f) (φ ≫ (Res f).map ψ) equals (mapShortComplexH2 f φ) ≫ (mapShortComplexH2 g ψ).
Русский
Для отображений f и g отображение на H2 уважает композицию: mapShortComplexH2(g ∘ f)(φ ≫ (Res f).map ψ) = mapShortComplexH2 f φ ∘ mapShortComplexH2 g ψ.
LaTeX
$$$ mapShortComplexH2(g \cdot f)(\varphi \;\mathrm{≫}\; (\mathrm{Res}\, f).map(\psi)) = (mapShortComplexH2 f \varphi) \;\mathrm{≫}\; (mapShortComplexH2 g \psi) $$$
Lean4
theorem mapShortComplexH2_comp {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k G} {B : Rep k H} {C : Rep k K}
(f : G →* H) (g : H →* K) (φ : A ⟶ (Action.res _ f).obj B) (ψ : B ⟶ (Action.res _ g).obj C) :
mapShortComplexH2 (g.comp f) (φ ≫ (Action.res _ f).map ψ) = (mapShortComplexH2 f φ) ≫ (mapShortComplexH2 g ψ) :=
by
refine ShortComplex.hom_ext _ _ ?_ ?_ ?_
all_goals {
simp only [shortComplexH2]
ext
simp [Prod.map]
}
