leftDerivedZeroIsoSelf_hom_inv_id

English

For every X, the composite F.fromLeftDerivedZero.app X ≫ F.leftDerivedZeroIsoSelf.inv.app X equals the identity on F.obj X.

Русский

Для каждого X композиция F.fromLeftDerivedZero.app X с F.leftDerivedZeroIsoSelf.inv.app X равна тождеству на объекте F(X).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem leftDerivedZeroIsoSelf_hom_inv_id : F.fromLeftDerivedZero ≫ F.leftDerivedZeroIsoSelf.inv = 𝟙 _ :=
  F.leftDerivedZeroIsoSelf.hom_inv_id

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