English
The map on the second short complex H2 is compatible with composition of maps: mapShortComplexH2 (g ∘ f) (φ ≫ (Res f).map ψ) equals the composition of mapShortComplexH2 f φ and mapShortComplexH2 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
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map from the short complex
`(G × G × G →₀ A) --d₃₂--> (G × G →₀ A) --d₂₁--> (G →₀ A)` to
`(H × H × H →₀ B) --d₃₂--> (H × H →₀ B) --d₂₁--> (H →₀ B)`. -/
@[simps]
noncomputable def mapShortComplexH2 : shortComplexH2 A ⟶ shortComplexH2 B
where
τ₁ := chainsMap₃ f φ
τ₂ := chainsMap₂ f φ
τ₃ := chainsMap₁ f φ
comm₁₂ := by
simp only [shortComplexH2]
ext : 3
simpa [d₃₂, map_add, map_sub, ← map_inv] using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))
comm₂₃ := by
simp only [shortComplexH2]
ext : 3
simpa [d₂₁, map_add, map_sub, ← map_inv] using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))
