isoOfNatIso_hom_π — Mathlib

English

Let F, G be functors with limits and w: F ≅ G. Then for each j in J, the hom component of the nat-iso satisfies a compatibility: (HasLimit.isoOfNatIso w).hom ≫ limit.π G j = limit.π F j ≫ w.hom.app j.

Русский

Пусть F, G — функторы с пределами, и w: F ≅ G. Тогда для каждого j в J гом-компонента нат-изоморфизма удовлетворяет совместимости: (HasLimit.isoOfNatIso w).hom ≫ limit.π G j = limit.π F j ≫ w.hom.app j.

LaTeX

$$$(HasLimit.isoOfNatIso w).hom \\gg \\operatorname{limit.}\\pi_G j = \\operatorname{limit.}\\pi_F j \\gg w.hom.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfNatIso_hom_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
    (HasLimit.isoOfNatIso w).hom ≫ limit.π G j = limit.π F j ≫ w.hom.app j :=
  IsLimit.conePointsIsoOfNatIso_hom_comp _ _ _ _

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