English
For each c', the descent along c'ι_j coincides with c'.ι_j.
Русский
Для каждого c' схождение по компоненте ι_j совпадает с соответствующей компонентой кокона.
LaTeX
$$hc.desc c' (c.ι j) = c'.ι j$$
Lean4
theorem eqvGen_colimitTypeRel_iff_of_isFiltered (x y : (j : J) × (F.obj j)) :
Relation.EqvGen F.ColimitTypeRel x y ↔ ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2 :=
by
constructor
· intro h
induction h with
| rel x y h =>
obtain ⟨f, h⟩ := h
exact ⟨y.1, f, 𝟙 _, by simpa using h.symm⟩
| refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
| symm _ _ _ h =>
obtain ⟨k, f, g, h⟩ := h
exact ⟨k, g, f, h.symm⟩
| trans x y z _ _ h h' =>
obtain ⟨k, f, g, h⟩ := h
obtain ⟨k', f', g', h'⟩ := h'
obtain ⟨l, a, b, h''⟩ := span g f'
refine ⟨l, f ≫ a, g' ≫ b, ?_⟩
rw [FunctorToTypes.map_comp_apply, FunctorToTypes.map_comp_apply _ g', h, ← h', ← FunctorToTypes.map_comp_apply, ←
FunctorToTypes.map_comp_apply, h'']
· rintro ⟨k, f, f', h⟩
apply Relation.EqvGen.trans (y := ⟨k, F.map f' y.2⟩)
· exact .rel _ _ ⟨f, by rw [← h]⟩
· exact .symm _ _ (.rel _ _ ⟨f', rfl⟩)
