of_final_functor_from_sifted — Mathlib

English

A functor with a final functor from a sifted category is sifted.

Русский

Функтор с финальным функтором из ситообразной категории является ситообразным.

LaTeX

$$IsSifted D$$

Lean4

/-- A functor admitting a final functor from a sifted category is sifted. -/
theorem of_final_functor_from_sifted {D : Type u₁} [Category.{v₁} D] [h₁ : IsSifted C] (F : C ⥤ D) [Final F] :
    IsSifted D := by
  rw [isSifted_iff_asSmallIsSifted] at h₁ ⊢
  exact
    of_final_functor_from_sifted' <| AsSmall.equiv.{_, _, max u₁ v₁}.inverse ⋙ F ⋙ AsSmall.equiv.{_, _, max u v}.functor

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