English
Natural associativity of mapShortComplexH1 with composition: mapShortComplexH1 (g ∘ f) (φ ≫ (Res f).map ψ) equals the composition of mapShortComplexH1 f φ and mapShortComplexH1 g ψ.
Русский
Естественная ассоциативность отображения между короткими комплексами: mapShortComplexH1 (g ∘ f) (φ ≫ (Res f).map ψ) равняется композиции mapShortComplexH1 f φ и mapShortComplexH1 g ψ.
LaTeX
$$$\mathrm{mapShortComplexH1}(g \circ f, \phi \gg (\mathrm{Res}\_f(\psi))) = \mathrm{mapShortComplexH1}(f, \phi) \circ \mathrm{mapShortComplexH1}(g, \psi)$$$
Lean4
theorem mapShortComplexH1_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) :
mapShortComplexH1 (g.comp f) (φ ≫ (Action.res _ f).map ψ) = (mapShortComplexH1 f φ) ≫ (mapShortComplexH1 g ψ) :=
by
refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
all_goals {
simp only [shortComplexH1]
ext
simp [Prod.map]
}
