fac — Mathlib

English

Let hK be a universal cone (IsLimit) for a multifork K. Given a family of arrows k a: T → I.left a compatible with the legs (hk), the lift from T to K.pt composed with K.ι a equals k a for every a.

Русский

Пусть h_K задает предельную связку для мультфорка K. Пусть дана семейство стрелок k a: T → I.left a, совместимое по ножкам (hk). Тогда подъём из T в K.pt, затем через K.ι a, равен k a для каждого a.

LaTeX

$$$\text{If } h_K:\ IsLimit\ K,\ k:\, \forall a,\ T \to I.left a,\ hk:\; \forall b,\ k(J.fst b) \circ I.fst b = k(J.snd b) \circ I.snd b,\ a:\; IsLimit.lift\ h_K\ k\ hk \circ K.\ι a = k a$$$

Lean4

@[reassoc (attr := simp)]
theorem fac (hK : IsLimit K) {T : C} (k : ∀ a, T ⟶ I.left a) (hk : ∀ b, k (J.fst b) ≫ I.fst b = k (J.snd b) ≫ I.snd b)
    (a : J.L) : IsLimit.lift hK k hk ≫ K.ι a = k a :=
  hK.fac _ _

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