eqvGen_colimitTypeRel_of_rel — Mathlib

English

Let F : J ⥤ Type be a diagram. If x,y are elements of Σ j, F.obj j and relate by FilteredColimit.Rel, then x and y are related by the equivalence generated by ColimitTypeRel, i.e., EqvGen F.ColimitTypeRel x y.

Русский

Пусть F : J ⥤ Type — диаграмма. Если P = (x,y) ∈ Σ j, F.obj j и P относится по FilteredColimit.Rel, то x и y эквивалентны по порождённому отношению EqvGen F.ColimitTypeRel.

LaTeX

$$$\mathrm{FilteredColimit.Rel}(F,x,y) \Rightarrow \mathrm{Relation.EqvGen}(F.{\text{ColimitTypeRel}})(x,y)$$$

Lean4

theorem eqvGen_colimitTypeRel_of_rel (x y : Σ j, F.obj j) :
    FilteredColimit.Rel.{v, u} F x y → Relation.EqvGen F.ColimitTypeRel x y := fun ⟨k, f, g, h⟩ =>
  by
  refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_
  · exact (Relation.EqvGen.rel _ _ ⟨f, rfl⟩)
  · exact (Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, h⟩))

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