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

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

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

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

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

theorem CategoryTheory.IsSubterminal.isIso_diag {C : Type u₁} [Category.{v₁, u₁} C] {A : C} (hA : IsSubterminal A) [Limits.HasBinaryProduct A A] : IsIso (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₁} [Category.{v₁, u₁} C] {A : C} [Limits.HasBinaryProduct A A] [IsIso (Limits.diag A)] : 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₁} [Category.{v₁, u₁} C] {A : C} (hA : IsSubterminal A) [Limits.HasBinaryProduct A A] : A ⨯ A ≅ A

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

@[simp]

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

@[simp]

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

def CategoryTheory.Subterminals (C : Type u₁) [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".

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

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

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

The inclusion of the subterminal objects into the original category.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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