English
In a filtered category, given a finite set of objects and a finite collection of morphisms among them, there exists a common right object S and morphisms from each X to S that render all specified triangles commutative.
Русский
В фильтрованной категории существует общий правый объект S и стрелки X ⟶ S от каждого X из конечного множества так, чтобы все заданные треугольники коммутировали.
LaTeX
$$$\exists S . \forall X \in O, \exists f_X : X ⟶ S, \text{ и далее треугольники коммутируют }$$$
Lean4
/-- If `C` is filtered or empty, and we have a functor `R : C ⥤ D` with a left adjoint, then `D` is
filtered or empty.
-/
theorem of_right_adjoint {L : D ⥤ C} {R : C ⥤ D} (h : L ⊣ R) : IsFilteredOrEmpty D :=
{ cocone_objs := fun X Y =>
⟨R.obj (max (L.obj X) (L.obj Y)), h.homEquiv _ _ (leftToMax _ _), h.homEquiv _ _ (rightToMax _ _), ⟨⟩⟩
cocone_maps := fun X Y f g =>
⟨R.obj (coeq (L.map f) (L.map g)), h.homEquiv _ _ (coeqHom _ _), by
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]⟩ }
