single₀_map_f_zero — Mathlib

English

For any morphism f : A ⟶ B, the 0-th component of (single₀ V).map f is f.

Русский

Для любого морфизма f: A ⟶ B, 0-ая компонента (single₀ V).map f равна f.

LaTeX

$$$$ ((\text{single}_0 V).\text{map } f).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]

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