coconePointUniqueUpToIso_inv_desc

English

For functors F,G with cocones s,t and a natural isomorphism w: F ≅ G, the inverse component maps desc r through P to Q via map and inv components: (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map r w.inv.

Русский

Пусть F,G — функторы, s,t — коконы, w: F ≅ G — натуральная изоморфизм. Тогда обратный компонент изоморфизма преобразует-desc- через P к Q: (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map r w.inv.

LaTeX

$$$ (coconePointsIsoOfNatIso P Q w).inv \; ≫ \; P.desc r = Q.map \; r \; w.inv $$$

Lean4

@[reassoc (attr := simp)]
theorem coconePointUniqueUpToIso_inv_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
    (coconePointUniqueUpToIso P Q).inv ≫ P.desc r = Q.desc r :=
  Q.uniq _ _ (by simp)

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