English
For a diagram F : J ⥤ Type with IsFilteredOrEmpty J, the relation Rel F on the colimit type is equal to the equivalence relation generated by F.ColimitTypeRel.
Русский
Для диаграммы F : J ⥤ Type с IsFilteredOrEmpty J, отношение Rel F на типе колимита совпадает с эквивалентностью, порождаемой F.ColimitTypeRel.
LaTeX
$$$\\text{FilteredColimit.Rel}(F) = \\text{Relation.EqvGen}(F.ColimitTypeRel)$$$
Lean4
protected theorem rel_equiv : _root_.Equivalence (FilteredColimit.Rel.{v, u} F)
where
refl x := ⟨x.1, 𝟙 x.1, 𝟙 x.1, rfl⟩
symm := fun ⟨k, f, g, h⟩ => ⟨k, g, f, h.symm⟩
trans
{x y z} := fun ⟨k, f, g, h⟩ ⟨k', f', g', h'⟩ =>
let ⟨l, fl, gl, _⟩ := IsFilteredOrEmpty.cocone_objs k k'
let ⟨m, n, hn⟩ := IsFilteredOrEmpty.cocone_maps (g ≫ fl) (f' ≫ gl)
⟨m, f ≫ fl ≫ n, g' ≫ gl ≫ n,
calc
F.map (f ≫ fl ≫ n) x.2 = F.map (fl ≫ n) (F.map f x.2) := by simp
_ = F.map (fl ≫ n) (F.map g y.2) := by rw [h]
_ = F.map ((g ≫ fl) ≫ n) y.2 := by simp
_ = F.map ((f' ≫ gl) ≫ n) y.2 := by rw [hn]
_ = F.map (gl ≫ n) (F.map f' y.2) := by simp
_ = F.map (gl ≫ n) (F.map g' z.2) := by rw [h']
_ = F.map (g' ≫ gl ≫ n) z.2 := by simp⟩
