conePointUniqueUpToIso_hom_comp — Mathlib

English

For a limit IsLimit hc and any j, the morphism from the cone point unique iso, composed with limit.π F j, equals c.π.app j.

Русский

Для IsLimit hc и любого j, композиция harris from conePointUniqueUpToIso с π_j равна конусному π_j.

LaTeX

$$$(\\mathrm{hc}.conePointUniqueUpToIso (\\mathrm{limit}.isLimit F)).hom \\;\\circ\\; \\mathrm{limit}.π F j = c.π.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem conePointUniqueUpToIso_hom_comp {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) :
    (IsLimit.conePointUniqueUpToIso hc (limit.isLimit _)).hom ≫ limit.π F j = c.π.app j :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

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