single₀ObjXSelf — Mathlib

English

The canonical isomorphism from the 0th level of the singleton object is the identity isomorphism.

Русский

Каноническое изоморфизм от нулевого уровня единичного объекта является тождественным изоморфизмом.

LaTeX

$$$$ \mathrm{singleObjXSelf}(\text{ComplexShape.down } \mathbb{N})\ 0\ X = \mathrm{Iso.refl}(\text{...}) $$$$

Lean4

@[simp]
theorem single₀ObjXSelf (X : V) : HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X = Iso.refl _ :=
  rfl

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