of_isLeftAdjoint — Mathlib

English

Let C be a category that is cofiltered or empty, and let L: C → D be a left adjoint functor. Then D is also cofiltered or empty.

Русский

Пусть C — категория, кофильтрована или пустая, и пусть L: C → D — левый сопряжённый функтор. Тогда D тоже кофильтрована или пуста.

LaTeX

$$$\mathrm{IsCofilteredOrEmpty}(C) \land \text{LeftAdjoint}(L: C \to D) \Rightarrow \mathrm{IsCofilteredOrEmpty}(D)$$$

Lean4

/-- If `C` is cofiltered or empty, and we have a left adjoint functor `L : C ⥤ D`, then `D` is
cofiltered or empty. -/
theorem of_isLeftAdjoint (L : C ⥤ D) [L.IsLeftAdjoint] : IsCofilteredOrEmpty D :=
  of_left_adjoint (Adjunction.ofIsLeftAdjoint L)

Похожие утверждения