English
Induced map between the two-term exact sequences on i, coming from a morphism φ.
Русский
Индукцированное отображение между двумя стрелами точной последовательности на i, которое идёт от морфизма φ.
LaTeX
$$mapComposableArrows₂ φ i$$
Lean4
/-- The map `composableArrows₅ hS₁ i j hij ⟶ composableArrows₅ hS₂ i j hij` of exact
sequences induced by a morphism `φ : S₁ ⟶ S₂` between short exact short complexes of
homological complexes. -/
@[simp]
noncomputable def mapComposableArrows₅ (i j : ι) (hij : c.Rel i j) :
composableArrows₅ hS₁ i j hij ⟶ composableArrows₅ hS₂ i j hij :=
homMk₅ (homologyMap φ.τ₁ i) (homologyMap φ.τ₂ i) (homologyMap φ.τ₃ i) (homologyMap φ.τ₁ j) (homologyMap φ.τ₂ j)
(homologyMap φ.τ₃ j) (naturality' (mapComposableArrows₂ φ i) 0 1) (naturality' (mapComposableArrows₂ φ i) 1 2)
(δ_naturality φ hS₁ hS₂ i j hij) (naturality' (mapComposableArrows₂ φ j) 0 1)
(naturality' (mapComposableArrows₂ φ j) 1 2)
