leftDerivedZeroIsoSelf_hom_inv_id_app

English

For every X, the inverse of the leftDerivedZeroIsoSelf at X followed by fromLeftDerivedZero at X yields identity on X.

Русский

Для каждого X обратная часть при X, затем fromLeftDerivedZero на X дают тождество на X.

LaTeX

$$$\\forall X,\\ F.leftDerivedZeroIsoSelf.inv.app X \\;\\circ\\; F.fromLeftDerivedZero.app X = \\mathrm{Id}_{X}$$$

Lean4

@[reassoc (attr := simp)]
theorem leftDerivedZeroIsoSelf_hom_inv_id_app (X : C) :
    F.fromLeftDerivedZero.app X ≫ F.leftDerivedZeroIsoSelf.inv.app X = 𝟙 _ :=
  F.leftDerivedZeroIsoSelf.hom_inv_id_app X

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