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).
An object A
is subterminal iff for any Z
, there is at most one morphism Z ⟶ A
.
Equations
- 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
- hA.iso_diag = let _inst : category_theory.is_iso (category_theory.limits.diag A) := _ in (category_theory.as_iso (category_theory.limits.diag A)).symm
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 inclusion of the subterminal objects into the original category.
Equations
Instances for category_theory.subterminal_inclusion
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
- category_theory.subterminals_equiv_mono_over_terminal C = {functor := {obj := λ (X : category_theory.subterminals C), {obj := category_theory.over.mk (category_theory.limits.terminal.from X.obj), property := _}, map := λ (X Y : category_theory.subterminals C) (f : X ⟶ Y), category_theory.mono_over.hom_mk f _, map_id' := _, map_comp' := _}, inverse := {obj := λ (X : category_theory.mono_over (⊤_ C)), {obj := X.obj.left, property := _}, map := λ (X Y : category_theory.mono_over (⊤_ C)) (f : X ⟶ Y), f.left, map_id' := _, map_comp' := _}, unit_iso := {hom := {app := λ (X : category_theory.subterminals C), 𝟙 ((𝟭 (category_theory.subterminals C)).obj X).obj, naturality' := _}, inv := {app := λ (X : category_theory.subterminals C), 𝟙 (({obj := λ (X : category_theory.subterminals C), {obj := category_theory.over.mk (category_theory.limits.terminal.from X.obj), property := _}, map := λ (X Y : category_theory.subterminals C) (f : X ⟶ Y), category_theory.mono_over.hom_mk f _, map_id' := _, map_comp' := _} ⋙ {obj := λ (X : category_theory.mono_over (⊤_ C)), {obj := X.obj.left, property := _}, map := λ (X Y : category_theory.mono_over (⊤_ C)) (f : X ⟶ Y), f.left, map_id' := _, map_comp' := _}).obj X).obj, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}, counit_iso := {hom := {app := λ (X : category_theory.mono_over (⊤_ C)), category_theory.over.hom_mk (𝟙 (({obj := λ (X : category_theory.mono_over (⊤_ C)), {obj := X.obj.left, property := _}, map := λ (X Y : category_theory.mono_over (⊤_ C)) (f : X ⟶ Y), f.left, map_id' := _, map_comp' := _} ⋙ {obj := λ (X : category_theory.subterminals C), {obj := category_theory.over.mk (category_theory.limits.terminal.from X.obj), property := _}, map := λ (X Y : category_theory.subterminals C) (f : X ⟶ Y), category_theory.mono_over.hom_mk f _, map_id' := _, map_comp' := _}).obj X).obj.left) _, naturality' := _}, inv := {app := λ (X : category_theory.mono_over (⊤_ C)), category_theory.over.hom_mk (𝟙 ((𝟭 (category_theory.mono_over (⊤_ C))).obj X).obj.left) _, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}, functor_unit_iso_comp' := _}