final_proj_of_isFiltered — Mathlib

English

The functor StructuredArrow.proj : StructuredArrow Y T ⥤ C is final if T is final and C is filtered.

Русский

Функтор StructuredArrow.proj : StructuredArrow Y T ⥤ C финален, если T финален и C фильтрована.

LaTeX

$$$[C\text{ IsFilteredOrEmpty}] (T: C \to D) [T.Final] (Y: D) \Rightarrow \mathrm{Final}(\mathrm{StructuredArrow.proj}\, Y\, T)$$$

Lean4

/-- The functor `StructuredArrow.proj : StructuredArrow Y T ⥤ C` is final if `T : C ⥤ D` is final
and `C` is filtered. -/
instance final_proj_of_isFiltered [IsFilteredOrEmpty C] (T : C ⥤ D) [Final T] (Y : D) :
    Final (StructuredArrow.proj Y T) := by
  refine ⟨fun X => ?_⟩
  rw [isConnected_iff_of_equivalence (ofStructuredArrowProjEquivalence T Y X)]
  exact (final_comp (Under.forget X) T).out _

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