English
Final functors preserve filteredness: if F is Final and C is IsFilteredOrEmpty, then D is IsFilteredOrEmpty.
Русский
Финальные функторы сохраняют фильтрованность: если F финальная и C — IsFilteredOrEmpty, то D — IsFilteredOrEmpty.
LaTeX
$$$\operatorname{Final}(F) \land \operatorname{IsFilteredOrEmpty}(C) \Rightarrow \operatorname{IsFilteredOrEmpty}(D)$$$
Lean4
/-- Initial functors preserve cofilteredness.
This can be seen as a generalization of `IsCofiltered.of_left_adjoint` (which states that left
adjoints preserve cofilteredness), as right adjoints are always initial,
see `initial_of_adjunction`.
-/
theorem of_initial (F : C ⥤ D) [Initial F] [IsCofilteredOrEmpty C] : IsCofilteredOrEmpty D :=
have : IsFilteredOrEmpty Dᵒᵖ := IsFilteredOrEmpty.of_final F.op
isCofilteredOrEmpty_of_isFilteredOrEmpty_op _
