# mathlibdocumentation

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 #

• Define exponential ideals, and show this subcategory is an exponential ideal.
• Define subobject lattices in general, show that subterminals C is equivalent to the subobject category of a terminal object.
• Use both the above to show that in a locally cartesian closed category, every subobject lattice is cartesian closed (equivalently, a Heyting algebra).
def category_theory.is_subterminal {C : Type u₁} (A : C) :
Prop

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

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

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.

theorem category_theory.is_subterminal.mono_terminal_from {C : Type u₁} {A : C}  :

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.

theorem category_theory.is_subterminal_of_is_terminal {C : Type u₁} {T : C}  :
def category_theory.is_subterminal.is_iso_diag {C : Type u₁} {A : C}  :

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

Equations

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

def category_theory.is_subterminal.iso_diag {C : Type u₁} {A : C}  :
A A A

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

Equations
@[simp]
theorem category_theory.is_subterminal.iso_diag_hom {C : Type u₁} {A : C}  :
@[simp]
theorem category_theory.is_subterminal.iso_diag_inv {C : Type u₁} {A : C}  :
def category_theory.subterminals (C : Type u₁)  :
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
@[instance]
@[instance]
Equations
@[instance]
def category_theory.subterminal_inclusion (C : Type u₁)  :

The inclusion of the subterminal objects into the original category.

Equations
@[instance]