instIsCofilteredCostructuredArrowProdDiagOfIsCofilteredOrEmpty

English

If C is cofiltered-or-empty, then the costructured arrow category of the diagonal functor diag(C) is cofiltered.

Русский

Если C кофильтрована-или-пустая, то CostructuredArrow(diag(C)) кофильтрована.

LaTeX

$$IsCofiltered (CostructuredArrow (diag C) X)$$

Lean4

/-- If `C` is cofiltered, then the costructured arrow category on the diagonal functor `C ⥤ C × C`
is cofiltered as well. -/
instance [IsCofilteredOrEmpty C] (X : C × C) : IsCofiltered (CostructuredArrow (diag C) X) :=
  by
  haveI : ∀ Y, IsCofiltered (CostructuredArrow (Over.forget X.1) Y) :=
    by
    rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
    infer_instance
  apply IsCofiltered.of_equivalence (CostructuredArrow.ofDiagEquivalence X).symm

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