mkNatIso_eq — Mathlib

English

Naturality of iso_hom in CatCommSqOver with respect to a morphism f in X: the natural transformation hom respects the map between F and G via the isomorphism S.iso.hom.

Русский

Естественность гомоморфизма изоморфии в CatCommSqOver по отношению к морфизму f в X: натуральное преобразование гомоморфизма сохраняет связь между F и G через S.iso.hom.

LaTeX

$$$ S.iso.hom.naturality f$$$

Lean4

/-- Comparing mkNatIso with the corresponding construction one can deduce from
`functorEquiv`. -/
theorem mkNatIso_eq :
    mkNatIso e₁ e₂ coh =
      (functorEquiv F G X).fullyFaithfulFunctor.preimageIso
        (CategoricalPullback.mkIso e₁ e₂ (by simpa [functorEquiv, toCatCommSqOver] using coh)) :=
  by
  rw [← toCatCommSqOver_mapIso_mkNatIso_eq_mkIso e₁ e₂ coh]
  dsimp [Equivalence.fullyFaithfulFunctor]
  cat_disch

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