leftDerivedZeroIsoSelf_inv_hom_id

English

For every X, the inverse side of the canonical isomorphism composed with the forward side yields the identity on X, at the level of app X.

Русский

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

LaTeX

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

Lean4

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

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