mathlib3 documentation

category_theory.subterminal

Subterminal objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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₁} [category_theory.category C] (A : C) :

Prop

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

theorem category_theory.is_subterminal.def {C : Type u₁} [category_theory.category C] {A : C} :

category_theory.is_subterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g

theorem category_theory.is_subterminal.mono_is_terminal_from {C : Type u₁} [category_theory.category C] {A : C} (hA : category_theory.is_subterminal A) {T : C} (hT : category_theory.limits.is_terminal T) :

category_theory.mono (hT.from A)

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₁} [category_theory.category C] {A : C} [category_theory.limits.has_terminal C] (hA : category_theory.is_subterminal A) :

category_theory.mono (category_theory.limits.terminal.from A)

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.

theorem category_theory.is_subterminal_of_mono_is_terminal_from {C : Type u₁} [category_theory.category C] {A T : C} (hT : category_theory.limits.is_terminal T) [category_theory.mono (hT.from A)] :

category_theory.is_subterminal A

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.

theorem category_theory.is_subterminal_of_mono_terminal_from {C : Type u₁} [category_theory.category C] {A : C} [category_theory.limits.has_terminal C] [category_theory.mono (category_theory.limits.terminal.from A)] :

category_theory.is_subterminal A

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₁} [category_theory.category C] {T : C} (hT : category_theory.limits.is_terminal T) :

category_theory.is_subterminal T

theorem category_theory.is_subterminal_of_terminal {C : Type u₁} [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.is_subterminal (⊤_ C)

theorem category_theory.is_subterminal.is_iso_diag {C : Type u₁} [category_theory.category C] {A : C} (hA : category_theory.is_subterminal A) [category_theory.limits.has_binary_product A A] :

category_theory.is_iso (category_theory.limits.diag A)

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

theorem category_theory.is_subterminal_of_is_iso_diag {C : Type u₁} [category_theory.category C] {A : C} [category_theory.limits.has_binary_product A A] [category_theory.is_iso (category_theory.limits.diag A)] :

category_theory.is_subterminal A

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₁} [category_theory.category C] {A : C} (hA : category_theory.is_subterminal A) [category_theory.limits.has_binary_product A A] :

A ⨯ A ≅ A

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

@[simp]

theorem category_theory.is_subterminal.iso_diag_hom {C : Type u₁} [category_theory.category C] {A : C} (hA : category_theory.is_subterminal A) [category_theory.limits.has_binary_product A A] :

hA.iso_diag.hom = category_theory.inv (category_theory.limits.diag A)

@[simp]

theorem category_theory.is_subterminal.iso_diag_inv {C : Type u₁} [category_theory.category C] {A : C} (hA : category_theory.is_subterminal A) [category_theory.limits.has_binary_product A A] :

hA.iso_diag.inv = category_theory.limits.diag A

def category_theory.subterminals (C : Type u₁) [category_theory.category C] :

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

category_theory.subterminals C = category_theory.full_subcategory (λ (A : C), category_theory.is_subterminal A)

Instances for category_theory.subterminals

@[protected, instance]

def category_theory.subterminals.category (C : Type u₁) [category_theory.category C] :

category_theory.category (category_theory.subterminals C)

@[protected, instance]

noncomputable def category_theory.subterminals.inhabited (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] :

inhabited (category_theory.subterminals C)

Equations

category_theory.subterminals.inhabited C = {default := {obj := ⊤_ C, property := _}}

@[protected, instance]

def category_theory.subterminal_inclusion.faithful (C : Type u₁) [category_theory.category C] :

category_theory.faithful (category_theory.subterminal_inclusion C)

@[simp]

theorem category_theory.subterminal_inclusion_obj (C : Type u₁) [category_theory.category C] (self : category_theory.full_subcategory (λ (A : C), category_theory.is_subterminal A)) :

(category_theory.subterminal_inclusion C).obj self = self.obj

@[simp]

theorem category_theory.subterminal_inclusion_map (C : Type u₁) [category_theory.category C] (x y : category_theory.induced_category C category_theory.full_subcategory.obj) (f : x ⟶ y) :

(category_theory.subterminal_inclusion C).map f = f

def category_theory.subterminal_inclusion (C : Type u₁) [category_theory.category C] :

category_theory.subterminals C ⥤ C

The inclusion of the subterminal objects into the original category.

Equations

category_theory.subterminal_inclusion C = category_theory.full_subcategory_inclusion (λ (A : C), category_theory.is_subterminal A)

Instances for category_theory.subterminal_inclusion

@[protected, instance]

def category_theory.subterminal_inclusion.full (C : Type u₁) [category_theory.category C] :

category_theory.full (category_theory.subterminal_inclusion C)

@[protected, instance]

def category_theory.subterminals_thin (C : Type u₁) [category_theory.category C] (X Y : category_theory.subterminals C) :

subsingleton (X ⟶ Y)

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_inverse_map (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X Y : category_theory.mono_over (⊤_ C)) (f : X ⟶ Y) :

(category_theory.subterminals_equiv_mono_over_terminal C).inverse.map f = f.left

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_functor_obj_obj (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.subterminals C) :

((category_theory.subterminals_equiv_mono_over_terminal C).functor.obj X).obj = category_theory.over.mk (category_theory.limits.terminal.from X.obj)

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_inverse_obj_obj (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.mono_over (⊤_ C)) :

((category_theory.subterminals_equiv_mono_over_terminal C).inverse.obj X).obj = X.obj.left

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_functor_map (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X Y : category_theory.subterminals C) (f : X ⟶ Y) :

(category_theory.subterminals_equiv_mono_over_terminal C).functor.map f = category_theory.mono_over.hom_mk f _

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_unit_iso_hom_app (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.subterminals C) :

(category_theory.subterminals_equiv_mono_over_terminal C).unit_iso.hom.app X = 𝟙 ((𝟭 (category_theory.subterminals C)).obj X).obj

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_unit_iso_inv_app (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.subterminals C) :

(category_theory.subterminals_equiv_mono_over_terminal C).unit_iso.inv.app X = 𝟙 (({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

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_counit_iso_hom_app (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.mono_over (⊤_ C)) :

(category_theory.subterminals_equiv_mono_over_terminal C).counit_iso.hom.app X = 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) _

noncomputable def category_theory.subterminals_equiv_mono_over_terminal (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] :

category_theory.subterminals C ≌ category_theory.mono_over (⊤_ C)

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' := _}

@[simp]

theorem category_theory.subterminals_equiv_mono_over_terminal_counit_iso_inv_app (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] (X : category_theory.mono_over (⊤_ C)) :

(category_theory.subterminals_equiv_mono_over_terminal C).counit_iso.inv.app X = category_theory.over.hom_mk (𝟙 ((𝟭 (category_theory.mono_over (⊤_ C))).obj X).obj.left) _

@[simp]

theorem category_theory.subterminals_to_mono_over_terminal_comp_forget (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] :

(category_theory.subterminals_equiv_mono_over_terminal C).functor ⋙ category_theory.mono_over.forget (⊤_ C) ⋙ category_theory.over.forget (⊤_ C) = category_theory.subterminal_inclusion C

@[simp]

theorem category_theory.mono_over_terminal_to_subterminals_comp (C : Type u₁) [category_theory.category C] [category_theory.limits.has_terminal C] :

(category_theory.subterminals_equiv_mono_over_terminal C).inverse ⋙ category_theory.subterminal_inclusion C = category_theory.mono_over.forget (⊤_ C) ⋙ category_theory.over.forget (⊤_ C)