Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv definition

: IsLimit (G.mapCone (asEmptyCone X)) ≃ IsTerminal (G.obj X)

Full source

/-- The map of an empty cone is a limit iff the mapped object is terminal.
-/
def isLimitMapConeEmptyConeEquiv :
    IsLimitIsLimit (G.mapCone (asEmptyCone X)) ≃ IsTerminal (G.obj X) :=
  isLimitEmptyConeEquiv D _ _ (eqToIso rfl)

Equivalence between limit condition of mapped empty cone and terminality of image object

Informal description

Given a functor $G \colon C \to D$ and an object $X$ in $C$, the equivalence states that the image of the empty cone over $X$ under $G$ is a limit cone if and only if $G(X)$ is a terminal object in $D$.

CategoryTheory.Limits.IsTerminal.isTerminalObj definition

[PreservesLimit (Functor.empty.{0} C) G] (l : IsTerminal X) : IsTerminal (G.obj X)

Full source

/-- The property of preserving terminal objects expressed in terms of `IsTerminal`. -/
def IsTerminal.isTerminalObj [PreservesLimit (Functor.empty.{0} C) G] (l : IsTerminal X) :
    IsTerminal (G.obj X) :=
  isLimitMapConeEmptyConeEquiv G X (isLimitOfPreserves G l)

Preservation of terminal objects under limit-preserving functors

Informal description

Given a functor $G \colon C \to D$ that preserves limits of the empty diagram, if $X$ is a terminal object in $C$, then $G(X)$ is a terminal object in $D$.

CategoryTheory.Limits.IsTerminal.isTerminalOfObj definition

[ReflectsLimit (Functor.empty.{0} C) G] (l : IsTerminal (G.obj X)) : IsTerminal X

Full source

/-- The property of reflecting terminal objects expressed in terms of `IsTerminal`. -/
def IsTerminal.isTerminalOfObj [ReflectsLimit (Functor.empty.{0} C) G] (l : IsTerminal (G.obj X)) :
    IsTerminal X :=
  isLimitOfReflects G ((isLimitMapConeEmptyConeEquiv G X).symm l)

Reflection of terminal objects under limit-reflecting functors

Informal description

Given a functor $G \colon C \to D$ that reflects limits of the empty diagram, if $G(X)$ is a terminal object in $D$, then $X$ is a terminal object in $C$.

CategoryTheory.Limits.IsTerminal.isTerminalIffObj definition

 [PreservesLimit (Functor.empty.{0} C) G] [ReflectsLimit (Functor.empty.{0} C) G] (X : C) :
  IsTerminal X ≃ IsTerminal (G.obj X)

Full source

/-- A functor that preserves and reflects terminal objects induces an equivalence on
`IsTerminal`. -/
def IsTerminal.isTerminalIffObj [PreservesLimit (Functor.empty.{0} C) G]
    [ReflectsLimit (Functor.empty.{0} C) G] (X : C) :
    IsTerminalIsTerminal X ≃ IsTerminal (G.obj X) where
  toFun := IsTerminal.isTerminalObj G X
  invFun := IsTerminal.isTerminalOfObj G X
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of terminality under limit-preserving and reflecting functors

Informal description

Given a functor $G \colon C \to D$ that both preserves and reflects limits of the empty diagram, there is an equivalence between the property of an object $X$ in $C$ being terminal and the property of its image $G(X)$ being terminal in $D$. Specifically, the equivalence is given by the maps `IsTerminal.isTerminalObj` and `IsTerminal.isTerminalOfObj`, which are mutual inverses.

CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal theorem

[PreservesLimit (Functor.empty.{0} C) G] : PreservesLimitsOfShape (Discrete PEmpty.{1}) G

Full source

/-- Preserving the terminal object implies preserving all limits of the empty diagram. -/
lemma preservesLimitsOfShape_pempty_of_preservesTerminal [PreservesLimit (Functor.empty.{0} C) G] :
    PreservesLimitsOfShape (Discrete PEmptyPEmpty.{1}) G where
  preservesLimit := preservesLimit_of_iso_diagram G (Functor.emptyExt (Functor.empty.{0} C) _)

Preservation of Empty Diagram Limits via Terminal Object Preservation

Informal description

If a functor $G \colon C \to D$ preserves the terminal object in category $C$, then it preserves all limits of the empty diagram (i.e., limits indexed by the discrete category on the empty type).

CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit definition

[PreservesLimit (Functor.empty.{0} C) G] : IsTerminal (G.obj (⊤_ C))

Full source

/--
If `G` preserves the terminal object and `C` has a terminal object, then the image of the terminal
object is terminal.
-/
def isLimitOfHasTerminalOfPreservesLimit [PreservesLimit (Functor.empty.{0} C) G] :
    IsTerminal (G.obj (⊤_ C)) :=
  terminalIsTerminal.isTerminalObj G (⊤_ C)

Preservation of terminal objects under limit-preserving functors

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves limits of the empty diagram (i.e., terminal objects), the image $G(\top_{\mathcal{C}})$ of the terminal object $\top_{\mathcal{C}}$ in $\mathcal{C}$ is a terminal object in $\mathcal{D}$.

CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit theorem

[PreservesLimit (Functor.empty.{0} C) G] : HasTerminal D

Full source

/-- 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 hasTerminal_of_hasTerminal_of_preservesLimit [PreservesLimit (Functor.empty.{0} C) G] :
    HasTerminal D := ⟨fun F => by
  haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
  apply hasLimit_of_iso F.uniqueFromEmpty.symm⟩

Existence of Terminal Object in Codomain via Terminal-Preserving Functor

Informal description

If a category $\mathcal{C}$ has a terminal object and a functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves terminal objects (i.e., preserves limits of the empty diagram), then the category $\mathcal{D}$ also has a terminal object.

CategoryTheory.Limits.PreservesTerminal.of_iso_comparison theorem

[i : IsIso (terminalComparison G)] : PreservesLimit (Functor.empty.{0} C) G

Full source

/-- If the terminal comparison map for `G` is an isomorphism, then `G` preserves terminal objects.
-/
lemma PreservesTerminal.of_iso_comparison [i : IsIso (terminalComparison G)] :
    PreservesLimit (Functor.empty.{0} C) G := by
  apply preservesLimit_of_preserves_limit_cone terminalIsTerminal
  apply (isLimitMapConeEmptyConeEquiv _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

Preservation of Terminal Objects via Isomorphic Comparison Morphism

Informal description

If the terminal comparison morphism $G(\top_{\mathcal{C}}) \to \top_{\mathcal{D}}$ for a functor $G \colon \mathcal{C} \to \mathcal{D}$ is an isomorphism, then $G$ preserves terminal objects.

CategoryTheory.Limits.preservesTerminal_of_isIso theorem

(f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : IsIso f] : PreservesLimit (Functor.empty.{0} C) G

Full source

/-- If there is any isomorphism `G.obj ⊤ ⟶ ⊤`, then `G` preserves terminal objects. -/
lemma preservesTerminal_of_isIso (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : IsIso f] :
    PreservesLimit (Functor.empty.{0} C) G := by
  rw [Subsingleton.elim f (terminalComparison G)] at i
  exact PreservesTerminal.of_iso_comparison G

Preservation of Terminal Objects via Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with terminal objects $\top_{\mathcal{C}}$ and $\top_{\mathcal{D}}$, respectively, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. If there exists an isomorphism $f \colon G(\top_{\mathcal{C}}) \to \top_{\mathcal{D}}$, then $G$ preserves terminal objects.

CategoryTheory.Limits.preservesTerminal_of_iso theorem

(f : G.obj (⊤_ C) ≅ ⊤_ D) : PreservesLimit (Functor.empty.{0} C) G

Full source

/-- If there is any isomorphism `G.obj ⊤ ≅ ⊤`, then `G` preserves terminal objects. -/
lemma preservesTerminal_of_iso (f : G.obj (⊤_ C) ≅ ⊤_ D) : PreservesLimit (Functor.empty.{0} C) G :=
  preservesTerminal_of_isIso G f.hom

Preservation of Terminal Objects via Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with terminal objects $\top_{\mathcal{C}}$ and $\top_{\mathcal{D}}$, respectively, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. If there exists an isomorphism $f \colon G(\top_{\mathcal{C}}) \to \top_{\mathcal{D}}$, then $G$ preserves terminal objects.

CategoryTheory.Limits.PreservesTerminal.iso definition

: G.obj (⊤_ C) ≅ ⊤_ D

Full source

/-- If `G` preserves terminal objects, then the terminal comparison map for `G` is an isomorphism.
-/
def PreservesTerminal.iso : G.obj (⊤_ C) ≅ ⊤_ D :=
  (isLimitOfHasTerminalOfPreservesLimit G).conePointUniqueUpToIso (limit.isLimit _)

Isomorphism induced by terminal object preservation

Informal description

Given a functor $ G \colon \mathcal{C} \to \mathcal{D} $ that preserves terminal objects, the isomorphism $ G(\top_{\mathcal{C}}) \cong \top_{\mathcal{D}} $ is induced by the universal property of terminal objects. Here, $ \top_{\mathcal{C}} $ and $ \top_{\mathcal{D}} $ denote the terminal objects in $\mathcal{C}$ and $\mathcal{D}$ respectively.

CategoryTheory.Limits.PreservesTerminal.iso_hom theorem

: (PreservesTerminal.iso G).hom = terminalComparison G

Full source

@[simp]
theorem PreservesTerminal.iso_hom : (PreservesTerminal.iso G).hom = terminalComparison G :=
  rfl

Homomorphism of Terminal Preservation Isomorphism Equals Terminal Comparison Morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves terminal objects, the homomorphism component of the isomorphism $G(\top_{\mathcal{C}}) \cong \top_{\mathcal{D}}$ is equal to the terminal comparison morphism $\mathrm{terminalComparison}\,G$.

CategoryTheory.Limits.instIsIsoTerminalComparison instance

: IsIso (terminalComparison G)

Full source

instance : IsIso (terminalComparison G) := by
  rw [← PreservesTerminal.iso_hom]
  infer_instance

Terminal Comparison Morphism is an Isomorphism

Informal description

The terminal comparison morphism $\mathrm{terminalComparison}\,G$ is an isomorphism.

CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv definition

: IsColimit (G.mapCocone (asEmptyCocone.{v₁} X)) ≃ IsInitial (G.obj X)

Full source

/-- The map of an empty cocone is a colimit iff the mapped object is initial.
-/
def isColimitMapCoconeEmptyCoconeEquiv :
    IsColimitIsColimit (G.mapCocone (asEmptyCocone.{v₁} X)) ≃ IsInitial (G.obj X) :=
  isColimitEmptyCoconeEquiv D _ _ (eqToIso rfl)

Equivalence between colimit of mapped empty cocone and initiality of the image object

Informal description

Given a functor $ G \colon C \to D $ and an object $ X $ in $ C $, there is an equivalence between the following two conditions: 1. The image of the empty cocone with apex $ X $ under $ G $ is a colimit cocone in $ D $. 2. The object $ G(X) $ is initial in $ D $. This equivalence is constructed using the isomorphism induced by the identity morphism on $ G(X) $.

CategoryTheory.Limits.IsInitial.isInitialObj definition

[PreservesColimit (Functor.empty.{0} C) G] (l : IsInitial X) : IsInitial (G.obj X)

Full source

/-- The property of preserving initial objects expressed in terms of `IsInitial`. -/
def IsInitial.isInitialObj [PreservesColimit (Functor.empty.{0} C) G] (l : IsInitial X) :
    IsInitial (G.obj X) :=
  isColimitMapCoconeEmptyCoconeEquiv G X (isColimitOfPreserves G l)

Preservation of initial objects under colimit-preserving functors

Informal description

Let $G : C \to D$ be a functor that preserves colimits of the empty diagram. If an object $X$ in $C$ is initial, then its image $G(X)$ in $D$ is also initial.

CategoryTheory.Limits.IsInitial.isInitialOfObj definition

[ReflectsColimit (Functor.empty.{0} C) G] (l : IsInitial (G.obj X)) : IsInitial X

Full source

/-- The property of reflecting initial objects expressed in terms of `IsInitial`. -/
def IsInitial.isInitialOfObj [ReflectsColimit (Functor.empty.{0} C) G] (l : IsInitial (G.obj X)) :
    IsInitial X :=
  isColimitOfReflects G ((isColimitMapCoconeEmptyCoconeEquiv G X).symm l)

Reflection of initial objects by a functor that reflects empty colimits

Informal description

Given a functor $G \colon C \to D$ that reflects colimits of the empty diagram, if the object $G(X)$ is initial in $D$, then $X$ is initial in $C$.

CategoryTheory.Limits.IsInitial.isInitialIffObj definition

 [PreservesColimit (Functor.empty.{0} C) G] [ReflectsColimit (Functor.empty.{0} C) G] (X : C) :
  IsInitial X ≃ IsInitial (G.obj X)

Full source

/-- A functor that preserves and reflects initial objects induces an equivalence on `IsInitial`. -/
def IsInitial.isInitialIffObj [PreservesColimit (Functor.empty.{0} C) G]
    [ReflectsColimit (Functor.empty.{0} C) G] (X : C) :
    IsInitialIsInitial X ≃ IsInitial (G.obj X) where
  toFun := IsInitial.isInitialObj G X
  invFun := IsInitial.isInitialOfObj G X
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of initiality under a functor preserving and reflecting empty colimits

Informal description

Given a functor $G \colon C \to D$ that both preserves and reflects colimits of the empty diagram, there is an equivalence between the property of an object $X$ in $C$ being initial and its image $G(X)$ in $D$ being initial. Specifically, the equivalence maps: - The proof that $X$ is initial to the proof that $G(X)$ is initial (via preservation) - The proof that $G(X)$ is initial back to the proof that $X$ is initial (via reflection)

CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial theorem

[PreservesColimit (Functor.empty.{0} C) G] : PreservesColimitsOfShape (Discrete PEmpty.{1}) G

Full source

/-- Preserving the initial object implies preserving all colimits of the empty diagram. -/
lemma preservesColimitsOfShape_pempty_of_preservesInitial
    [PreservesColimit (Functor.empty.{0} C) G] :
    PreservesColimitsOfShape (Discrete PEmptyPEmpty.{1}) G where
  preservesColimit :=
    preservesColimit_of_iso_diagram G (Functor.emptyExt (Functor.empty.{0} C) _)

Preservation of Empty Colimits from Initial Object Preservation

Informal description

If a functor $G \colon C \to D$ preserves the initial object (i.e., the colimit of the empty diagram), then $G$ preserves all colimits of the empty diagram (i.e., colimits indexed by the discrete category on the empty type).

CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit definition

[PreservesColimit (Functor.empty.{0} C) G] : IsInitial (G.obj (⊥_ C))

Full source

/-- If `G` preserves the initial object and `C` has an initial object, then the image of the initial
object is initial.
-/
def isColimitOfHasInitialOfPreservesColimit [PreservesColimit (Functor.empty.{0} C) G] :
    IsInitial (G.obj (⊥_ C)) :=
  initialIsInitial.isInitialObj G (⊥_ C)

Preservation of initial objects under colimit-preserving functors

Informal description

If a functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves colimits of the empty diagram (i.e., preserves initial objects), then the image $G(\bot_{\mathcal{C}})$ of the initial object $\bot_{\mathcal{C}}$ in $\mathcal{C}$ is an initial object in $\mathcal{D}$.

CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit theorem

[PreservesColimit (Functor.empty.{0} C) G] : HasInitial D

Full source

/-- 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 hasInitial_of_hasInitial_of_preservesColimit [PreservesColimit (Functor.empty.{0} C) G] :
    HasInitial D :=
  ⟨fun F => by
    haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
    apply hasColimit_of_iso F.uniqueFromEmpty⟩

Existence of Initial Object in Target Category via Initial-Preserving Functor

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves colimits of the empty diagram (i.e., preserves initial objects). If $\mathcal{C}$ has an initial object, then $\mathcal{D}$ also has an initial object.

CategoryTheory.Limits.PreservesInitial.of_iso_comparison theorem

[i : IsIso (initialComparison G)] : PreservesColimit (Functor.empty.{0} C) G

Full source

/-- If the initial comparison map for `G` is an isomorphism, then `G` preserves initial objects.
-/
lemma PreservesInitial.of_iso_comparison [i : IsIso (initialComparison G)] :
    PreservesColimit (Functor.empty.{0} C) G := by
  apply preservesColimit_of_preserves_colimit_cocone initialIsInitial
  apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

Preservation of Initial Objects via Isomorphic Initial Comparison

Informal description

If the initial comparison morphism $\bot_{\mathcal{D}} \to G(\bot_{\mathcal{C}})$ for a functor $G \colon \mathcal{C} \to \mathcal{D}$ is an isomorphism, then $G$ preserves initial objects (i.e., it preserves colimits of the empty diagram).

CategoryTheory.Limits.preservesInitial_of_isIso theorem

(f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] : PreservesColimit (Functor.empty.{0} C) G

Full source

/-- If there is any isomorphism `⊥ ⟶ G.obj ⊥`, then `G` preserves initial objects. -/
lemma preservesInitial_of_isIso (f : ⊥_ D⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] :
    PreservesColimit (Functor.empty.{0} C) G := by
  rw [Subsingleton.elim f (initialComparison G)] at i
  exact PreservesInitial.of_iso_comparison G

Preservation of Initial Objects via Isomorphic Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with initial objects $\bot_{\mathcal{C}}$ and $\bot_{\mathcal{D}}$, respectively, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. If there exists a morphism $f \colon \bot_{\mathcal{D}} \to G(\bot_{\mathcal{C}})$ that is an isomorphism, then $G$ preserves initial objects (i.e., $G$ preserves colimits of the empty diagram).

CategoryTheory.Limits.preservesInitial_of_iso theorem

(f : ⊥_ D ≅ G.obj (⊥_ C)) : PreservesColimit (Functor.empty.{0} C) G

Full source

/-- If there is any isomorphism `⊥ ≅ G.obj ⊥`, then `G` preserves initial objects. -/
lemma preservesInitial_of_iso (f : ⊥_ D⊥_ D ≅ G.obj (⊥_ C)) :
    PreservesColimit (Functor.empty.{0} C) G :=
  preservesInitial_of_isIso G f.hom

Preservation of Initial Objects via Isomorphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with initial objects $\bot_{\mathcal{C}}$ and $\bot_{\mathcal{D}}$, respectively, and let $G \colon \mathcal{C} \to \mathcal{D}$ be a functor. If there exists an isomorphism $f \colon \bot_{\mathcal{D}} \cong G(\bot_{\mathcal{C}})$, then $G$ preserves initial objects (i.e., $G$ preserves colimits of the empty diagram).

CategoryTheory.Limits.PreservesInitial.iso definition

: G.obj (⊥_ C) ≅ ⊥_ D

Full source

/-- If `G` preserves initial objects, then the initial comparison map for `G` is an isomorphism. -/
def PreservesInitial.iso : G.obj (⊥_ C) ≅ ⊥_ D :=
  (isColimitOfHasInitialOfPreservesColimit G).coconePointUniqueUpToIso (colimit.isColimit _)

Isomorphism induced by preservation of initial objects

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves initial objects, the isomorphism `PreservesInitial.iso G` is the unique isomorphism between $G(\bot_{\mathcal{C}})$ and $\bot_{\mathcal{D}}$ induced by the universal property of initial objects.

CategoryTheory.Limits.PreservesInitial.iso_hom theorem

: (PreservesInitial.iso G).inv = initialComparison G

Full source

@[simp]
theorem PreservesInitial.iso_hom : (PreservesInitial.iso G).inv = initialComparison G :=
  rfl

Inverse of Preservation Iso Equals Initial Comparison Morphism

Informal description

Given a functor $G \colon \mathcal{C} \to \mathcal{D}$ that preserves initial objects, the inverse of the isomorphism $\mathrm{PreservesInitial.iso}\,G$ is equal to the initial comparison morphism $\mathrm{initialComparison}\,G$.

CategoryTheory.Limits.instIsIsoInitialComparison instance

: IsIso (initialComparison G)

Full source

instance : IsIso (initialComparison G) := by
  rw [← PreservesInitial.iso_hom]
  infer_instance

Initial Comparison Morphism is an Isomorphism

Informal description

The initial comparison morphism $\bot_{\mathcal{D}} \to G(\bot_{\mathcal{C}})$ is an isomorphism.