ι_of_isLimit — Mathlib

English

Given a limit cone ht on a diagram f, the iota morphisms of the biproduct are determined by ht.lift applied to the appropriate cones.

Русский

Пусть ht — предел конуса; тогда морфизмы ι определяются через ht.lift применённый к соответствующим конусам.

LaTeX

$$$$ t.\\ι_j = ht.lift(\\mathrm{Fan.mk}(f(j))\\;\\text{with appropriate conditions}). $$$$

Lean4

theorem ι_of_isLimit {f : J → C} {t : Bicone f} (ht : IsLimit t.toCone) (j : J) :
    t.ι j = ht.lift (Fan.mk _ fun j' => if h : j = j' then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

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