of_isRightAdjoint — Mathlib

English

If C is filtered and R: C ⥤ D has a right adjoint, then D is filtered.

Русский

Если C фильтрована и у R: C ⥤ D есть правый сопряженный, то D также фильтрована.

LaTeX

$$$\\text{IsFiltered } C \\Rightarrow \\text{IsFiltered } D$ under the assumption that $R$ has a right adjoint.$$

Lean4

/-- If `C` is filtered, and we have a right adjoint functor `R : C ⥤ D`, then `D` is filtered. -/
theorem of_isRightAdjoint (R : C ⥤ D) [R.IsRightAdjoint] : IsFiltered D :=
  of_right_adjoint (Adjunction.ofIsRightAdjoint R)

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