Documentation

Mathlib.CategoryTheory.Subterminal

Subterminal objects #

Subterminal objects are the objects which can be thought of as subobjects of the terminal object. In fact, the definition can be constructed to not require a terminal object, by defining A to be subterminal iff for any Z, there is at most one morphism Z ⟶ A. An alternate definition is that the diagonal morphism A ⟶ A ⨯ A is an isomorphism. In this file we define subterminal objects and show the equivalence of these three definitions.

We also construct the subcategory of subterminal objects.

TODO #

An object A is subterminal iff for any Z, there is at most one morphism Z ⟶ A.

Equations
Instances For

    If A is subterminal, the unique morphism from it to a terminal object is a monomorphism. The converse of isSubterminal_of_mono_isTerminal_from.

    If A is subterminal, the unique morphism from it to the terminal object is a monomorphism. The converse of isSubterminal_of_mono_terminal_from.

    If the unique morphism from A to a terminal object is a monomorphism, A is subterminal. The converse of IsSubterminal.mono_isTerminal_from.

    If the diagonal morphism of A is an isomorphism, then it is subterminal. The converse of isSubterminal.isIso_diag.

    If A is subterminal, it is isomorphic to A ⨯ A.

    Equations
    Instances For

      The (full sub)category of subterminal objects. TODO: If C is the category of sheaves on a topological space X, this category is equivalent to the lattice of open subsets of X. More generally, if C is a topos, this is the lattice of "external truth values".

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.subterminalInclusion_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
        ∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X Y), (CategoryTheory.subterminalInclusion C).map f = f
        @[simp]
        theorem CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] :
        (CategoryTheory.subterminalsEquivMonoOverTerminal C).counitIso = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.MonoOver (⊤_ C)) => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (({ obj := fun (X : CategoryTheory.MonoOver (⊤_ C)) => { obj := X.obj.left, property := }, map := fun {X Y : CategoryTheory.MonoOver (⊤_ C)} (f : X Y) => f.left, map_id := , map_comp := }.comp { obj := fun (X : CategoryTheory.Subterminals C) => { obj := CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj), property := }, map := fun {X Y : CategoryTheory.Subterminals C} (f : X Y) => CategoryTheory.MonoOver.homMk f , map_id := , map_comp := }).obj X).obj.left) )

        The category of subterminal objects is equivalent to the category of monomorphisms to the terminal object (which is in turn equivalent to the subobjects of the terminal object).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For