single₀_map_f_zero — Mathlib

English

For a morphism f: A ⟶ B, the 0th component of the induced map on the single₀ complex is precisely f.

Русский

Для морфизма f: A ⟶ B нулевая компонента индуцированного отображения на когайнко́вом single₀ равна самому f.

LaTeX

$$$((\\mathrm{single}_0 V).\\mathrm{map} f)_0 = f$$$

Lean4

@[simp]
theorem single₀_map_f_zero {A B : V} (f : A ⟶ B) : ((single₀ V).map f).f 0 = f :=
  by
  rw [HomologicalComplex.single_map_f_self]
  dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]
  rw [comp_id, id_comp]

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