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

• Define exponential ideals, and show this subcategory is an exponential ideal.
• Use the above to show that in a locally cartesian closed category, every subobject lattice is cartesian closed (equivalently, a Heyting algebra).
def CategoryTheory.IsSubterminal {C : Type u₁} [] (A : C) :

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

Instances For
theorem CategoryTheory.IsSubterminal.def {C : Type u₁} [] {A : C} :
∀ ⦃Z : C⦄ (f g : Z A), f = g
theorem CategoryTheory.IsSubterminal.mono_isTerminal_from {C : Type u₁} [] {A : C} (hA : ) {T : C} (hT : ) :

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

theorem CategoryTheory.IsSubterminal.mono_terminal_from {C : Type u₁} [] {A : C} (hA : ) :

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

theorem CategoryTheory.isSubterminal_of_mono_isTerminal_from {C : Type u₁} [] {A : C} {T : C} (hT : ) :

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 unique morphism from A to the terminal object is a monomorphism, A is subterminal. The converse of IsSubterminal.mono_terminal_from.

theorem CategoryTheory.isSubterminal_of_isTerminal {C : Type u₁} [] {T : C} (hT : ) :
theorem CategoryTheory.IsSubterminal.isIso_diag {C : Type u₁} [] {A : C} (hA : ) :

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

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

@[simp]
theorem CategoryTheory.IsSubterminal.isoDiag_inv {C : Type u₁} [] {A : C} (hA : ) :
@[simp]
theorem CategoryTheory.IsSubterminal.isoDiag_hom {C : Type u₁} [] {A : C} (hA : ) :
def CategoryTheory.IsSubterminal.isoDiag {C : Type u₁} [] {A : C} (hA : ) :
A A A

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

Instances For
def CategoryTheory.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".

Instances For
@[simp]
theorem CategoryTheory.subterminalInclusion_map (C : Type u₁) [] :
∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X Y), ().map f = f
@[simp]
theorem CategoryTheory.subterminalInclusion_obj (C : Type u₁) [] (self : ) :
().obj self = self.obj

The inclusion of the subterminal objects into the original category.

Instances For
instance CategoryTheory.subterminals_thin (C : Type u₁) [] (X : ) (Y : ) :
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj (C : Type u₁) [] (X : ) :
(().functor.obj X).obj =
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj (C : Type u₁) [] (X : ) :
(().inverse.obj X).obj = X.obj.left
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y), ().inverse.map f = f.left
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso (C : Type u₁) [] :
().counitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Functor.mk { obj := fun X => { obj := X.obj.left, property := (_ : ∀ (Z : C) (f g : Z X.obj.left), f = g) }, map := fun {X Y} f => f.left }) (CategoryTheory.Functor.mk { obj := fun X => { obj := , property := (_ : ) }, map := fun {X Y} f => })).obj X).obj.left)
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y), ().functor.map f =

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).

Instances For
@[simp]
@[simp]