instIsFilteredStructuredArrowProdDiagOfIsFilteredOrEmpty

English

If C is filtered-or-empty, then the StructuredArrow X → diag(C) is filtered for any X ∈ C × C.

Русский

Если C фильтрована-или-пустая, то структурированная стрелка X → диагональ(C) фильтрована для любого X ∈ C × C.

LaTeX

$$IsFiltered (StructuredArrow X (diag C))$$

Lean4

/-- If `C` is filtered, then the structured arrow category on the diagonal functor `C ⥤ C × C`
is filtered as well. -/
instance [IsFilteredOrEmpty C] (X : C × C) : IsFiltered (StructuredArrow X (diag C)) :=
  by
  haveI : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) :=
    by
    rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
    infer_instance
  apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm

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