id — Mathlib · SciLib

English

The canonical sum of the fst and snd components yields the identity on the mapping cone object: fstφ.1 ∘ inl φ + snd φ ∘ Cochain.ofHom(inr φ) = id_{mappingCone φ}.

Русский

Каноническая сумма компонент fst и snd даёт тождественный morphism на объекте mappingCone φ.

LaTeX

$$$ (fst\varphi).1 \circ inl(\varphi) + (snd\varphi) \circ Cochain.ofHom(inr\varphi) = Cochain.ofHom(I_{mappingCone(\varphi)}). $$$

Lean4

theorem id :
    (fst φ).1.comp (inl φ) (add_neg_cancel 1) + (snd φ).comp (Cochain.ofHom (inr φ)) (add_zero 0) =
      Cochain.ofHom (𝟙 _) :=
  by simp [ext_cochain_from_iff φ (-1) 0 (neg_add_cancel 1)]

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