colimit_eq — Mathlib

English

As above, for any F: J → Type u and IsColimit t, the colimit cocone t is jointly surjective: every element of t lies in the image of some t.ι.app j.

Русский

Как и выше, для F: J → Type u и IsColimit t, кокон колимита совместно сюръективен: каждый элемент t принадлежит образу некоторого t.ι.app j.

LaTeX

$$$$ \forall x \in t.pt, \exists j, y: F(j), t.ι.app j y = x. $$$$

Lean4

theorem colimit_eq {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : colimit.ι F j x = colimit.ι F j' x') :
    Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', x'⟩ :=
  by
  apply Quot.eq.1
  simpa using congr_arg (colimitEquivColimitType F) w

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