mathlib documentation

category_theory.limits.preserves.shapes.terminal

Preserving terminal object #

Constructions to relate the notions of preserving terminal objects and reflecting terminal objects to concrete objects.

In particular, we show that terminal_comparison G is an isomorphism iff G preserves terminal objects.

def category_theory.limits.is_limit_map_cone_empty_cone_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X : C) :

category_theory.limits.is_limit (G.map_cone (category_theory.limits.as_empty_cone X)) ≃ category_theory.limits.is_terminal (G.obj X)

The map of an empty cone is a limit iff the mapped object is terminal.

Equations

def category_theory.limits.is_terminal_obj_of_is_terminal {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X : C) [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] (l : category_theory.limits.is_terminal X) :

category_theory.limits.is_terminal (G.obj X)

The property of preserving terminal objects expressed in terms of is_terminal.

Equations

category_theory.limits.is_terminal_obj_of_is_terminal G X l = ⇑(category_theory.limits.is_limit_map_cone_empty_cone_equiv G X) (category_theory.limits.preserves_limit.preserves l)

def category_theory.limits.is_terminal_of_is_terminal_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (X : C) [category_theory.limits.reflects_limit (category_theory.functor.empty C) G] (l : category_theory.limits.is_terminal (G.obj X)) :

category_theory.limits.is_terminal X

The property of reflecting terminal objects expressed in terms of is_terminal.

Equations

category_theory.limits.is_terminal_of_is_terminal_obj G X l = category_theory.limits.reflects_limit.reflects (⇑((category_theory.limits.is_limit_map_cone_empty_cone_equiv G X).symm) l)

def category_theory.limits.is_limit_of_has_terminal_of_preserves_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] :

category_theory.limits.is_terminal (G.obj (⊤_C))

If G preserves the terminal object and C has a terminal object, then the image of the terminal object is terminal.

Equations

category_theory.limits.is_limit_of_has_terminal_of_preserves_limit G = category_theory.limits.is_terminal_obj_of_is_terminal G (⊤_C) category_theory.limits.terminal_is_terminal

theorem category_theory.limits.has_terminal_of_has_terminal_of_preserves_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] :

category_theory.limits.has_terminal D

If C has a terminal object and G preserves terminal objects, then D has a terminal object also. Note this property is somewhat unique to (co)limits of the empty diagram: for general J, if C has limits of shape J and G preserves them, then D does not necessarily have limits of shape J.

def category_theory.limits.preserves_terminal.of_iso_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] [i : category_theory.is_iso (category_theory.limits.terminal_comparison G)] :

category_theory.limits.preserves_limit (category_theory.functor.empty C) G

If the terminal comparison map for G is an isomorphism, then G preserves terminal objects.

Equations

category_theory.limits.preserves_terminal.of_iso_comparison G = category_theory.limits.preserves_limit_of_preserves_limit_cone category_theory.limits.terminal_is_terminal (⇑((category_theory.limits.is_limit_map_cone_empty_cone_equiv G (⊤_C)).symm) (category_theory.limits.limit.is_limit (category_theory.functor.empty D)).of_point_iso)

def category_theory.limits.preserves_terminal_of_is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] (f : G.obj (⊤_C) ⟶ ⊤_D) [i : category_theory.is_iso f] :

category_theory.limits.preserves_limit (category_theory.functor.empty C) G

If there is any isomorphism G.obj ⊤ ⟶ ⊤, then G preserves terminal objects.

Equations

category_theory.limits.preserves_terminal_of_is_iso G f = category_theory.limits.preserves_terminal.of_iso_comparison G

def category_theory.limits.preserves_terminal_of_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] (f : G.obj (⊤_C) ≅ ⊤_D) :

category_theory.limits.preserves_limit (category_theory.functor.empty C) G

If there is any isomorphism G.obj ⊤ ≅ ⊤, then G preserves terminal objects.

Equations

category_theory.limits.preserves_terminal_of_iso G f = category_theory.limits.preserves_terminal_of_is_iso G f.hom

def category_theory.limits.preserves_terminal.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] :

G.obj (⊤_C) ≅ ⊤_D

If G preserves terminal objects, then the terminal comparison map for G an isomorphism.

Equations

category_theory.limits.preserves_terminal.iso G = category_theory.limits.is_limit.cone_point_unique_up_to_iso (category_theory.limits.is_limit_of_has_terminal_of_preserves_limit G) (category_theory.limits.limit.is_limit (category_theory.functor.empty D))

@[simp]

theorem category_theory.limits.preserves_terminal.iso_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] :

(category_theory.limits.preserves_terminal.iso G).hom = category_theory.limits.terminal_comparison G

@[instance]

def category_theory.limits.terminal_comparison.category_theory.is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) [category_theory.limits.has_terminal C] [category_theory.limits.has_terminal D] [category_theory.limits.preserves_limit (category_theory.functor.empty C) G] :

category_theory.is_iso (category_theory.limits.terminal_comparison G)

Equations

category_theory.limits.terminal_comparison.category_theory.is_iso G = _.mpr (category_theory.is_iso.of_iso (category_theory.limits.preserves_terminal.iso G))