rightDerivedZeroIsoSelf_hom_inv_id

English

For each X, the hom component of the isomorphism composed with the app X equals the identity on the target.

Русский

Для каждого X отображение гомоморфизма канонического изоморфизма, умноженное на app X, дает тождественный морфизм на целевом объекте.

LaTeX

$$F.rightDerivedZeroIsoSelf.hom.app X ≫ F.toRightDerivedZero.app X = 𝟙 _$$

Lean4

@[reassoc (attr := simp)]
theorem rightDerivedZeroIsoSelf_hom_inv_id : F.rightDerivedZeroIsoSelf.hom ≫ F.toRightDerivedZero = 𝟙 _ :=
  F.rightDerivedZeroIsoSelf.hom_inv_id

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