instIsCofilteredOfIsCofilteredOrEmpty

English

If C is CofilteredOrEmpty, then the terminal-augmented category WithTerminal(C) is Cofiltered.

Русский

Если C обладает свойством CofilteredOrEmpty, то WithTerminal(C) является Cofiltered.

LaTeX

$$$[\mathrm{IsCofilteredOrEmpty}(C)] \implies \mathrm{IsCofiltered}(\mathrm{WithTerminal}(C))$$$

Lean4

instance [IsCofilteredOrEmpty C] : IsCofiltered (WithTerminal C)
    where
  cone_objs x
    y :=
    match x, y with
    | star, y => ⟨y, default, 𝟙 y, trivial⟩
    | x, star => ⟨x, 𝟙 x, default, trivial⟩
    | of x, of y => ⟨.of <| min x y, minToLeft _ _, minToRight _ _, trivial⟩
  cone_maps x y f
    g :=
    match x, y with
    | star, _ => ⟨star, 𝟙 _, (IsIso.eq_comp_inv f).mp rfl⟩
    | x, star => ⟨x, 𝟙 _, Subsingleton.elim _ _⟩
    | of _, of _ => ⟨.of <| eq f g, eqHom _ _, eq_condition _ _⟩

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