isoLimitCone_hom_π — Mathlib

English

For a limit cone t of F, the hom component of limit isoLimitCone t followed by t.cone.π app j equals limit.π F j; this confirms the defining property of the isoLimitCone.

Русский

Для предела-конуса t функтор F, композиция limitIsoCone t.hom и t.cone.π j равна limit.π F j.

LaTeX

$$$(\\mathrm{limit}.isoLimitCone t).hom \\;\\circ\\; t.cone.π app j = \\mathrm{limit}.π F j$$$

Lean4

@[reassoc (attr := simp)]
theorem isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j :=
  by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  simp

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