isFilteredOrEmpty_op_of_isCofilteredOrEmpty

English

If C⁰ᵖ is filtered or empty, then C is cofiltered.

Русский

Если Cᵒᵖ фильтрована или пуста, то C кофильтрована.

LaTeX

$$[IsFilteredOrEmpty Cᵒᵖ] ⇒ IsCofilteredOrEmpty C$$

Lean4

instance isFilteredOrEmpty_op_of_isCofilteredOrEmpty [IsCofilteredOrEmpty C] : IsFilteredOrEmpty Cᵒᵖ
    where
  cocone_objs X
    Y :=
    ⟨op (IsCofiltered.min X.unop Y.unop), (IsCofiltered.minToLeft X.unop Y.unop).op,
      (IsCofiltered.minToRight X.unop Y.unop).op, trivial⟩
  cocone_maps X Y f
    g :=
    ⟨op (IsCofiltered.eq f.unop g.unop), (IsCofiltered.eqHom f.unop g.unop).op,
      by
      rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
      congr 1
      exact IsCofiltered.eq_condition f.unop g.unop⟩

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