cone_π — Mathlib

English

For a limit cone t of F, the hom component of the isoLimitCone from t to the canonical limit agrees with the limit projection: (limit.isoLimitCone t).hom ≫ t.cone.π j = limit.π F j.

Русский

Для предела-конуса t предела F, композиция гом-части из isoLimitCone с π j совпадает с limit.π F j.

LaTeX

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

Lean4

@[simp]
theorem cone_π {F : J ⥤ C} [HasLimit F] : (limit.cone F).π.app = limit.π _ :=
  rfl

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