conePointsIsoOfNatIso_hom_comp — Mathlib

English

For two functors F and G with cones s and t and a natural isomorphism w, the wrenching of the cone points along w respects the projections: (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j for all j.

Русский

Для F и G с конусами s и t и натурального изоморфизма w отображение конусных точек согласуется с проекциями: (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j для всех j.

LaTeX

$$$ (conePointsIsoOfNatIso\, P\, Q\, w).hom \\circ t.\\pi_{j} = s.\\pi_{j} \\circ w.hom_{j} $$$

Lean4

@[reassoc]
theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
    (w : F ≅ G) (j : J) : (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j := by simp

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