rel_of_colimitTypeRel — Mathlib

English

Let F : J ⥤ Type be a diagram indexed by a category J, and let x and y be elements of the sigma-type Σ j, F.obj j. If x and y are related by the ColimitTypeRel, then they are related in the filtered colimit relation of F.

Русский

Пусть F : J ⥤ Type — диаграмма, индексируемая категорией J, и пусть x, y — элементы совокупности Σ j, F.obj j. Если x и y связаны отношением ColimitTypeRel, то они связаны отношением FilteredColimit.Rel для F.

LaTeX

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

Lean4

theorem rel_of_colimitTypeRel (x y : Σ j, F.obj j) : F.ColimitTypeRel x y → FilteredColimit.Rel.{v, u} F x y :=
  fun ⟨f, h⟩ => ⟨y.1, f, 𝟙 y.1, by rw [← h, FunctorToTypes.map_id_apply]⟩

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