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₁} [CategoryTheory.Category.{v₁, u₁} C] (A : C) : Prop

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

Equations

• CategoryTheory.IsSubterminal A = ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g

theorem CategoryTheory.IsSubterminal.def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} : CategoryTheory.IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g

theorem CategoryTheory.IsSubterminal.mono_isTerminal_from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hT.from A)

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₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} [CategoryTheory.Limits.HasTerminal C] (hA : CategoryTheory.IsSubterminal A) : CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)

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₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {T : C} (hT : CategoryTheory.Limits.IsTerminal T) [CategoryTheory.Mono (hT.from A)] : CategoryTheory.IsSubterminal A

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

theorem CategoryTheory.isSubterminal_of_mono_terminal_from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)] : CategoryTheory.IsSubterminal A

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₁} [CategoryTheory.Category.{v₁, u₁} C] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsSubterminal T

theorem CategoryTheory.isSubterminal_of_terminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsSubterminal (⊤_ C)

theorem CategoryTheory.IsSubterminal.isIso_diag {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) [CategoryTheory.Limits.HasBinaryProduct A A] : CategoryTheory.IsIso (CategoryTheory.Limits.diag A)

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

theorem CategoryTheory.isSubterminal_of_isIso_diag {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryTheory.IsIso (CategoryTheory.Limits.diag A)] : CategoryTheory.IsSubterminal A

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

def CategoryTheory.IsSubterminal.isoDiag {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) [CategoryTheory.Limits.HasBinaryProduct A A] : A ⨯ A ≅ A

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

Equations

• hA.isoDiag = (CategoryTheory.asIso (CategoryTheory.Limits.diag A)).symm

@[simp]

theorem CategoryTheory.IsSubterminal.isoDiag_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) [CategoryTheory.Limits.HasBinaryProduct A A] : hA.isoDiag.inv = CategoryTheory.Limits.diag A

@[simp]

theorem CategoryTheory.IsSubterminal.isoDiag_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) [CategoryTheory.Limits.HasBinaryProduct A A] : hA.isoDiag.hom = CategoryTheory.inv (CategoryTheory.Limits.diag A)

def CategoryTheory.Subterminals (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} 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

• CategoryTheory.Subterminals C = CategoryTheory.FullSubcategory fun (A : C) => CategoryTheory.IsSubterminal A

instance CategoryTheory.instCategorySubterminals (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Category.{v₁, u₁} (CategoryTheory.Subterminals C)

Equations

• CategoryTheory.instCategorySubterminals C = CategoryTheory.FullSubcategory.category fun (A : C) => CategoryTheory.IsSubterminal A

instance CategoryTheory.instInhabitedSubterminalsOfHasTerminal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : Inhabited (CategoryTheory.Subterminals C)

Equations

• CategoryTheory.instInhabitedSubterminalsOfHasTerminal C = { default := { obj := ⊤_ C, property := ⋯ } }

def CategoryTheory.subterminalInclusion (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor (CategoryTheory.Subterminals C) C

The inclusion of the subterminal objects into the original category.

Equations

• CategoryTheory.subterminalInclusion C = CategoryTheory.fullSubcategoryInclusion fun (A : C) => CategoryTheory.IsSubterminal A

@[simp]

theorem CategoryTheory.subterminalInclusion_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.FullSubcategory fun (A : C) => CategoryTheory.IsSubterminal A) : (CategoryTheory.subterminalInclusion C).obj self = self.obj

@[simp]

theorem CategoryTheory.subterminalInclusion_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.subterminalInclusion C).map f = f

instance CategoryTheory.instFullSubterminalsSubterminalInclusion (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.subterminalInclusion C).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulSubterminalsSubterminalInclusion (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.subterminalInclusion C).Faithful

Equations

• ⋯ = ⋯

instance CategoryTheory.subterminals_thin (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Subterminals C) (Y : CategoryTheory.Subterminals C) : Subsingleton (X ⟶ Y)

Equations

• ⋯ = ⋯

def CategoryTheory.subterminalsEquivMonoOverTerminal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Subterminals C ≌ CategoryTheory.MonoOver (⊤_ 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).counitIso = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.MonoOver (⊤_ C)) => CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (({ obj := fun (X : CategoryTheory.MonoOver (⊤_ C)) => { obj := X.obj.left, property := ⋯ }, map := fun {X Y : CategoryTheory.MonoOver (⊤_ C)} (f : X ⟶ Y) => f.left, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (X : CategoryTheory.Subterminals C) => { obj := CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj), property := ⋯ }, map := fun {X Y : CategoryTheory.Subterminals C} (f : X ⟶ Y) => CategoryTheory.MonoOver.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }).obj X).obj.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (X : CategoryTheory.MonoOver (⊤_ C)) : ((CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.obj X).obj = X.obj.left

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_inverse_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : ∀ {X Y : CategoryTheory.MonoOver (⊤_ C)} (f : X ⟶ Y), (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.map f = f.left

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (X : CategoryTheory.Subterminals C) : ((CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.obj X).obj = CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj)

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : ∀ {X Y : CategoryTheory.Subterminals C} (f : X ⟶ Y), (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.map f = CategoryTheory.MonoOver.homMk f ⋯

@[simp]

theorem CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).unitIso = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Subterminals C) => CategoryTheory.Iso.refl X) ⋯

@[simp]

theorem CategoryTheory.subterminals_to_monoOver_terminal_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.comp ((CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))) = CategoryTheory.subterminalInclusion C

@[simp]

theorem CategoryTheory.monoOver_terminal_to_subterminals_comp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : (CategoryTheory.subterminalsEquivMonoOverTerminal C).inverse.comp (CategoryTheory.subterminalInclusion C) = (CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))