of_right_adjoint — Mathlib

English

If C is filtered and L ⊣ R is an adjunction, then D is filtered as well.

Русский

Если C — фильтрованная категория и L ⊣ R образуют сопряжение, тогда и D фильтрована.

LaTeX

$$$\\text{IsFiltered } C,\\; L: D \\to C,\\; R: C \\to D,\\; L \\dashv R \\Rightarrow \\text{IsFiltered } D.$$$

Lean4

/-- If `C` is filtered, and we have a functor `R : C ⥤ D` with a left adjoint, then `D` is filtered.
-/
theorem of_right_adjoint {L : D ⥤ C} {R : C ⥤ D} (h : L ⊣ R) : IsFiltered D :=
  { IsFilteredOrEmpty.of_right_adjoint h with nonempty := IsFiltered.nonempty.map R.obj }

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