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.

Equations
• = ∀ ⦃Z : C⦄ (f g : Z A), f = g
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 : ) [CategoryTheory.Mono (hT.from A)] :

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_hom {C : Type u₁} [] {A : C} (hA : ) :
hA.isoDiag.hom =
@[simp]
theorem CategoryTheory.IsSubterminal.isoDiag_inv {C : Type u₁} [] {A : C} (hA : ) :
hA.isoDiag.inv =
def CategoryTheory.IsSubterminal.isoDiag {C : Type u₁} [] {A : C} (hA : ) :
A A A

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

Equations
• hA.isoDiag = .symm
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".

Equations
Instances For
Equations
Equations
• = { default := { obj := ⊤_ C, property := } }
@[simp]
theorem CategoryTheory.subterminalInclusion_map (C : Type u₁) [] :
∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X Y), f = f
@[simp]
theorem CategoryTheory.subterminalInclusion_obj (C : Type u₁) [] (self : CategoryTheory.FullSubcategory fun (A : C) => ) :
self = self.obj

The inclusion of the subterminal objects into the original category.

Equations
Instances For
Equations
• =
Equations
• =
instance CategoryTheory.subterminals_thin (C : Type u₁) [] (X : ) (Y : ) :
Equations
• =
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map (C : Type u₁) [] :
∀ {X Y : } (f : X Y), .functor.map f =
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso (C : Type u₁) [] :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : ) => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (({ obj := fun (X : ) => { obj := X.obj.left, property := }, map := fun {X Y : } (f : X Y) => f.left, map_id := , map_comp := }.comp { obj := fun (X : ) => { obj := , property := }, map := fun {X Y : } (f : X Y) => , map_id := , map_comp := }).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_inverse_obj_obj (C : Type u₁) [] (X : ) :
(.inverse.obj X).obj = X.obj.left
@[simp]
theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj (C : Type u₁) [] (X : ) :
(.functor.obj X).obj =

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.subterminals_to_monoOver_terminal_comp_forget (C : Type u₁) [] :
.functor.comp (.comp ()) =
@[simp]
theorem CategoryTheory.monoOver_terminal_to_subterminals_comp (C : Type u₁) [] :
.inverse.comp = .comp ()