English
In locally small categories, for a final functor F : C → D and arrows s,s' : d → F.obj c, there exists c' and t: c ⟶ c' such that s ≫ F.map t = s' ≫ F.map t.
Русский
В локально малой категории, для финального функторa F : C → D и стрел s,s' : d → F(c), существует c' и t: c ⟶ c' такое, что s ≫ F(t) = s' ≫ F(t).
LaTeX
$$[(IsFilteredOrEmpty C) (Final F)] {d : D} {c : C} (s s' : d ⟶ F.obj c) → ∃(c' : C)(t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t$$
Lean4
/-- Implementation; use `Functor.Final.exists_coeq instead`. -/
theorem exists_coeq_of_locally_small [IsFilteredOrEmpty C] [Final F] {d : D} {c : C} (s s' : d ⟶ F.obj c) :
∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t :=
by
have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' :=
by
apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
subsingleton
obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]
dsimp only [comp_obj, coyoneda_obj_obj, unop_op, Functor.comp_map, coyoneda_obj_map] at h
simp [reassoc_of% h]
