mathlib documentation

category_theory.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 #

def category_theory.is_subterminal {C : Type u₁} [category_theory.category C] (A : C) :
Prop

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

Equations
theorem category_theory.is_subterminal.def {C : Type u₁} [category_theory.category C] {A : C} :
category_theory.is_subterminal A ∀ ⦃Z : C⦄ (f g : Z A), f = g

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

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

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

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

If A is subterminal, its diagonal morphism is an isomorphism. The converse of is_subterminal_of_is_iso_diag.

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

def category_theory.subterminals (C : Type u₁) [category_theory.category C] :
Type u₁

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

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