Preserving terminal object

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

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

def CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.asEmptyCone X)) ≃ CategoryTheory.Limits.IsTerminal (G.obj X)

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

Equations

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

def CategoryTheory.Limits.IsTerminal.isTerminalObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal (G.obj X)

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

Equations

• CategoryTheory.Limits.IsTerminal.isTerminalObj G X l = (CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv G X) (CategoryTheory.Limits.isLimitOfPreserves G l)

def CategoryTheory.Limits.IsTerminal.isTerminalOfObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsTerminal (G.obj X)) : CategoryTheory.Limits.IsTerminal X

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

Equations

• CategoryTheory.Limits.IsTerminal.isTerminalOfObj G X l = CategoryTheory.Limits.isLimitOfReflects G ((CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv G X).symm l)

def CategoryTheory.Limits.IsTerminal.isTerminalIffObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] (X : C) : CategoryTheory.Limits.IsTerminal X ≃ CategoryTheory.Limits.IsTerminal (G.obj X)

A functor that preserves and reflects terminal objects induces an equivalence on IsTerminal.

Equations

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G

Preserving the terminal object implies preserving all limits of the empty diagram.

def CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.IsTerminal (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

• CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit G = CategoryTheory.Limits.IsTerminal.isTerminalObj G (⊤_ C) CategoryTheory.Limits.terminalIsTerminal

theorem CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.HasTerminal 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.

theorem CategoryTheory.Limits.PreservesTerminal.of_iso_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [i : CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G

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

theorem CategoryTheory.Limits.preservesTerminal_of_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : CategoryTheory.IsIso f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G

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

theorem CategoryTheory.Limits.preservesTerminal_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ≅ ⊤_ D) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G

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

def CategoryTheory.Limits.PreservesTerminal.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : G.obj (⊤_ C) ≅ ⊤_ D

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesTerminal.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : (CategoryTheory.Limits.PreservesTerminal.iso G).hom = CategoryTheory.Limits.terminalComparison G

instance CategoryTheory.Limits.instIsIsoTerminalComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.IsIso (CategoryTheory.Limits.terminalComparison G)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.asEmptyCocone X)) ≃ CategoryTheory.Limits.IsInitial (G.obj X)

The map of an empty cocone is a colimit iff the mapped object is initial.

Equations

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

def CategoryTheory.Limits.IsInitial.isInitialObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsInitial (G.obj X)

The property of preserving initial objects expressed in terms of IsInitial.

Equations

• CategoryTheory.Limits.IsInitial.isInitialObj G X l = (CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv G X) (CategoryTheory.Limits.isColimitOfPreserves G l)

def CategoryTheory.Limits.IsInitial.isInitialOfObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsInitial (G.obj X)) : CategoryTheory.Limits.IsInitial X

The property of reflecting initial objects expressed in terms of IsInitial.

Equations

• CategoryTheory.Limits.IsInitial.isInitialOfObj G X l = CategoryTheory.Limits.isColimitOfReflects G ((CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv G X).symm l)

def CategoryTheory.Limits.IsInitial.isInitialIffObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] (X : C) : CategoryTheory.Limits.IsInitial X ≃ CategoryTheory.Limits.IsInitial (G.obj X)

A functor that preserves and reflects initial objects induces an equivalence on IsInitial.

Equations

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

theorem CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G

Preserving the initial object implies preserving all colimits of the empty diagram.

def CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.IsInitial (G.obj (⊥_ C))

If G preserves the initial object and C has an initial object, then the image of the initial object is initial.

Equations

• CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit G = CategoryTheory.Limits.IsInitial.isInitialObj G (⊥_ C) CategoryTheory.Limits.initialIsInitial

theorem CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.HasInitial D

If C has an initial object and G preserves initial objects, then D has an initial object also. Note this property is somewhat unique to colimits of the empty diagram: for general J, if C has colimits of shape J and G preserves them, then D does not necessarily have colimits of shape J.

theorem CategoryTheory.Limits.PreservesInitial.of_iso_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] [i : CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G

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

theorem CategoryTheory.Limits.preservesInitial_of_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : CategoryTheory.IsIso f] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G

If there is any isomorphism ⊥ ⟶ G.obj ⊥, then G preserves initial objects.

theorem CategoryTheory.Limits.preservesInitial_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] (f : ⊥_ D ≅ G.obj (⊥_ C)) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G

If there is any isomorphism ⊥ ≅ G.obj ⊥, then G preserves initial objects.

def CategoryTheory.Limits.PreservesInitial.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : G.obj (⊥_ C) ≅ ⊥_ D

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesInitial.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : (CategoryTheory.Limits.PreservesInitial.iso G).inv = CategoryTheory.Limits.initialComparison G

instance CategoryTheory.Limits.instIsIsoInitialComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.IsIso (CategoryTheory.Limits.initialComparison G)

Equations

• ⋯ = ⋯