rel_eq_eqvGen_colimitTypeRel — Mathlib

English

Let t be a colimit cocone for F. Then t.ι.app i xi equals t.ι.app j xj exactly when there exists a common apex k with maps from i and j to k sending xi and xj to the same element under F.

Русский

Пусть t — колимитный кокон для F. Тогда t.ι.app i xi равно t.ι.app j xj тогда и только тогда, когда существует общее апекс-объект k с стрелками i→k и j→k, переводящими xi и xj в один общий элемент F.

LaTeX

$$$\\forall i,j,\\forall \\xi\\in F(i),\\forall x_j\\in F(j):\\quad t.ι_i(\\xi)=t.ι_j(x_j)\\ \\Longleftrightarrow\\ \\exists k,f,g:\\ i\\to k, j\\to k, F.map f(\\xi)=F.map g(x_j)$$$

Lean4

protected theorem rel_eq_eqvGen_colimitTypeRel : FilteredColimit.Rel.{v, u} F = Relation.EqvGen F.ColimitTypeRel :=
  by
  ext ⟨j, x⟩ ⟨j', y⟩
  constructor
  · apply eqvGen_colimitTypeRel_of_rel
  · rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F)

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