# 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.
• Use 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}  :
theorem 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.

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

noncomputable 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
Instances for category_theory.subterminals
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.subterminals.inhabited (C : Type u₁)  :
Equations
@[protected, instance]
@[simp]
theorem category_theory.subterminal_inclusion_obj (C : Type u₁) (self : category_theory.full_subcategory (λ (A : C), ) :
= self.obj
@[simp]
theorem category_theory.subterminal_inclusion_map (C : Type u₁) (f : x y) :
def category_theory.subterminal_inclusion (C : Type u₁)  :

The inclusion of the subterminal objects into the original category.

Equations
Instances for category_theory.subterminal_inclusion
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.subterminals_equiv_mono_over_terminal_unit_iso_inv_app (C : Type u₁)  :
= 𝟙 (({obj := λ (X : , , map := λ (X Y : (f : X Y), , map_id' := _, map_comp' := _} {obj := λ (X : , {obj := X.obj.left, property := _}, map := λ (X Y : (f : X Y), f.left, map_id' := _, map_comp' := _}).obj X).obj
@[simp]
theorem category_theory.subterminals_equiv_mono_over_terminal_counit_iso_hom_app (C : Type u₁) (X : category_theory.mono_over (⊤_ C)) :
= category_theory.over.hom_mk (𝟙 (({obj := λ (X : , {obj := X.obj.left, property := _}, map := λ (X Y : (f : X Y), f.left, map_id' := _, map_comp' := _} {obj := λ (X : , , map := λ (X Y : (f : X Y), , map_id' := _, map_comp' := _}).obj X).obj.left) _
noncomputable def category_theory.subterminals_equiv_mono_over_terminal (C : Type u₁)  :

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
@[simp]
@[simp]