lift_ι — Mathlib

English

Let f,g: X → Y be a parallel pair in a category. If s is a limit fork for the pair (f,g) and t is any fork for (f,g), then there exists a unique mediating morphism hs.lift t: t.pt → s.pt such that hs.lift t ≫ s.ι = t.ι.

Русский

Пусть f,g: X → Y образуют параллельную пару в категории. Если s является пределом-форком для пары (f,g) и t — произвольный форк этой пары, тогда существует единственный медиатор hs.lift t: t.pt → s.pt такой, что hs.lift t ≫ s.ι = t.ι.

LaTeX

$$$\operatorname{IsLimit}(s) \Rightarrow \forall t:\, \mathrm{Fork}(f,g),\ (\text{lift}_{s}(t))\,;\; s.\iota = t.\iota$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_ι {s t : Fork f g} (hs : IsLimit s) : hs.lift t ≫ s.ι = t.ι :=
  hs.fac _ _

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