fac — Mathlib

English

For a multicofork K over a multispan I, the components π_a composed with the universal IsColimit desc equals the corresponding k(a).

Русский

Для мультикофорка K над мультипрана I компоненты π_a после применения IsColimit.desc равны соответствующему k(a).

LaTeX

$$$K.\pi_a \;\circ\; \mathrm{IsColimit.desc}\; h_K\; k\; hk = k_a.$$$

Lean4

@[reassoc (attr := simp)]
theorem fac (hK : IsColimit K) {T : C} (k : ∀ a, I.right a ⟶ T)
    (hk : ∀ b, I.fst b ≫ k (J.fst b) = I.snd b ≫ k (J.snd b)) (a : J.R) : K.π a ≫ IsColimit.desc hK k hk = k a :=
  hK.fac _ _

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