final_of_exists_of_isFiltered — Mathlib

English

If for every d the StructuredArrow d F is filtered, then F is final.

Русский

Если для каждого d стрелка структурированного стрелка d F фильтрована, то F финальна.

LaTeX

$$$\\forall d, \\mathrm{IsFiltered}(\\mathrm{StructuredArrow}\\, d\\, F) \\Rightarrow \\mathrm{Final}(F)$$$

Lean4

/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final. The converse is also true, see `final_iff_of_isFiltered`. -/
theorem final_of_exists_of_isFiltered [IsFilteredOrEmpty C] (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c))
    (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) :
    Functor.Final F :=
  by
  suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F
  exact isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂

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