English
If L ⊣ R is an adjunction and C is cofiltered (or empty), then D inherits cofiltered-ness.
Русский
Если L ⊣ R — адъюнкция и C кофильтрована (или пустая), тогда D тоже кофильтрована.
LaTeX
$$$$ \\text{IsCofilteredOrEmpty}(D) \\text{ from } \\text{IsCofilteredOrEmpty}(C) \\text{ via } L \\dashv R. $$$$
Lean4
/-- If `C` is cofiltered or empty, and we have a functor `L : C ⥤ D` with a right adjoint,
then `D` is cofiltered or empty.
-/
theorem of_left_adjoint {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) : IsCofilteredOrEmpty D :=
{ cone_objs := fun X Y =>
⟨L.obj (min (R.obj X) (R.obj Y)), (h.homEquiv _ X).symm (minToLeft _ _), (h.homEquiv _ Y).symm (minToRight _ _),
⟨⟩⟩
cone_maps := fun X Y f g =>
⟨L.obj (eq (R.map f) (R.map g)), (h.homEquiv _ _).symm (eqHom _ _), by
rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]⟩ }
