isCofilteredOrEmpty_op_of_isFilteredOrEmpty

English

If C is cofiltered, then for any finite diagram F: J ⥤ C, Cone F exists.

Русский

Если C кофильтрована, то для любой конечной диаграммы F: J ⥤ C существует конус над F.

LaTeX

$$$\mathrm{IsCofiltered} C \Rightarrow \forall J\; [SmallCategory J][FinCategory J]\; (F: J \to C) \Rightarrow \mathrm{Cone}\,F\text{ nonempty}$$$

Lean4

instance isCofilteredOrEmpty_op_of_isFilteredOrEmpty [IsFilteredOrEmpty C] : IsCofilteredOrEmpty Cᵒᵖ
    where
  cone_objs X
    Y := ⟨op (IsFiltered.max X.unop Y.unop), (IsFiltered.leftToMax _ _).op, (IsFiltered.rightToMax _ _).op, trivial⟩
  cone_maps X Y f
    g :=
    ⟨op (IsFiltered.coeq f.unop g.unop), (IsFiltered.coeqHom _ _).op,
      by
      rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
      congr 1
      exact IsFiltered.coeq_condition f.unop g.unop⟩

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