mapToComposableArrows_app_0 — Mathlib

English

The 0-th component of the induced morphism equals the first component τ1 of φ.

Русский

0-я компонента индуцированного морфизма равна первой компоненте τ1 φ.

LaTeX

$$$\big(\operatorname{mapToComposableArrows}(\varphi)\big)_0 = \varphi_1^{\tau}$$$

Lean4

@[simp]
theorem mapToComposableArrows_app_0 {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) :
    (ShortComplex.mapToComposableArrows φ).app 0 = φ.τ₁ :=
  rfl

Похожие утверждения