comp_coconePointsIsoOfNatIso_hom — Mathlib

English

For F ≅ G and cocones s,t with IsColimit, the action on legs commutes: s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app j ≫ t.ι.app j.

Русский

Для F ≅ G и коконов s,t с IsColimit выполняется commuting по основаниям: s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app j ≫ t.ι.app j.

LaTeX

$$$ s.\iota.app j \\! ≫ \\! (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app j \\! ≫ \\! t.\iota.app j $$$

Lean4

@[reassoc]
theorem comp_coconePointsIsoOfNatIso_hom {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t)
    (w : F ≅ G) (j : J) : s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).hom = w.hom.app j ≫ t.ι.app j := by simp

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