mathlib3 documentation

category_theory.subterminal

Subterminal objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

Equations

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

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