of_initial — Mathlib

English

If T is final, then StructuredArrow.pre X T S is final.

Русский

Если T финальная, то StructuredArrow.pre X T S финальная.

LaTeX

$$$\operatorname{Final}(T) \Rightarrow \operatorname{Final}(\operatorname{StructuredArrow.pre}(X,T,S))$$$

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] [IsCofiltered C] : IsCofiltered D :=
  have : IsFiltered Dᵒᵖ := IsFiltered.of_final F.op
  isCofiltered_of_isFiltered_op _

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