Mathlib.CategoryTheory.Limits.HasLimits

CategoryTheory.Limits.LimitCone structure

(F : J ⥤ C)

Full source

/-- `LimitCone F` contains a cone over `F` together with the information that it is a limit. -/
structure LimitCone (F : J ⥤ C) where
  /-- The cone itself -/
  cone : Cone F
  /-- The proof that is the limit cone -/
  isLimit : IsLimit cone

Limit cone of a functor

Informal description

A `LimitCone` for a functor $ F : J \to C $ consists of a cone over $ F $ together with a proof that this cone is a limit cone. That is, it provides both the limit object and the universal property that characterizes it as a limit in the category $ C $.

CategoryTheory.Limits.HasLimit structure

(F : J ⥤ C)

Full source

/-- `HasLimit F` represents the mere existence of a limit for `F`. -/
class HasLimit (F : J ⥤ C) : Prop where mk' ::
  /-- There is some limit cone for `F` -/
  exists_limit : Nonempty (LimitCone F)

Existence of a limit for a functor

Informal description

The proposition `HasLimit F` asserts the existence of a limit cone for the functor `F : J ⥤ C` in a category `C`. This means there exists a cone over `F` that satisfies the universal property of being a limit, i.e., it is terminal among all cones over `F`.

CategoryTheory.Limits.HasLimit.mk theorem

{F : J ⥤ C} (d : LimitCone F) : HasLimit F

Full source

theorem HasLimit.mk {F : J ⥤ C} (d : LimitCone F) : HasLimit F :=
  ⟨Nonempty.intro d⟩

Existence of Limit from Limit Cone

Informal description

Given a functor $F \colon J \to C$ and a limit cone $d$ for $F$, the category $C$ has a limit for $F$.

CategoryTheory.Limits.getLimitCone definition

(F : J ⥤ C) [HasLimit F] : LimitCone F

Full source

/-- Use the axiom of choice to extract explicit `LimitCone F` from `HasLimit F`. -/
def getLimitCone (F : J ⥤ C) [HasLimit F] : LimitCone F :=
  Classical.choice <| HasLimit.exists_limit

Selection of a limit cone for a functor

Informal description

Given a functor $ F : J \to C $ in a category $ C $ for which a limit exists (i.e., `[HasLimit F]`), the definition `getLimitCone F` selects a specific limit cone for $ F $ using the axiom of choice. This provides both the cone object and the proof that it satisfies the universal property of a limit.

CategoryTheory.Limits.HasLimitsOfShape structure

Full source

/-- `C` has limits of shape `J` if there exists a limit for every functor `F : J ⥤ C`. -/
class HasLimitsOfShape : Prop where
  /-- All functors `F : J ⥤ C` from `J` have limits -/
  has_limit : ∀ F : J ⥤ C, HasLimit F := by infer_instance

Existence of limits of shape $J$ in a category $\mathcal{C}$

Informal description

A category $\mathcal{C}$ has limits of shape $J$ if for every functor $F : J \to \mathcal{C}$, there exists a limit cone for $F$. This means there exists a cone over $F$ that satisfies the universal property of being a limit.

CategoryTheory.Limits.HasLimitsOfSize structure

(C : Type u) [Category.{v} C]

Full source

/-- `C` has all limits of size `v₁ u₁` (`HasLimitsOfSize.{v₁ u₁} C`)
if it has limits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
-/
@[pp_with_univ]
class HasLimitsOfSize (C : Type u) [Category.{v} C] : Prop where
  /-- All functors `F : J ⥤ C` from all small `J` have limits -/
  has_limits_of_shape : ∀ (J : Type u₁) [Category.{v₁} J], HasLimitsOfShape J C := by
    infer_instance

Existence of all limits of a given size in a category

Informal description

A category $\mathcal{C}$ is said to have all limits of size $(v_1, u_1)$ if for every small category $\mathcal{J}$ of size $(v_1, u_1)$, the category $\mathcal{C}$ has a limit for every functor $F : \mathcal{J} \to \mathcal{C}$. Here, the size $(v_1, u_1)$ refers to the universe levels of the objects and morphisms in the indexing category $\mathcal{J}$.

CategoryTheory.Limits.HasLimits abbrev

(C : Type u) [Category.{v} C] : Prop

Full source

/-- `C` has all (small) limits if it has limits of every shape that is as big as its hom-sets. -/
abbrev HasLimits (C : Type u) [Category.{v} C] : Prop :=
  HasLimitsOfSize.{v, v} C

Existence of All Small Limits in a Category

Informal description

A category $\mathcal{C}$ has all (small) limits if for every small category $\mathcal{J}$ (where the size of $\mathcal{J}$ is compatible with the hom-sets of $\mathcal{C}$), and for every functor $F : \mathcal{J} \to \mathcal{C}$, there exists a limit cone for $F$.

CategoryTheory.Limits.HasLimits.has_limits_of_shape theorem

{C : Type u} [Category.{v} C] [HasLimits C] (J : Type v) [Category.{v} J] : HasLimitsOfShape J C

Full source

theorem HasLimits.has_limits_of_shape {C : Type u} [Category.{v} C] [HasLimits C] (J : Type v)
    [Category.{v} J] : HasLimitsOfShape J C :=
  HasLimitsOfSize.has_limits_of_shape J

Existence of Limits of Shape $\mathcal{J}$ in a Category with All Limits

Informal description

If a category $\mathcal{C}$ has all (small) limits, then for any small category $\mathcal{J}$ (with size compatible with $\mathcal{C}$), $\mathcal{C}$ has limits of shape $\mathcal{J}$.

CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instance

{J : Type u₁} [Category.{v₁} J] [HasLimitsOfShape J C] (F : J ⥤ C) : HasLimit F

Full source

instance (priority := 100) hasLimitOfHasLimitsOfShape {J : Type u₁} [Category.{v₁} J]
    [HasLimitsOfShape J C] (F : J ⥤ C) : HasLimit F :=
  HasLimitsOfShape.has_limit F

Existence of Limits for Functors in Categories with Limits of Shape $J$

Informal description

For any category $\mathcal{C}$ that has limits of shape $J$, every functor $F : J \to \mathcal{C}$ has a limit.

CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits instance

{J : Type u₁} [Category.{v₁} J] [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfShape J C

Full source

instance (priority := 100) hasLimitsOfShapeOfHasLimits {J : Type u₁} [Category.{v₁} J]
    [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfShape J C :=
  HasLimitsOfSize.has_limits_of_shape J

Existence of Limits of Shape $J$ in Categories with All Limits

Informal description

For any small category $J$ and any category $\mathcal{C}$ that has all limits of size $(v_1, u_1)$, $\mathcal{C}$ has limits of shape $J$.

CategoryTheory.Limits.limit.cone definition

(F : J ⥤ C) [HasLimit F] : Cone F

Full source

/-- An arbitrary choice of limit cone for a functor. -/
def limit.cone (F : J ⥤ C) [HasLimit F] : Cone F :=
  (getLimitCone F).cone

Underlying cone of a limit

Informal description

Given a functor $ F : J \to C $ in a category $ C $ for which a limit exists (i.e., `[HasLimit F]`), the definition `limit.cone F` returns the underlying cone object of the selected limit cone for $ F $. This cone consists of: - An object `limit.cone F`.pt (the limit object) - A natural transformation `limit.cone F`.π from the constant functor at this object to $ F $

CategoryTheory.Limits.limit definition

(F : J ⥤ C) [HasLimit F]

Full source

/-- An arbitrary choice of limit object of a functor. -/
def limit (F : J ⥤ C) [HasLimit F] :=
  (limit.cone F).pt

Limit object of a functor

Informal description

Given a functor $ F : J \to C $ in a category $ C $ for which a limit exists (i.e., `[HasLimit F]`), the definition `limit F` returns an arbitrarily chosen limit object of $ F $. This object serves as the vertex of the limit cone for $ F $, satisfying the universal property that it admits a unique morphism from any other cone over $ F $.

CategoryTheory.Limits.limit.π definition

(F : J ⥤ C) [HasLimit F] (j : J) : limit F ⟶ F.obj j

Full source

/-- The projection from the limit object to a value of the functor. -/
def limit.π (F : J ⥤ C) [HasLimit F] (j : J) : limitlimit F ⟶ F.obj j :=
  (limit.cone F).π.app j

Limit projection morphism

Informal description

For a functor $ F : J \to C $ in a category $ C $ with a limit, the morphism $\pi_j : \text{limit } F \to F(j)$ is the projection from the limit object to the object $F(j)$ in the diagram, where $j$ is an object in the indexing category $J$.

CategoryTheory.Limits.limit.π_comp_eqToHom theorem

(F : J ⥤ C) [HasLimit F] {j j' : J} (hj : j = j') : limit.π F j ≫ eqToHom (by subst hj; rfl) = limit.π F j'

Full source

@[reassoc]
theorem limit.π_comp_eqToHom (F : J ⥤ C) [HasLimit F] {j j' : J} (hj : j = j') :
    limit.πlimit.π F j ≫ eqToHom (by subst hj; rfl) = limit.π F j' := by
  subst hj
  simp

Compatibility of Limit Projections with Object Equality

Informal description

For a functor $F : J \to C$ in a category $C$ that has a limit, and for any objects $j, j' \in J$ with an equality $hj : j = j'$, the composition of the limit projection $\pi_j : \text{limit } F \to F(j)$ with the morphism $\text{eqToHom}(hj) : F(j) \to F(j')$ is equal to the limit projection $\pi_{j'} : \text{limit } F \to F(j')$.

CategoryTheory.Limits.limit.cone_x theorem

{F : J ⥤ C} [HasLimit F] : (limit.cone F).pt = limit F

Full source

@[simp]
theorem limit.cone_x {F : J ⥤ C} [HasLimit F] : (limit.cone F).pt = limit F :=
  rfl

Limit Cone Vertex Equals Limit Object

Informal description

For a functor $F : J \to C$ in a category $C$ that has a limit, the vertex of the limit cone for $F$ is equal to the limit object of $F$, i.e., $(\text{limit.cone } F).\text{pt} = \text{limit } F$.

CategoryTheory.Limits.limit.cone_π theorem

{F : J ⥤ C} [HasLimit F] : (limit.cone F).π.app = limit.π _

Full source

@[simp]
theorem limit.cone_π {F : J ⥤ C} [HasLimit F] : (limit.cone F).π.app = limit.π _ :=
  rfl

Limit Cone Projections Equal Limit Projections

Informal description

For a functor $F : J \to C$ in a category $C$ that has a limit, the natural transformation $\pi$ of the limit cone for $F$ is equal to the family of projection morphisms $\text{limit.π } F$ from the limit object to each $F(j)$.

CategoryTheory.Limits.limit.w theorem

(F : J ⥤ C) [HasLimit F] {j j' : J} (f : j ⟶ j') : limit.π F j ≫ F.map f = limit.π F j'

Full source

@[reassoc (attr := simp)]
theorem limit.w (F : J ⥤ C) [HasLimit F] {j j' : J} (f : j ⟶ j') :
    limit.πlimit.π F j ≫ F.map f = limit.π F j' :=
  (limit.cone F).w f

Commutativity of limit projections with functor morphisms

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a limit, and for any morphism $f \colon j \to j'$ in $J$, the diagram \[ \pi_j \circ F(f) = \pi_{j'} \] commutes, where $\pi_j \colon \mathrm{limit}\, F \to F(j)$ and $\pi_{j'} \colon \mathrm{limit}\, F \to F(j')$ are the limit projection morphisms.

CategoryTheory.Limits.limit.isLimit definition

(F : J ⥤ C) [HasLimit F] : IsLimit (limit.cone F)

Full source

/-- Evidence that the arbitrary choice of cone provided by `limit.cone F` is a limit cone. -/
def limit.isLimit (F : J ⥤ C) [HasLimit F] : IsLimit (limit.cone F) :=
  (getLimitCone F).isLimit

Universal property of the limit cone

Informal description

For a functor $ F : J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), the definition `limit.isLimit F` provides the proof that the cone selected by `limit.cone F` satisfies the universal property of a limit cone. This means it is terminal among all cones over $ F $.

CategoryTheory.Limits.limit.lift definition

(F : J ⥤ C) [HasLimit F] (c : Cone F) : c.pt ⟶ limit F

Full source

/-- The morphism from the cone point of any other cone to the limit object. -/
def limit.lift (F : J ⥤ C) [HasLimit F] (c : Cone F) : c.pt ⟶ limit F :=
  (limit.isLimit F).lift c

Universal morphism from a cone to the limit

Informal description

Given a functor $ F : J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), and given a cone $ c $ over $ F $, the morphism `limit.lift F c` is the unique morphism from the cone point $ c.\mathrm{pt} $ to the limit object $ \mathrm{limit}\, F $ that commutes with the cone maps. Specifically, for each object $ j $ in $ J $, the diagram \[ \mathrm{limit.lift}\, F\, c \circ \mathrm{limit.π}\, F\, j = c.π_j \] commutes, where $ \mathrm{limit.π}\, F\, j $ is the projection from the limit to $ F(j) $.

CategoryTheory.Limits.limit.isLimit_lift theorem

{F : J ⥤ C} [HasLimit F] (c : Cone F) : (limit.isLimit F).lift c = limit.lift F c

Full source

@[simp]
theorem limit.isLimit_lift {F : J ⥤ C} [HasLimit F] (c : Cone F) :
    (limit.isLimit F).lift c = limit.lift F c :=
  rfl

Equality of Limit Lifts via Universal Property

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a limit, and for any cone $c$ over $F$, the lift morphism provided by the universal property of the limit cone equals the canonical limit lift morphism, i.e., $(\mathrm{limit.isLimit}\, F).\mathrm{lift}\, c = \mathrm{limit.lift}\, F\, c$.

CategoryTheory.Limits.limit.lift_π theorem

{F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) : limit.lift F c ≫ limit.π F j = c.π.app j

Full source

@[reassoc (attr := simp)]
theorem limit.lift_π {F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) :
    limit.liftlimit.lift F c ≫ limit.π F j = c.π.app j :=
  IsLimit.fac _ c j

Commutativity of the Universal Morphism with Cone Maps

Informal description

For a functor $ F : J \to C $ in a category $ C $ that has a limit, and for any cone $ c $ over $ F $, the composition of the universal morphism $\text{limit.lift}\, F\, c$ with the projection $\text{limit.π}\, F\, j$ equals the cone map $ c.\pi_j $, i.e., \[ \text{limit.lift}\, F\, c \circ \text{limit.π}\, F\, j = c.\pi_j. \]

CategoryTheory.Limits.limMap definition

{F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) : limit F ⟶ limit G

Full source

/-- Functoriality of limits.

Usually this morphism should be accessed through `lim.map`,
but may be needed separately when you have specified limits for the source and target functors,
but not necessarily for all functors of shape `J`.
-/
def limMap {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) : limitlimit F ⟶ limit G :=
  IsLimit.map _ (limit.isLimit G) α

Induced morphism between limits via natural transformation

Informal description

Given functors $ F, G \colon J \to C $ in a category $ C $ that both have limits (i.e., `[HasLimit F]` and `[HasLimit G]`), and a natural transformation $ \alpha \colon F \to G $, the morphism $\text{limMap}\ \alpha$ is the unique morphism from the limit object of $ F $ to the limit object of $ G $ induced by the universal property of the limit of $ G $.

CategoryTheory.Limits.limMap_π theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) : limMap α ≫ limit.π G j = limit.π F j ≫ α.app j

Full source

@[reassoc (attr := simp)]
theorem limMap_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) :
    limMaplimMap α ≫ limit.π G j = limit.πlimit.π F j ≫ α.app j :=
  limit.lift_π _ j

Commutativity of Limit Morphism with Projections

Informal description

Given functors $ F, G \colon J \to C $ in a category $ C $ that both have limits, and a natural transformation $ \alpha \colon F \Rightarrow G $, the following diagram commutes for every object $ j $ in $ J $: \[ \text{limMap}\, \alpha \circ \pi^G_j = \pi^F_j \circ \alpha_j \] where: - $ \pi^F_j \colon \text{limit}\, F \to F(j) $ and $ \pi^G_j \colon \text{limit}\, G \to G(j) $ are the limit projections, - $ \alpha_j \colon F(j) \to G(j) $ is the component of $ \alpha $ at $ j $, - $ \text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G $ is the induced morphism between the limits.

CategoryTheory.Limits.limit.coneMorphism definition

{F : J ⥤ C} [HasLimit F] (c : Cone F) : c ⟶ limit.cone F

Full source

/-- The cone morphism from any cone to the arbitrary choice of limit cone. -/
def limit.coneMorphism {F : J ⥤ C} [HasLimit F] (c : Cone F) : c ⟶ limit.cone F :=
  (limit.isLimit F).liftConeMorphism c

Universal cone morphism to the limit cone

Informal description

Given a functor $ F : J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), and a cone $ c $ over $ F $, the definition `limit.coneMorphism c` constructs the unique morphism of cones from $ c $ to the chosen limit cone for $ F $. This morphism is determined by the universal property of the limit cone.

CategoryTheory.Limits.limit.coneMorphism_hom theorem

{F : J ⥤ C} [HasLimit F] (c : Cone F) : (limit.coneMorphism c).hom = limit.lift F c

Full source

@[simp]
theorem limit.coneMorphism_hom {F : J ⥤ C} [HasLimit F] (c : Cone F) :
    (limit.coneMorphism c).hom = limit.lift F c :=
  rfl

Universal cone morphism homomorphism equals limit lift

Informal description

For a functor $F \colon J \to C$ in a category $C$ that has a limit, and for any cone $c$ over $F$, the underlying homomorphism of the universal cone morphism from $c$ to the limit cone of $F$ is equal to the universal morphism $\mathrm{limit.lift}\, F\, c$ from the cone point of $c$ to the limit object of $F$.

CategoryTheory.Limits.limit.coneMorphism_π theorem

{F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) : (limit.coneMorphism c).hom ≫ limit.π F j = c.π.app j

Full source

theorem limit.coneMorphism_π {F : J ⥤ C} [HasLimit F] (c : Cone F) (j : J) :
    (limit.coneMorphism c).hom ≫ limit.π F j = c.π.app j := by simp

Commutativity of Universal Cone Morphism with Projections

Informal description

For a functor $F \colon J \to C$ in a category $C$ that has a limit, and for any cone $c$ over $F$, the composition of the homomorphism of the universal cone morphism $\text{limit.coneMorphism}\, c$ with the projection $\text{limit.π}\, F\, j$ equals the cone map $c.\pi_j$, i.e., \[ (\text{limit.coneMorphism}\, c).\text{hom} \circ \text{limit.π}\, F\, j = c.\pi_j. \]

CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp theorem

 {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) :
  (IsLimit.conePointUniqueUpToIso hc (limit.isLimit _)).hom ≫ limit.π F j = c.π.app j

Full source

@[reassoc (attr := simp)]
theorem limit.conePointUniqueUpToIso_hom_comp {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c)
    (j : J) : (IsLimit.conePointUniqueUpToIso hc (limit.isLimit _)).hom ≫ limit.π F j = c.π.app j :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Compatibility of limit cone isomorphism with projections

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a limit. Given a limit cone $c$ over $F$ with universal property witness $hc \colon \mathrm{IsLimit}\, c$, and for any object $j$ in $J$, the isomorphism $\varphi \colon c.\mathrm{pt} \to \mathrm{limit}\, F$ between the apexes of the cones (induced by their universal properties) satisfies $\varphi \circ \pi_j = c.\pi_j$, where $\pi_j \colon \mathrm{limit}\, F \to F(j)$ is the limit projection and $c.\pi_j \colon c.\mathrm{pt} \to F(j)$ is the cone projection.

CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp theorem

 {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) :
  (IsLimit.conePointUniqueUpToIso (limit.isLimit _) hc).inv ≫ limit.π F j = c.π.app j

Full source

@[reassoc (attr := simp)]
theorem limit.conePointUniqueUpToIso_inv_comp {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c)
    (j : J) : (IsLimit.conePointUniqueUpToIso (limit.isLimit _) hc).inv ≫ limit.π F j = c.π.app j :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ _ _

Compatibility of Inverse Isomorphism with Limit Projections

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a limit. Given any limit cone $c$ over $F$ (with $hc$ being the proof that $c$ is a limit cone) and any object $j$ in $J$, the composition of the inverse of the isomorphism between the apexes of the chosen limit cone and $c$ with the projection morphism $\pi_j \colon \text{limit } F \to F(j)$ equals the projection morphism $c.\pi_j \colon c.\mathrm{pt} \to F(j)$.

CategoryTheory.Limits.limit.existsUnique theorem

{F : J ⥤ C} [HasLimit F] (t : Cone F) : ∃! l : t.pt ⟶ limit F, ∀ j, l ≫ limit.π F j = t.π.app j

Full source

theorem limit.existsUnique {F : J ⥤ C} [HasLimit F] (t : Cone F) :
    ∃! l : t.pt ⟶ limit F, ∀ j, l ≫ limit.π F j = t.π.app j :=
  (limit.isLimit F).existsUnique _

Unique Factorization Property of Limits

Informal description

For any functor $ F \colon J \to C $ in a category $ C $ that has a limit, and for any cone $ t $ over $ F $, there exists a unique morphism $ l \colon t.pt \to \text{limit } F $ such that for every object $ j $ in $ J $, the composition $ l \circ \pi_j = t.\pi_j $, where $ \pi_j \colon \text{limit } F \to F(j) $ is the projection morphism from the limit.

CategoryTheory.Limits.limit.isoLimitCone definition

{F : J ⥤ C} [HasLimit F] (t : LimitCone F) : limit F ≅ t.cone.pt

Full source

/-- Given any other limit cone for `F`, the chosen `limit F` is isomorphic to the cone point.
-/
def limit.isoLimitCone {F : J ⥤ C} [HasLimit F] (t : LimitCone F) : limitlimit F ≅ t.cone.pt :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit F) t.isLimit

Isomorphism between chosen limit and any limit cone

Informal description

Given a functor $ F : J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), and given any other limit cone $ t $ for $ F $, there exists an isomorphism between the chosen limit object `limit F` and the apex of the limit cone $ t $. This isomorphism is uniquely determined by the universal properties of the limit cones.

CategoryTheory.Limits.limit.isoLimitCone_hom_π theorem

{F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) : (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j

Full source

@[reassoc (attr := simp)]
theorem limit.isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j := by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  simp

Commutativity of Limit Isomorphism with Projections

Informal description

For any functor $ F \colon J \to C $ in a category $ C $ that has a limit, and for any limit cone $ t $ of $ F $, the composition of the isomorphism $ \text{limit } F \cong t.\text{cone.pt} $ with the projection $ t.\text{cone.π}_j $ equals the projection $ \pi_j \colon \text{limit } F \to F(j) $ for every object $ j $ in $ J $. That is, the following diagram commutes: \[ (\text{limit.isoLimitCone } t).\text{hom} \circ t.\text{cone.π}_j = \pi_j \]

CategoryTheory.Limits.limit.isoLimitCone_inv_π theorem

{F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) : (limit.isoLimitCone t).inv ≫ limit.π F j = t.cone.π.app j

Full source

@[reassoc (attr := simp)]
theorem limit.isoLimitCone_inv_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).inv ≫ limit.π F j = t.cone.π.app j := by
  dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
  simp

Commutativity of Inverse Limit Isomorphism with Projections

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a limit, and let $t$ be a limit cone for $F$. For any object $j$ in $J$, the composition of the inverse of the isomorphism $\text{limit } F \cong t.\text{cone.pt}$ with the projection $\pi_j \colon \text{limit } F \to F(j)$ equals the cone map $t.\text{cone.π}_j$. That is, \[ (\text{limit.isoLimitCone } t)^{-1} \circ \pi_j = t.\text{cone.π}_j. \]

CategoryTheory.Limits.limit.hom_ext theorem

 {F : J ⥤ C} [HasLimit F] {X : C} {f f' : X ⟶ limit F} (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f'

Full source

@[ext]
theorem limit.hom_ext {F : J ⥤ C} [HasLimit F] {X : C} {f f' : X ⟶ limit F}
    (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
  (limit.isLimit F).hom_ext w

Uniqueness of Morphisms into Limit via Projections

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a limit. For any object $X$ in $C$ and any two morphisms $f, f' \colon X \to \text{limit } F$, if for every object $j$ in $J$ the compositions $f \circ \pi_j$ and $f' \circ \pi_j$ are equal (where $\pi_j \colon \text{limit } F \to F(j)$ is the projection morphism), then $f = f'$.

CategoryTheory.Limits.limit.lift_map theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) :
  limit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c)

Full source

@[reassoc (attr := simp)]
theorem limit.lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) :
    limit.liftlimit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c) := by
  ext
  rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
  rfl

Commutativity of Limit Lifting with Natural Transformation

Informal description

Given functors $F, G \colon J \to C$ in a category $C$ that both have limits, a cone $c$ over $F$, and a natural transformation $\alpha \colon F \Rightarrow G$, the following diagram commutes: \[ \text{limit.lift}\, F\, c \circ \text{limMap}\, \alpha = \text{limit.lift}\, G\, (c \circ \alpha) \] where: - $\text{limit.lift}\, F\, c \colon c.\mathrm{pt} \to \text{limit}\, F$ is the universal morphism from the cone $c$ to the limit of $F$, - $\text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G$ is the morphism between limits induced by $\alpha$, - $c \circ \alpha$ denotes the cone over $G$ obtained by postcomposing $c$ with $\alpha$.

CategoryTheory.Limits.limit.lift_cone theorem

{F : J ⥤ C} [HasLimit F] : limit.lift F (limit.cone F) = 𝟙 (limit F)

Full source

@[simp]
theorem limit.lift_cone {F : J ⥤ C} [HasLimit F] : limit.lift F (limit.cone F) = 𝟙 (limit F) :=
  (limit.isLimit _).lift_self

Identity Lift of Limit Cone to Itself

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a limit, the universal morphism from the limit cone of $F$ to itself is the identity morphism on the limit object, i.e., $\mathrm{limit.lift}\, F\, (\mathrm{limit.cone}\, F) = \mathrm{id}_{\mathrm{limit}\, F}$.

CategoryTheory.Limits.limit.homIso definition

(F : J ⥤ C) [HasLimit F] (W : C) : ULift.{u₁} (W ⟶ limit F : Type v) ≅ F.cones.obj (op W)

Full source

/-- The isomorphism (in `Type`) between
morphisms from a specified object `W` to the limit object,
and cones with cone point `W`.
-/
def limit.homIso (F : J ⥤ C) [HasLimit F] (W : C) :
    ULiftULift.{u₁} (W ⟶ limit F : Type v) ≅ F.cones.obj (op W) :=
  (limit.isLimit F).homIso W

Universal property isomorphism for limits

Informal description

Given a functor $ F \colon J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), and an object $ W $ in $ C $, there is a natural isomorphism between the lifted hom-set $ \text{ULift}(W \to \text{limit } F) $ and the set of cones over $ F $ with apex $ W $. More precisely, the isomorphism relates: - Morphisms $ f \colon W \to \text{limit } F $ (lifted via `ULift`) - Natural transformations from the constant functor at $ W $ to $ F $ (i.e., cones over $ F $ with apex $ W $) This isomorphism is a manifestation of the universal property of the limit, showing that morphisms into the limit correspond bijectively to cones over $ F $.

CategoryTheory.Limits.limit.homIso_hom theorem

 (F : J ⥤ C) [HasLimit F] {W : C} (f : ULift (W ⟶ limit F)) :
  (limit.homIso F W).hom f = (const J).map f.down ≫ (limit.cone F).π

Full source

@[simp]
theorem limit.homIso_hom (F : J ⥤ C) [HasLimit F] {W : C} (f : ULift (W ⟶ limit F)) :
    (limit.homIso F W).hom f = (const J).map f.down ≫ (limit.cone F).π :=
  (limit.isLimit F).homIso_hom f

Universal property isomorphism forward map for limits

Informal description

Given a functor $F \colon J \to C$ in a category $C$ that has a limit (i.e., `[HasLimit F]`), and an object $W$ in $C$, the forward map of the universal property isomorphism $\mathrm{homIso}\, F\, W$ applied to a lifted morphism $f \colon W \to \mathrm{limit}\, F$ equals the composition of the constant natural transformation $(W \to \mathrm{limit}\, F)$ with the projection morphisms $(\mathrm{limit.cone}\, F).\pi$ of the limit cone. More precisely, for any morphism $f \colon W \to \mathrm{limit}\, F$, we have: $$(\mathrm{homIso}\, F\, W).\mathrm{hom}\, f = (\mathrm{const}\, J).\mathrm{map}\, f \circ (\mathrm{limit.cone}\, F).\pi$$

CategoryTheory.Limits.limit.homIso' definition

 (F : J ⥤ C) [HasLimit F] (W : C) :
  ULift.{u₁} (W ⟶ limit F : Type v) ≅ { p : ∀ j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }

Full source

/-- The isomorphism (in `Type`) between
morphisms from a specified object `W` to the limit object,
and an explicit componentwise description of cones with cone point `W`.
-/
def limit.homIso' (F : J ⥤ C) [HasLimit F] (W : C) :
    ULiftULift.{u₁} (W ⟶ limit F : Type v) ≅
      { p : ∀ j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
  (limit.isLimit F).homIso' W

Universal property isomorphism for limits (explicit formulation)

Informal description

Given a functor $ F : J \to C $ in a category $ C $ that has a limit (i.e., `[HasLimit F]`), and an object $ W $ in $ C $, there is a natural isomorphism between the lifted hom-set $\text{ULift}(W \to \text{limit}\, F)$ and the set of all cones over $ F $ with apex $ W $. More precisely, this isomorphism identifies a lifted morphism $ f : W \to \text{limit}\, F $ with the family of morphisms $ \{p_j : W \to F.obj\, j\}_{j \in J} $ that satisfy the compatibility condition $ p_j \circ F.map\, f = p_{j'} $ for every morphism $ f : j \to j' $ in $ J $.

CategoryTheory.Limits.limit.lift_extend theorem

{F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) : limit.lift F (c.extend f) = f ≫ limit.lift F c

Full source

theorem limit.lift_extend {F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) :
    limit.lift F (c.extend f) = f ≫ limit.lift F c := by aesop_cat

Compatibility of Limit Lift with Cone Extension

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a limit. For any cone $c$ over $F$ and any morphism $f \colon X \to c.\mathrm{pt}$ in $C$, the universal morphism from the extended cone $c.\mathrm{extend}\, f$ to the limit of $F$ is equal to the composition of $f$ with the universal morphism from $c$ to the limit. In other words, the following diagram commutes: \[ \mathrm{limit.lift}\, F\, (c.\mathrm{extend}\, f) = f \circ \mathrm{limit.lift}\, F\, c \]

CategoryTheory.Limits.hasLimit_of_iso theorem

{F G : J ⥤ C} [HasLimit F] (α : F ≅ G) : HasLimit G

Full source

/-- If a functor `F` has a limit, so does any naturally isomorphic functor.
-/
theorem hasLimit_of_iso {F G : J ⥤ C} [HasLimit F] (α : F ≅ G) : HasLimit G :=
  HasLimit.mk
    { cone := (Cones.postcompose α.hom).obj (limit.cone F)
      isLimit := (IsLimit.postcomposeHomEquiv _ _).symm (limit.isLimit F) }

Existence of limits under natural isomorphism

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$, if $F$ has a limit, then $G$ also has a limit.

CategoryTheory.Limits.hasLimit_iff_of_iso theorem

{F G : J ⥤ C} (α : F ≅ G) : HasLimit F ↔ HasLimit G

Full source

theorem hasLimit_iff_of_iso {F G : J ⥤ C} (α : F ≅ G) : HasLimitHasLimit F ↔ HasLimit G :=
  ⟨fun _ ↦ hasLimit_of_iso α, fun _ ↦ hasLimit_of_iso α.symm⟩

Equivalence of Limit Existence under Natural Isomorphism

Informal description

For any two functors $F, G \colon J \to C$ in a category $C$, if there exists a natural isomorphism $\alpha \colon F \cong G$, then $F$ has a limit if and only if $G$ has a limit.

CategoryTheory.Limits.HasLimit.ofConesIso theorem

 {J K : Type u₁} [Category.{v₁} J] [Category.{v₂} K] (F : J ⥤ C) (G : K ⥤ C) (h : F.cones ≅ G.cones) [HasLimit F] :
  HasLimit G

Full source

/-- If a functor `G` has the same collection of cones as a functor `F`
which has a limit, then `G` also has a limit. -/
theorem HasLimit.ofConesIso {J K : Type u₁} [Category.{v₁} J] [Category.{v₂} K] (F : J ⥤ C)
    (G : K ⥤ C) (h : F.cones ≅ G.cones) [HasLimit F] : HasLimit G :=
  HasLimit.mk ⟨_, IsLimit.ofNatIso (IsLimit.natIso (limit.isLimit F) ≪≫ h)⟩

Existence of Limit via Cone Functor Isomorphism

Informal description

Let $J$ and $K$ be small categories, and let $F \colon J \to C$ and $G \colon K \to C$ be functors. If there exists a natural isomorphism $h$ between their cone functors (i.e., $F.\mathrm{cones} \cong G.\mathrm{cones}$) and $F$ has a limit, then $G$ also has a limit.

CategoryTheory.Limits.HasLimit.isoOfNatIso definition

{F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) : limit F ≅ limit G

Full source

/-- The limits of `F : J ⥤ C` and `G : J ⥤ C` are isomorphic,
if the functors are naturally isomorphic.
-/
def HasLimit.isoOfNatIso {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) : limitlimit F ≅ limit G :=
  IsLimit.conePointsIsoOfNatIso (limit.isLimit F) (limit.isLimit G) w

Isomorphism between limits of naturally isomorphic functors

Informal description

Given two naturally isomorphic functors $ F, G \colon J \to C $ in a category $ C $, both of which have limits (i.e., `[HasLimit F]` and `[HasLimit G]`), there is a canonical isomorphism between their limit objects $ \text{limit } F $ and $ \text{limit } G $. This isomorphism is constructed using the natural isomorphism $ w \colon F \cong G $ and the universal properties of the limits.

CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
  (HasLimit.isoOfNatIso w).hom ≫ limit.π G j = limit.π F j ≫ w.hom.app j

Full source

@[reassoc (attr := simp)]
theorem HasLimit.isoOfNatIso_hom_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
    (HasLimit.isoOfNatIso w).hom ≫ limit.π G j = limit.πlimit.π F j ≫ w.hom.app j :=
  IsLimit.conePointsIsoOfNatIso_hom_comp _ _ _ _

Commutativity of Limit Isomorphism with Projections via Natural Isomorphism

Informal description

Let $F, G \colon J \to C$ be naturally isomorphic functors via $w \colon F \cong G$ in a category $C$, and assume both $F$ and $G$ have limits. Then for any object $j \in J$, the following diagram commutes: \[ (\text{isoOfNatIso}\ w).\text{hom} \circ \pi^G_j = \pi^F_j \circ w.\text{hom}_j \] where $\pi^F_j \colon \text{limit } F \to F(j)$ and $\pi^G_j \colon \text{limit } G \to G(j)$ are the limit projections, and $\text{isoOfNatIso}\ w$ is the isomorphism between $\text{limit } F$ and $\text{limit } G$ induced by $w$.

CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
  (HasLimit.isoOfNatIso w).inv ≫ limit.π F j = limit.π G j ≫ w.inv.app j

Full source

@[reassoc (attr := simp)]
theorem HasLimit.isoOfNatIso_inv_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) :
    (HasLimit.isoOfNatIso w).inv ≫ limit.π F j = limit.πlimit.π G j ≫ w.inv.app j :=
  IsLimit.conePointsIsoOfNatIso_inv_comp _ _ _ _

Commutativity of Inverse Limit Isomorphism with Projections via Natural Isomorphism

Informal description

For any two naturally isomorphic functors $ F, G \colon J \to C $ in a category $ C $ that both have limits, and for any object $ j \in J $, the following diagram commutes: \[ (\text{isoOfNatIso}\ w)^{-1} \circ \pi^F_j = \pi^G_j \circ w^{-1}_j \] where: - $\text{isoOfNatIso}\ w$ is the canonical isomorphism between the limits $\text{limit}\ F$ and $\text{limit}\ G$ induced by the natural isomorphism $w \colon F \cong G$, - $\pi^F_j \colon \text{limit}\ F \to F(j)$ and $\pi^G_j \colon \text{limit}\ G \to G(j)$ are the limit projection morphisms, - $w^{-1}_j \colon G(j) \to F(j)$ is the component of the inverse natural isomorphism at $j$.

CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (t : Cone F) (w : F ≅ G) :
  limit.lift F t ≫ (HasLimit.isoOfNatIso w).hom = limit.lift G ((Cones.postcompose w.hom).obj _)

Full source

@[reassoc (attr := simp)]
theorem HasLimit.lift_isoOfNatIso_hom {F G : J ⥤ C} [HasLimit F] [HasLimit G] (t : Cone F)
    (w : F ≅ G) :
    limit.liftlimit.lift F t ≫ (HasLimit.isoOfNatIso w).hom =
      limit.lift G ((Cones.postcompose w.hom).obj _) :=
  IsLimit.lift_comp_conePointsIsoOfNatIso_hom _ _ _

Compatibility of Limit Lifting with Natural Isomorphism

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$ that both have limits, a cone $t$ over $F$, and a natural isomorphism $w \colon F \cong G$, the following diagram commutes: \[ \text{limit.lift}\, F\, t \circ (\text{HasLimit.isoOfNatIso}\, w).\text{hom} = \text{limit.lift}\, G\, ((\text{Cones.postcompose}\, w.\text{hom}).\text{obj}\, t) \] Here: - $\text{limit.lift}\, F\, t$ is the universal morphism from the cone $t$ to the limit of $F$, - $\text{HasLimit.isoOfNatIso}\, w$ is the isomorphism between the limits of $F$ and $G$ induced by $w$, - $\text{Cones.postcompose}\, w.\text{hom}$ transforms the cone $t$ over $F$ into a cone over $G$ by postcomposing with $w.\text{hom}$, - $\text{limit.lift}\, G$ is the universal morphism from the transformed cone to the limit of $G$.

CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv theorem

 {F G : J ⥤ C} [HasLimit F] [HasLimit G] (t : Cone G) (w : F ≅ G) :
  limit.lift G t ≫ (HasLimit.isoOfNatIso w).inv = limit.lift F ((Cones.postcompose w.inv).obj _)

Full source

@[reassoc (attr := simp)]
theorem HasLimit.lift_isoOfNatIso_inv {F G : J ⥤ C} [HasLimit F] [HasLimit G] (t : Cone G)
    (w : F ≅ G) :
    limit.liftlimit.lift G t ≫ (HasLimit.isoOfNatIso w).inv =
      limit.lift F ((Cones.postcompose w.inv).obj _) :=
  IsLimit.lift_comp_conePointsIsoOfNatIso_inv _ _ _

Compatibility of limit lifts with natural isomorphism inverses

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$ that both have limits, and given a cone $t$ over $G$, the following diagram commutes: \[ \text{limit.lift}\, G\, t \circ (\text{isoOfNatIso}\, w)^{-1} = \text{limit.lift}\, F\, ((\text{Cones.postcompose}\, w^{-1}).\text{obj}\, t) \] where: - $\text{limit.lift}\, G\, t$ is the universal morphism from $t$ to the limit of $G$, - $\text{isoOfNatIso}\, w$ is the isomorphism between the limits of $F$ and $G$ induced by the natural isomorphism $w \colon F \cong G$, - $\text{Cones.postcompose}\, w^{-1}$ transforms the cone $t$ over $G$ into a cone over $F$ by postcomposing with $w^{-1}$.

CategoryTheory.Limits.HasLimit.isoOfEquivalence definition

{F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) : limit F ≅ limit G

Full source

/-- The limits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
if there is an equivalence `e : J ≌ K` making the triangle commute up to natural isomorphism.
-/
def HasLimit.isoOfEquivalence {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K)
    (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) : limitlimit F ≅ limit G :=
  IsLimit.conePointsIsoOfEquivalence (limit.isLimit F) (limit.isLimit G) e w

Isomorphism of limits under equivalence of indexing categories

Informal description

Given two functors $ F \colon J \to C $ and $ G \colon K \to C $ in a category $ C $ that both have limits, and an equivalence of categories $ e \colon J \simeq K $ such that the composition $ e.\text{functor} \circ G $ is naturally isomorphic to $ F $, the limit objects $ \text{limit}\, F $ and $ \text{limit}\, G $ are isomorphic in $ C $.

CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π theorem

 {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) :
  (HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Full source

@[simp]
theorem HasLimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G]
    (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) (k : K) :
    (HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k =
      limit.πlimit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) := by
  simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
  dsimp
  simp

Commutativity of limit isomorphism with projections under equivalence of indexing categories

Informal description

Given two functors $F \colon J \to C$ and $G \colon K \to C$ in a category $C$ that both have limits, an equivalence of categories $e \colon J \simeq K$, and a natural isomorphism $w \colon e.\text{functor} \circ G \cong F$, the following diagram commutes for any object $k$ in $K$: \[ (\text{isoOfEquivalence}\, e\, w).\text{hom} \circ \pi_G(k) = \pi_F(e^{-1}(k)) \circ w^{-1}_{e^{-1}(k)} \circ G(\epsilon_k), \] where: - $\text{isoOfEquivalence}\, e\, w$ is the isomorphism between the limits of $F$ and $G$, - $\pi_G(k)$ is the projection from the limit of $G$ to $G(k)$, - $\pi_F(e^{-1}(k))$ is the projection from the limit of $F$ to $F(e^{-1}(k))$, - $w^{-1}_{e^{-1}(k)}$ is the component of the inverse natural isomorphism at $e^{-1}(k)$, - $\epsilon_k$ is the counit of the equivalence $e$ at $k$, - $G(\epsilon_k)$ is the image of $\epsilon_k$ under the functor $G$.

CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π theorem

 {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) :
  (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j

Full source

@[simp]
theorem HasLimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G]
    (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) (j : J) :
    (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j =
    limit.πlimit.π G (e.functor.obj j) ≫ w.hom.app j := by
  simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
  dsimp
  simp

Commutativity of inverse limit isomorphism with projections under equivalence of indexing categories

Informal description

Given two functors $F \colon J \to C$ and $G \colon K \to C$ in a category $C$ that both have limits, an equivalence of categories $e \colon J \simeq K$, and a natural isomorphism $w \colon e.\text{functor} \circ G \cong F$, the following diagram commutes for any object $j$ in $J$: \[ (\text{isoOfEquivalence}\, e\, w)^{-1} \circ \pi_F(j) = \pi_G(e(j)) \circ w_j, \] where: - $(\text{isoOfEquivalence}\, e\, w)^{-1}$ is the inverse of the isomorphism between the limits of $F$ and $G$, - $\pi_F(j)$ is the projection from the limit of $F$ to $F(j)$, - $\pi_G(e(j))$ is the projection from the limit of $G$ to $G(e(j))$, - $w_j$ is the component of the natural isomorphism $w$ at $j$.

CategoryTheory.Limits.limit.pre definition

: limit F ⟶ limit (E ⋙ F)

Full source

/-- The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.
-/
def limit.pre : limitlimit F ⟶ limit (E ⋙ F) :=
  limit.lift (E ⋙ F) ((limit.cone F).whisker E)

Canonical morphism from limit to precomposition limit

Informal description

Given a functor $ F : J \to C $ with a limit and a functor $ E : K \to J $, the morphism $\text{limit.pre}\, F\, E$ is the canonical morphism from the limit of $ F $ to the limit of the composition $ E \circ F $. This morphism is constructed by lifting the whiskered cone of the limit cone of $ F $ along $ E $ to the limit of $ E \circ F $.

CategoryTheory.Limits.limit.pre_π theorem

(k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k)

Full source

@[reassoc (attr := simp)]
theorem limit.pre_π (k : K) : limit.prelimit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) := by
  erw [IsLimit.fac]
  rfl

Compatibility of limit precomposition with projections

Informal description

For any object $k$ in the category $K$, the composition of the canonical morphism $\text{limit.pre}\, F\, E$ from the limit of $F$ to the limit of $E \circ F$ with the projection $\pi_k$ from the limit of $E \circ F$ to $(E \circ F)(k)$ equals the projection $\pi_{E(k)}$ from the limit of $F$ to $F(E(k))$. In symbols: \[ \text{limit.pre}\, F\, E \circ \pi_k = \pi_{E(k)}. \]

CategoryTheory.Limits.limit.lift_pre theorem

(c : Cone F) : limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E)

Full source

@[simp]
theorem limit.lift_pre (c : Cone F) :
    limit.liftlimit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) := by ext; simp

Compatibility of Limit Lift with Precomposition

Informal description

Given a functor $F \colon J \to C$ with a limit, a cone $c$ over $F$, and a functor $E \colon K \to J$, the composition of the universal morphism $\mathrm{limit.lift}\, F\, c$ with the canonical morphism $\mathrm{limit.pre}\, F\, E$ equals the universal morphism $\mathrm{limit.lift}\, (E \circ F)\, (c.\mathrm{whisker}\, E)$. In symbols: \[ \mathrm{limit.lift}\, F\, c \circ \mathrm{limit.pre}\, F\, E = \mathrm{limit.lift}\, (E \circ F)\, (c.\mathrm{whisker}\, E). \]

CategoryTheory.Limits.limit.pre_pre theorem

 [h : HasLimit (D ⋙ E ⋙ F)] :
  haveI : HasLimit ((D ⋙ E) ⋙ F) := h
  limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E)

Full source

@[simp]
theorem limit.pre_pre [h : HasLimit (D ⋙ E ⋙ F)] : haveI : HasLimit ((D ⋙ E) ⋙ F) := h
    limit.prelimit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E) := by
  haveI : HasLimit ((D ⋙ E) ⋙ F) := h
  ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; rfl

Composition of Precomposition Limits Morphisms

Informal description

Given functors $D \colon K \to J$, $E \colon J \to C$, and $F \colon C \to D$ such that the composition $D \circ E \circ F$ has a limit, the composition of the canonical morphisms \[ \text{limit.pre}\, F\, E \circ \text{limit.pre}\, (E \circ F)\, D \] equals the canonical morphism \[ \text{limit.pre}\, F\, (D \circ E). \]

CategoryTheory.Limits.limit.pre_eq theorem

 (s : LimitCone (E ⋙ F)) (t : LimitCone F) :
  limit.pre F E = (limit.isoLimitCone t).hom ≫ s.isLimit.lift (t.cone.whisker E) ≫ (limit.isoLimitCone s).inv

Full source

/-- -
If we have particular limit cones available for `E ⋙ F` and for `F`,
we obtain a formula for `limit.pre F E`.
-/
theorem limit.pre_eq (s : LimitCone (E ⋙ F)) (t : LimitCone F) :
    limit.pre F E = (limit.isoLimitCone t).hom ≫ s.isLimit.lift (t.cone.whisker E) ≫
      (limit.isoLimitCone s).inv := by aesop_cat

Expression of limit precomposition morphism via limit cones

Informal description

Given functors $E \colon K \to J$ and $F \colon J \to C$, and given limit cones $s$ for $E \circ F$ and $t$ for $F$, the canonical morphism $\mathrm{limit.pre}\, F\, E$ from the limit of $F$ to the limit of $E \circ F$ can be expressed as the composition: \[ \mathrm{limit.pre}\, F\, E = (\mathrm{limit.isoLimitCone}\, t).\mathrm{hom} \circ s.\mathrm{isLimit.lift}\, (t.\mathrm{cone.whisker}\, E) \circ (\mathrm{limit.isoLimitCone}\, s).\mathrm{inv} \] where: - $(\mathrm{limit.isoLimitCone}\, t).\mathrm{hom}$ is the isomorphism from the chosen limit of $F$ to the apex of $t$, - $s.\mathrm{isLimit.lift}\, (t.\mathrm{cone.whisker}\, E)$ is the universal morphism from the whiskered cone to the limit of $E \circ F$, - $(\mathrm{limit.isoLimitCone}\, s).\mathrm{inv}$ is the inverse isomorphism from the apex of $s$ to the chosen limit of $E \circ F$.

CategoryTheory.Limits.limit.post definition

: G.obj (limit F) ⟶ limit (F ⋙ G)

Full source

/-- The canonical morphism from `G` applied to the limit of `F` to the limit of `F ⋙ G`.
-/
def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
  limit.lift (F ⋙ G) (G.mapCone (limit.cone F))

Canonical map from image of limit to limit of composition

Informal description

Given functors $ F \colon J \to C $ and $ G \colon C \to D $, where $ C $ and $ D $ are categories and $ F $ has a limit, the morphism $ G(\mathrm{limit}\, F) \to \mathrm{limit}\, (F \circ G) $ is the canonical map induced by applying $ G $ to the limit cone of $ F $. This map is constructed as the universal morphism from the image of the limit cone under $ G $ to the limit of the composition $ F \circ G $.

CategoryTheory.Limits.limit.post_π theorem

(j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j)

Full source

@[reassoc (attr := simp)]
theorem limit.post_π (j : J) : limit.postlimit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) := by
  erw [IsLimit.fac]
  rfl

Compatibility of Post with Projections: $\mathrm{post} \circ \pi_j = G(\pi_j)$

Informal description

For any object $j$ in the indexing category $J$, the composition of the canonical morphism $\mathrm{post} \colon G(\mathrm{limit}\, F) \to \mathrm{limit}\, (F \circ G)$ with the projection $\pi_j \colon \mathrm{limit}\, (F \circ G) \to G(F(j))$ is equal to the image under $G$ of the projection $\pi_j \colon \mathrm{limit}\, F \to F(j)$. In symbols: \[ \mathrm{post} \circ \pi_j = G(\pi_j). \]

CategoryTheory.Limits.limit.lift_post theorem

(c : Cone F) : G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c)

Full source

@[simp]
theorem limit.lift_post (c : Cone F) :
    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c) := by
  ext
  rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]
  rfl

Compatibility of Lift and Post: $G(\mathrm{lift}) \circ \mathrm{post} = \mathrm{lift}(G(c))$

Informal description

Given a functor $F \colon J \to C$ with a limit, a cone $c$ over $F$, and a functor $G \colon C \to D$, the composition of the image under $G$ of the universal morphism $\mathrm{limit.lift}\, F\, c$ with the canonical morphism $\mathrm{limit.post}\, F\, G$ equals the universal morphism from the image cone $G(c)$ to the limit of the composition $F \circ G$. In symbols: \[ G(\mathrm{limit.lift}\, F\, c) \circ \mathrm{limit.post}\, F\, G = \mathrm{limit.lift}\, (F \circ G)\, (G(c)). \]

CategoryTheory.Limits.limit.post_post theorem

 {E : Type u''} [Category.{v''} E] (H : D ⥤ E) [h : HasLimit ((F ⋙ G) ⋙ H)] :
  -- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals
      -- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H))haveI : HasLimit (F ⋙ G ⋙ H) := h
  H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H)

Full source

@[simp]
theorem limit.post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E) [h : HasLimit ((F ⋙ G) ⋙ H)] :
    -- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals
    -- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H))
    haveI : HasLimit (F ⋙ G ⋙ H) := h
    H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H) := by
  haveI : HasLimit (F ⋙ G ⋙ H) := h
  ext; erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]; rfl

Composition of Post Maps: $H(\mathrm{post}_{F,G}) \circ \mathrm{post}_{F \circ G,H} = \mathrm{post}_{F,G \circ H}$

Informal description

Let $C$, $D$, and $E$ be categories, and let $F \colon J \to C$, $G \colon C \to D$, and $H \colon D \to E$ be functors. Suppose the composition $(F \circ G) \circ H$ has a limit. Then the composition of the canonical maps \[ H(\mathrm{post}_{F,G}) \circ \mathrm{post}_{F \circ G,H} \colon H(G(\mathrm{limit}\, F)) \to \mathrm{limit}\, ((F \circ G) \circ H) \] equals the canonical map \[ \mathrm{post}_{F,G \circ H} \colon G(\mathrm{limit}\, F) \to \mathrm{limit}\, (F \circ (G \circ H)), \] where $\mathrm{post}_{F,G}$ denotes the canonical map $G(\mathrm{limit}\, F) \to \mathrm{limit}\, (F \circ G)$.

CategoryTheory.Limits.limit.pre_post theorem

 {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D) [HasLimit F] [HasLimit (E ⋙ F)] [HasLimit (F ⋙ G)]
  [h : HasLimit ((E ⋙ F) ⋙ G)] :
  -- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs
              -- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) orhaveI : HasLimit (E ⋙ F ⋙ G) := h
  G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E

Full source

theorem limit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
    [HasLimit F] [HasLimit (E ⋙ F)] [HasLimit (F ⋙ G)]
    [h : HasLimit ((E ⋙ F) ⋙ G)] :-- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs
            -- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or
    haveI : HasLimit (E ⋙ F ⋙ G) := h
    G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.postlimit.post F G ≫ limit.pre (F ⋙ G) E := by
  haveI : HasLimit (E ⋙ F ⋙ G) := h
  ext; erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]

Commutativity of Precomposition and Postcomposition for Limits

Informal description

Let $C$, $D$ be categories, and let $E \colon K \to J$, $F \colon J \to C$, $G \colon C \to D$ be functors. Suppose $F$, $E \circ F$, $F \circ G$, and $(E \circ F) \circ G$ all have limits. Then the following diagram commutes: \[ G(\mathrm{limit}\, F) \xrightarrow{G(\mathrm{pre})} G(\mathrm{limit}\, (E \circ F)) \xrightarrow{\mathrm{post}} \mathrm{limit}\, ((E \circ F) \circ G) \] \[ G(\mathrm{limit}\, F) \xrightarrow{\mathrm{post}} \mathrm{limit}\, (F \circ G) \xrightarrow{\mathrm{pre}} \mathrm{limit}\, (E \circ (F \circ G)) \] where $\mathrm{pre}$ and $\mathrm{post}$ denote the canonical morphisms associated with limit precomposition and postcomposition respectively.

CategoryTheory.Limits.hasLimitEquivalenceComp instance

(e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F)

Full source

instance hasLimitEquivalenceComp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
  HasLimit.mk
    { cone := Cone.whisker e.functor (limit.cone F)
      isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }

Preservation of Limits under Precomposition with Equivalence

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a functor $F \colon J \to C$ that has a limit in $C$, the composition $e.\text{functor} \circ F \colon K \to C$ also has a limit in $C$.

CategoryTheory.Limits.hasLimitOfEquivalenceComp theorem

(e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F

Full source

/-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
-/
theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F := by
  haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm
  apply hasLimit_of_iso (e.invFunIdAssoc F)

Existence of Limit for Functor Composed with Equivalence Inverse

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a functor $F \colon J \to C$, if the composition $e.\text{functor} \circ F \colon K \to C$ has a limit, then $F$ itself has a limit in $C$.

CategoryTheory.Limits.lim definition

: (J ⥤ C) ⥤ C

Full source

/-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`. -/
@[simps]
def lim : (J ⥤ C) ⥤ C where
  obj F := limit F
  map α := limMap α
  map_id F := by
    apply Limits.limit.hom_ext; intro j
    simp
  map_comp α β := by
    apply Limits.limit.hom_ext; intro j
    simp [assoc]

Limit functor

Informal description

The functor $\text{lim} \colon (J \to C) \to C$ assigns to each functor $F \colon J \to C$ its limit object $\text{limit}\, F$ (when it exists), and to each natural transformation $\alpha \colon F \to G$ the induced morphism $\text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G$ between the corresponding limits. This functor respects identities and compositions of natural transformations, as verified by the universal property of limits.

CategoryTheory.Limits.limMap_eq theorem

: limMap α = lim.map α

Full source

theorem limMap_eq : limMap α = lim.map α := rfl

Equality of Induced Morphism and Limit Functor Application

Informal description

Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon J \to C$ in a category $C$ that has limits for both $F$ and $G$, the induced morphism $\text{limMap}\,\alpha$ between their limits is equal to the image of $\alpha$ under the limit functor $\text{lim} \colon (J \to C) \to C$.

CategoryTheory.Limits.limit.map_pre theorem

[HasLimitsOfShape K C] (E : K ⥤ J) : lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α)

Full source

theorem limit.map_pre [HasLimitsOfShape K C] (E : K ⥤ J) :
    limlim.map α ≫ limit.pre G E = limit.prelimit.pre F E ≫ lim.map (whiskerLeft E α) := by
  ext
  simp

Commutativity of Limit Morphism with Precomposition

Informal description

Let $\mathcal{C}$ be a category with limits of shape $K$, and let $F, G \colon J \to \mathcal{C}$ be functors with a natural transformation $\alpha \colon F \to G$. For any functor $E \colon K \to J$, the following diagram commutes: \[ \text{limMap}\, \alpha \circ \text{limit.pre}\, G\, E = \text{limit.pre}\, F\, E \circ \text{limMap}\, (\text{whiskerLeft}\, E\, \alpha) \] where: - $\text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G$ is the morphism induced by $\alpha$, - $\text{limit.pre}\, F\, E \colon \text{limit}\, F \to \text{limit}\, (E \circ F)$ is the canonical morphism from the limit of $F$ to the limit of the composition $E \circ F$, - $\text{whiskerLeft}\, E\, \alpha$ is the natural transformation obtained by precomposing $\alpha$ with $E$.

CategoryTheory.Limits.limit.map_pre' theorem

 [HasLimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
  limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whiskerRight α F)

Full source

theorem limit.map_pre' [HasLimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
    limit.pre F E₂ = limit.prelimit.pre F E₁ ≫ lim.map (whiskerRight α F) := by
  ext1; simp [← category.assoc]

Compatibility of limit precomposition with natural transformations

Informal description

Let $\mathcal{C}$ be a category that has limits of shape $K$, and let $F \colon J \to \mathcal{C}$ be a functor. For any two functors $E_1, E_2 \colon K \to J$ and a natural transformation $\alpha \colon E_1 \to E_2$, the following diagram commutes: \[ \text{limit.pre}\, F\, E_2 = \text{limit.pre}\, F\, E_1 \circ \text{limMap}\, (\alpha \circ F), \] where: - $\text{limit.pre}\, F\, E_i$ is the canonical morphism from the limit of $F$ to the limit of $E_i \circ F$ ($i = 1, 2$), - $\text{limMap}\, (\alpha \circ F)$ is the morphism between the limits of $E_1 \circ F$ and $E_2 \circ F$ induced by the whiskered natural transformation $\alpha \circ F$.

CategoryTheory.Limits.limit.id_pre theorem

(F : J ⥤ C) : limit.pre F (𝟭 _) = lim.map (Functor.leftUnitor F).inv

Full source

theorem limit.id_pre (F : J ⥤ C) : limit.pre F (𝟭 _) = lim.map (Functor.leftUnitor F).inv := by
  aesop_cat

Identity Precomposition Preserves Limit Morphism

Informal description

For any functor $F \colon J \to C$, the canonical morphism $\text{limit.pre}\, F\, \text{id}_J$ from the limit of $F$ to the limit of $F \circ \text{id}_J$ equals the morphism induced by the inverse of the left unitor natural isomorphism of $F$.

CategoryTheory.Limits.limit.map_post theorem

 {D : Type u'} [Category.{v'} D] [HasLimitsOfShape J D] (H : C ⥤ D) :
  /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
       H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/H.map (limMap α) ≫ limit.post G H =
    limit.post F H ≫ limMap (whiskerRight α H)

Full source

theorem limit.map_post {D : Type u'} [Category.{v'} D] [HasLimitsOfShape J D] (H : C ⥤ D) :
    /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
     H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
    H.map (limMap α) ≫ limit.post G H = limit.postlimit.post F H ≫ limMap (whiskerRight α H) := by
  ext
  simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]

Commutativity of Post-Limit Morphism with Functor Application: $H(\text{limMap}\, \alpha) \circ \text{post}_G^H = \text{post}_F^H \circ \text{limMap}\, (\alpha \circ H)$

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories where $\mathcal{D}$ has limits of shape $J$, and let $H \colon \mathcal{C} \to \mathcal{D}$ be a functor. For any natural transformation $\alpha \colon F \to G$ between functors $F, G \colon J \to \mathcal{C}$, the following diagram commutes: \[ H(\text{limMap}\, \alpha) \circ \text{post}_G^H = \text{post}_F^H \circ \text{limMap}\, (\alpha \circ H), \] where: - $\text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G$ is the morphism induced by $\alpha$ between limits, - $\text{post}_F^H \colon H(\text{limit}\, F) \to \text{limit}\, (F \circ H)$ and $\text{post}_G^H \colon H(\text{limit}\, G) \to \text{limit}\, (G \circ H)$ are the canonical morphisms, - $\alpha \circ H$ denotes the whiskering of $\alpha$ with $H$.

CategoryTheory.Limits.limYoneda definition

: lim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cones J C

Full source

/-- The isomorphism between
morphisms from `W` to the cone point of the limit cone for `F`
and cones over `F` with cone point `W`
is natural in `F`.
-/
def limYoneda :
    limlim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}lim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cones J C :=
  NatIso.ofComponents fun F => NatIso.ofComponents fun W => limit.homIso F (unop W)

Yoneda-Limit Cone Isomorphism

Informal description

The natural isomorphism between the functor $\mathrm{lim} \circ \mathrm{y} \circ \mathrm{uliftFunctor}$ and the functor of cones over diagrams of shape $J$ in the category $C$. Here, $\mathrm{lim}$ is the limit functor, $\mathrm{y}$ is the Yoneda embedding, and $\mathrm{uliftFunctor}$ is the type lifting functor. This isomorphism expresses that morphisms into a limit object correspond naturally to cones over the diagram. More precisely, for any functor $F \colon J \to C$ and any object $W$ in $C^{\mathrm{op}}$, the isomorphism relates: - Morphisms from $W$ to the limit of $F$ (lifted via $\mathrm{ULift}$) - Cones over $F$ with apex $W$ This is a categorical formulation of the universal property of limits, showing that the limit functor is naturally isomorphic to the functor of cones via the Yoneda embedding and type lifting.

CategoryTheory.Limits.constLimAdj definition

: (const J : C ⥤ J ⥤ C) ⊣ lim

Full source

/-- The constant functor and limit functor are adjoint to each other -/
def constLimAdj : (const J : C ⥤ J ⥤ C) ⊣ lim := Adjunction.mk' {
  homEquiv := fun c g ↦
    { toFun := fun f => limit.lift _ ⟨c, f⟩
      invFun := fun f =>
        { app := fun _ => f ≫ limit.π _ _ }
      left_inv := by aesop_cat
      right_inv := by aesop_cat }
  unit := { app := fun _ => limit.lift _ ⟨_, 𝟙 _⟩ }
  counit := { app := fun g => { app := limit.π _ } } }

Adjunction between constant functor and limit functor

Informal description

The constant functor $\text{const}_J \colon \mathcal{C} \to (J \to \mathcal{C})$ is left adjoint to the limit functor $\text{lim} \colon (J \to \mathcal{C}) \to \mathcal{C}$. This means there is a natural bijection between morphisms $c \to \text{lim}\, G$ in $\mathcal{C}$ and natural transformations $\text{const}_J\, c \to G$ in the functor category $J \to \mathcal{C}$.

CategoryTheory.Limits.instIsRightAdjointFunctorLim instance

: IsRightAdjoint (lim : (J ⥤ C) ⥤ C)

Full source

instance : IsRightAdjoint (lim : (J ⥤ C) ⥤ C) :=
  ⟨_, ⟨constLimAdj⟩⟩

The Limit Functor is a Right Adjoint

Informal description

The limit functor $\text{lim} \colon (J \to \mathcal{C}) \to \mathcal{C}$ is a right adjoint functor. This means there exists a left adjoint functor to $\text{lim}$, which is the constant functor $\text{const}_J \colon \mathcal{C} \to (J \to \mathcal{C})$, establishing an adjunction between them.

CategoryTheory.Limits.limMap_mono' instance

{F G : J ⥤ C} [HasLimitsOfShape J C] (α : F ⟶ G) [Mono α] : Mono (limMap α)

Full source

instance limMap_mono' {F G : J ⥤ C} [HasLimitsOfShape J C] (α : F ⟶ G) [Mono α] : Mono (limMap α) :=
  (lim : (J ⥤ C) ⥤ C).map_mono α

Monomorphic Natural Transformation Induces Monomorphism on Limits of Shape $J$

Informal description

For any functors $F, G \colon J \to \mathcal{C}$ in a category $\mathcal{C}$ with limits of shape $J$, if a natural transformation $\alpha \colon F \Rightarrow G$ is a monomorphism (i.e., injective in each component), then the induced morphism $\text{limMap}\, \alpha \colon \text{lim}\, F \to \text{lim}\, G$ between their limits is also a monomorphism.

CategoryTheory.Limits.limMap_mono instance

{F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [∀ j, Mono (α.app j)] : Mono (limMap α)

Full source

instance limMap_mono {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [∀ j, Mono (α.app j)] :
    Mono (limMap α) :=
  ⟨fun {Z} u v h =>
    limit.hom_ext fun j => (cancel_mono (α.app j)).1 <| by simpa using h =≫ limit.π _ j⟩

Monomorphic Natural Transformation Induces Monomorphism on Limits

Informal description

Given functors $ F, G \colon J \to C $ in a category $ C $ that both have limits, and a natural transformation $ \alpha \colon F \Rightarrow G $ such that each component $ \alpha_j \colon F(j) \to G(j) $ is a monomorphism, the induced morphism $\text{limMap}\, \alpha \colon \text{limit}\, F \to \text{limit}\, G$ is also a monomorphism.

CategoryTheory.Limits.coneOfAdj definition

(F : J ⥤ C) : Cone F

Full source

/-- The limit cone obtained from a right adjoint of the constant functor. -/
@[simps]
noncomputable def coneOfAdj (F : J ⥤ C) : Cone F where
  pt := L.obj F
  π := adj.counit.app F

Cone construction via right adjoint to constant functor

Informal description

Given a right adjoint functor $L \colon C \to D$ to the constant functor $\Delta \colon D \to C$, the cone over a functor $F \colon J \to C$ is constructed with: - The cone point being $L(F)$ (the image of $F$ under $L$), - The natural transformation $\pi$ given by the counit of the adjunction applied to $F$. This construction yields a cone over $F$ where the components of the natural transformation are determined by the counit of the adjunction.

CategoryTheory.Limits.isLimitConeOfAdj definition

(F : J ⥤ C) : IsLimit (coneOfAdj adj F)

Full source

/-- The cones defined by `coneOfAdj` are limit cones. -/
@[simps]
def isLimitConeOfAdj (F : J ⥤ C) :
    IsLimit (coneOfAdj adj F) where
  lift s := adj.homEquiv _ _ s.π
  fac s j := by
    have eq := NatTrans.congr_app (adj.counit.naturality s.π) j
    have eq' := NatTrans.congr_app (adj.left_triangle_components s.pt) j
    dsimp at eq eq' ⊢
    rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']
  uniq s m hm := (adj.homEquiv _ _).symm.injective (by ext j; simpa using hm j)

Limit cone via adjunction

Informal description

Given a right adjoint functor $ L \colon C \to D $ to the constant functor $ \Delta \colon D \to C $, the cone $ \text{coneOfAdj} \, F $ constructed via this adjunction is a limit cone for the functor $ F \colon J \to C $. Specifically: - The universal morphism $ \text{lift} $ from any other cone $ s $ to $ \text{coneOfAdj} \, F $ is given by the hom-set bijection of the adjunction applied to $ s.\pi $. - The factorization condition $ \text{fac} $ follows from the naturality of the counit of the adjunction and the adjunction's triangle identity. - The uniqueness condition $ \text{uniq} $ is ensured by the injectivity of the hom-set bijection.

CategoryTheory.Limits.hasLimitsOfShape_of_equivalence theorem

{J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J') [HasLimitsOfShape J C] : HasLimitsOfShape J' C

Full source

/-- We can transport limits of shape `J` along an equivalence `J ≌ J'`.
-/
theorem hasLimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
    [HasLimitsOfShape J C] : HasLimitsOfShape J' C := by
  constructor
  intro F
  apply hasLimitOfEquivalenceComp e

Preservation of Limits of Shape under Equivalence of Categories

Informal description

Let $J$ and $J'$ be categories, and let $e \colon J \simeq J'$ be an equivalence of categories. If a category $\mathcal{C}$ has limits of shape $J$, then $\mathcal{C}$ also has limits of shape $J'$.

CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE theorem

[UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfSize.{v₂, u₂} C

Full source

/-- A category that has larger limits also has smaller limits. -/
theorem hasLimitsOfSizeOfUnivLE [UnivLEUnivLE.{v₂, v₁}] [UnivLEUnivLE.{u₂, u₁}]
    [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfSize.{v₂, u₂} C where
  has_limits_of_shape J {_} := hasLimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Existence of Smaller Limits in Categories with Larger Limits under Universe Constraints

Informal description

Let $\mathcal{C}$ be a category with all limits of size $(v_1, u_1)$. If the universe levels $v_2$ and $u_2$ are respectively less than or equal to $v_1$ and $u_1$ (denoted by $\text{UnivLE}\{v_2, v_1\}$ and $\text{UnivLE}\{u_2, u_1\}$), then $\mathcal{C}$ has all limits of size $(v_2, u_2)$.

CategoryTheory.Limits.hasLimitsOfSizeShrink theorem

[HasLimitsOfSize.{max v₁ v₂, max u₁ u₂} C] : HasLimitsOfSize.{v₁, u₁} C

Full source

/-- `hasLimitsOfSizeShrink.{v u} C` tries to obtain `HasLimitsOfSize.{v u} C`
from some other `HasLimitsOfSize C`.
-/
theorem hasLimitsOfSizeShrink [HasLimitsOfSize.{max v₁ v₂, max u₁ u₂} C] :
    HasLimitsOfSize.{v₁, u₁} C := hasLimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

Existence of Smaller Limits from Larger Limits via Universe Shrinkage

Informal description

If a category $\mathcal{C}$ has all limits of size $(\max(v_1, v_2), \max(u_1, u_2))$, then it also has all limits of size $(v_1, u_1)$.

CategoryTheory.Limits.hasSmallestLimitsOfHasLimits instance

[HasLimits C] : HasLimitsOfSize.{0, 0} C

Full source

instance (priority := 100) hasSmallestLimitsOfHasLimits [HasLimits C] : HasLimitsOfSize.{0, 0} C :=
  hasLimitsOfSizeShrink.{0, 0} C

Existence of Smallest Limits in Categories with All Limits

Informal description

Every category $\mathcal{C}$ that has all (small) limits also has all limits indexed by small categories of the smallest size $(0, 0)$.

CategoryTheory.Limits.ColimitCocone structure

(F : J ⥤ C)

Full source

/-- `ColimitCocone F` contains a cocone over `F` together with the information that it is a
    colimit. -/
structure ColimitCocone (F : J ⥤ C) where
  /-- The cocone itself -/
  cocone : Cocone F
  /-- The proof that it is the colimit cocone -/
  isColimit : IsColimit cocone

Colimit Cocone Structure

Informal description

The structure `ColimitCocone F` consists of a cocone over a functor `F : J ⥤ C` together with the proof that it is a colimit cocone. This means the cocone is universal among all cocones over `F`, satisfying the appropriate universal property for colimits in category theory.

CategoryTheory.Limits.HasColimit structure

(F : J ⥤ C)

Full source

/-- `HasColimit F` represents the mere existence of a colimit for `F`. -/
class HasColimit (F : J ⥤ C) : Prop where mk' ::
  /-- There exists a colimit for `F` -/
  exists_colimit : Nonempty (ColimitCocone F)

Existence of colimit for a functor

Informal description

The structure `HasColimit F` asserts the mere existence of a colimit for the functor `F : J ⥤ C` in a category `C`. This is a propositional typeclass, meaning it only states the existence of some colimit cocone without specifying a particular one, to avoid issues with non-defeq instances.

CategoryTheory.Limits.HasColimit.mk theorem

{F : J ⥤ C} (d : ColimitCocone F) : HasColimit F

Full source

theorem HasColimit.mk {F : J ⥤ C} (d : ColimitCocone F) : HasColimit F :=
  ⟨Nonempty.intro d⟩

Construction of Colimit Existence from Colimit Cocone

Informal description

Given a functor $F : J \to C$ and a colimit cocone $d$ for $F$, the structure `HasColimit F` is constructed, asserting the existence of a colimit for $F$.

CategoryTheory.Limits.getColimitCocone definition

(F : J ⥤ C) [HasColimit F] : ColimitCocone F

Full source

/-- Use the axiom of choice to extract explicit `ColimitCocone F` from `HasColimit F`. -/
def getColimitCocone (F : J ⥤ C) [HasColimit F] : ColimitCocone F :=
  Classical.choice <| HasColimit.exists_colimit

Explicit colimit cocone from existence

Informal description

Given a functor $F : J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), the function `getColimitCocone` produces an explicit colimit cocone for $F$ using the axiom of choice.

CategoryTheory.Limits.HasColimitsOfShape structure

Full source

/-- `C` has colimits of shape `J` if there exists a colimit for every functor `F : J ⥤ C`. -/
class HasColimitsOfShape : Prop where
  /-- All `F : J ⥤ C` have colimits for a fixed `J` -/
  has_colimit : ∀ F : J ⥤ C, HasColimit F := by infer_instance

Existence of colimits of a given shape

Informal description

A category $C$ has colimits of shape $J$ if for every functor $F : J \to C$, there exists a colimit cocone for $F$.

CategoryTheory.Limits.HasColimitsOfSize structure

(C : Type u) [Category.{v} C]

Full source

/-- `C` has all colimits of size `v₁ u₁` (`HasColimitsOfSize.{v₁ u₁} C`)
if it has colimits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
-/
@[pp_with_univ]
class HasColimitsOfSize (C : Type u) [Category.{v} C] : Prop where
  /-- All `F : J ⥤ C` have colimits for all small `J` -/
  has_colimits_of_shape : ∀ (J : Type u₁) [Category.{v₁} J], HasColimitsOfShape J C := by
    infer_instance

Existence of colimits of a given size in a category

Informal description

The structure `HasColimitsOfSize.{v₁ u₁} C` asserts that a category `C` has all colimits of size `(v₁, u₁)`, meaning it has colimits for every diagram shape `J : Type u₁` with a category structure `Category.{v₁} J`.

CategoryTheory.Limits.HasColimits abbrev

(C : Type u) [Category.{v} C] : Prop

Full source

/-- `C` has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.
-/
abbrev HasColimits (C : Type u) [Category.{v} C] : Prop :=
  HasColimitsOfSize.{v, v} C

Existence of all small colimits in a category

Informal description

A category $\mathcal{C}$ has all (small) colimits if for every small category $\mathcal{J}$ and every functor $F : \mathcal{J} \to \mathcal{C}$, there exists a colimit cocone for $F$.

CategoryTheory.Limits.HasColimits.hasColimitsOfShape theorem

{C : Type u} [Category.{v} C] [HasColimits C] (J : Type v) [Category.{v} J] : HasColimitsOfShape J C

Full source

theorem HasColimits.hasColimitsOfShape {C : Type u} [Category.{v} C] [HasColimits C] (J : Type v)
    [Category.{v} J] : HasColimitsOfShape J C :=
  HasColimitsOfSize.has_colimits_of_shape J

Existence of Colimits of Given Shape in Categories with All Colimits

Informal description

If a category $\mathcal{C}$ has all small colimits, then for any small category $\mathcal{J}$, $\mathcal{C}$ has colimits of shape $\mathcal{J}$.

CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instance

{J : Type u₁} [Category.{v₁} J] [HasColimitsOfShape J C] (F : J ⥤ C) : HasColimit F

Full source

instance (priority := 100) hasColimitOfHasColimitsOfShape {J : Type u₁} [Category.{v₁} J]
    [HasColimitsOfShape J C] (F : J ⥤ C) : HasColimit F :=
  HasColimitsOfShape.has_colimit F

Existence of Colimits for Functors in Categories with Colimits of Given Shape

Informal description

For any category $C$ that has colimits of shape $J$, every functor $F : J \to C$ has a colimit.

CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize instance

{J : Type u₁} [Category.{v₁} J] [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfShape J C

Full source

instance (priority := 100) hasColimitsOfShapeOfHasColimitsOfSize {J : Type u₁} [Category.{v₁} J]
    [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfShape J C :=
  HasColimitsOfSize.has_colimits_of_shape J

Existence of Colimits of Given Shape from All Colimits of Given Size

Informal description

For any category $C$ that has all colimits of size $(v₁, u₁)$, and for any small category $J$ of size $(v₁, u₁)$, $C$ has colimits of shape $J$.

CategoryTheory.Limits.colimit.cocone definition

(F : J ⥤ C) [HasColimit F] : Cocone F

Full source

/-- An arbitrary choice of colimit cocone of a functor. -/
def colimit.cocone (F : J ⥤ C) [HasColimit F] : Cocone F :=
  (getColimitCocone F).cocone

Colimit cocone of a functor

Informal description

Given a functor $F : J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), the function `colimit.cocone` produces an explicit cocone over $F$ that serves as a colimit cocone. This is constructed using the axiom of choice from the existence proof `HasColimit F`.

CategoryTheory.Limits.colimit definition

(F : J ⥤ C) [HasColimit F]

Full source

/-- An arbitrary choice of colimit object of a functor. -/
def colimit (F : J ⥤ C) [HasColimit F] :=
  (colimit.cocone F).pt

Colimit object of a functor

Informal description

Given a functor $F : J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), the object `colimit F` is an arbitrary choice of colimit object for $F$. This is constructed as the apex of the colimit cocone provided by `colimit.cocone F`.

CategoryTheory.Limits.colimit.ι definition

(F : J ⥤ C) [HasColimit F] (j : J) : F.obj j ⟶ colimit F

Full source

/-- The coprojection from a value of the functor to the colimit object. -/
def colimit.ι (F : J ⥤ C) [HasColimit F] (j : J) : F.obj j ⟶ colimit F :=
  (colimit.cocone F).ι.app j

Coprojection to colimit

Informal description

For a functor $F : J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), the morphism $\iota_j : F(j) \to \text{colimit } F$ is the coprojection from the object $F(j)$ to the colimit object of $F$, for each object $j$ in the indexing category $J$.

CategoryTheory.Limits.colimit.eqToHom_comp_ι theorem

(F : J ⥤ C) [HasColimit F] {j j' : J} (hj : j = j') : eqToHom (by subst hj; rfl) ≫ colimit.ι F j = colimit.ι F j'

Full source

@[reassoc]
theorem colimit.eqToHom_comp_ι (F : J ⥤ C) [HasColimit F] {j j' : J} (hj : j = j') :
    eqToHomeqToHom (by subst hj; rfl) ≫ colimit.ι F j = colimit.ι F j'  := by
  subst hj
  simp

Compatibility of Coprojections with Object Equality in Colimits

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a colimit. For any objects $j, j' \in J$ with an equality $hj : j = j'$, the composition of the morphism $\text{eqToHom}(hj) \colon F(j) \to F(j')$ with the coprojection $\iota_j \colon F(j) \to \text{colimit } F$ equals the coprojection $\iota_{j'} \colon F(j') \to \text{colimit } F$.

CategoryTheory.Limits.colimit.cocone_ι theorem

{F : J ⥤ C} [HasColimit F] (j : J) : (colimit.cocone F).ι.app j = colimit.ι _ j

Full source

@[simp]
theorem colimit.cocone_ι {F : J ⥤ C} [HasColimit F] (j : J) :
    (colimit.cocone F).ι.app j = colimit.ι _ j :=
  rfl

Components of Colimit Cocone Equal Coprojections

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit (i.e., `[HasColimit F]`), and for any object $j$ in $J$, the $j$-th component of the colimit cocone's natural transformation equals the coprojection morphism $\iota_j \colon F(j) \to \text{colimit } F$.

CategoryTheory.Limits.colimit.cocone_x theorem

{F : J ⥤ C} [HasColimit F] : (colimit.cocone F).pt = colimit F

Full source

@[simp]
theorem colimit.cocone_x {F : J ⥤ C} [HasColimit F] : (colimit.cocone F).pt = colimit F :=
  rfl

Apex of Colimit Cocone Equals Colimit Object

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit (i.e., `[HasColimit F]`), the apex of the colimit cocone `colimit.cocone F` is equal to the chosen colimit object `colimit F`.

CategoryTheory.Limits.colimit.w theorem

(F : J ⥤ C) [HasColimit F] {j j' : J} (f : j ⟶ j') : F.map f ≫ colimit.ι F j' = colimit.ι F j

Full source

@[reassoc (attr := simp)]
theorem colimit.w (F : J ⥤ C) [HasColimit F] {j j' : J} (f : j ⟶ j') :
    F.map f ≫ colimit.ι F j' = colimit.ι F j :=
  (colimit.cocone F).w f

Naturality condition for colimit coprojections

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit (i.e., `[HasColimit F]`), and for any morphism $f \colon j \to j'$ in $J$, the diagram \[ F(j) \xrightarrow{F(f)} F(j') \xrightarrow{\iota_{j'}} \text{colimit } F \] commutes, where $\iota_{j'}$ is the coprojection from $F(j')$ to the colimit. In other words, $F(f) \circ \iota_{j'} = \iota_j$.

CategoryTheory.Limits.colimit.isColimit definition

(F : J ⥤ C) [HasColimit F] : IsColimit (colimit.cocone F)

Full source

/-- Evidence that the arbitrary choice of cocone is a colimit cocone. -/
def colimit.isColimit (F : J ⥤ C) [HasColimit F] : IsColimit (colimit.cocone F) :=
  (getColimitCocone F).isColimit

Universal property of the colimit cocone

Informal description

Given a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), the function `colimit.isColimit` provides evidence that the cocone `colimit.cocone F` is indeed a colimit cocone for $F$. This means it satisfies the universal property of colimits: for any other cocone $c$ over $F$, there exists a unique morphism from `colimit.cocone F` to $c$.

CategoryTheory.Limits.colimit.desc definition

(F : J ⥤ C) [HasColimit F] (c : Cocone F) : colimit F ⟶ c.pt

Full source

/-- The morphism from the colimit object to the cone point of any other cocone. -/
def colimit.desc (F : J ⥤ C) [HasColimit F] (c : Cocone F) : colimitcolimit F ⟶ c.pt :=
  (colimit.isColimit F).desc c

Universal morphism from colimit to a cocone

Informal description

Given a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), and given any cocone $c$ over $F$, the morphism $\text{colimit.desc}\, F\, c \colon \text{colimit}\, F \to c.\text{pt}$ is the unique morphism from the colimit object to the apex of $c$ that makes the resulting diagram commute. This morphism is constructed using the universal property of the colimit cocone.

CategoryTheory.Limits.colimit.isColimit_desc theorem

{F : J ⥤ C} [HasColimit F] (c : Cocone F) : (colimit.isColimit F).desc c = colimit.desc F c

Full source

@[simp]
theorem colimit.isColimit_desc {F : J ⥤ C} [HasColimit F] (c : Cocone F) :
    (colimit.isColimit F).desc c = colimit.desc F c :=
  rfl

Equality of Colimit Descent Morphisms

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit, and for any cocone $c$ over $F$, the description morphism provided by the universal property of the colimit cocone equals the colimit descent morphism, i.e., $(\text{colimit.isColimit}\, F).\text{desc}\, c = \text{colimit.desc}\, F\, c$.

CategoryTheory.Limits.colimit.ι_desc theorem

{F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) : colimit.ι F j ≫ colimit.desc F c = c.ι.app j

Full source

/-- We have lots of lemmas describing how to simplify `colimit.ι F j ≫ _`,
and combined with `colimit.ext` we rely on these lemmas for many calculations.

However, since `Category.assoc` is a `@[simp]` lemma, often expressions are
right associated, and it's hard to apply these lemmas about `colimit.ι`.

We thus use `reassoc` to define additional `@[simp]` lemmas, with an arbitrary extra morphism.
(see `Tactic/reassoc_axiom.lean`)
-/
@[reassoc (attr := simp)]
theorem colimit.ι_desc {F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) :
    colimit.ιcolimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
  IsColimit.fac _ c j

Commutativity of Colimit Coprojection with Descending Morphism

Informal description

For a functor $F \colon J \to C$ in a category $C$ with a colimit, given any cocone $c$ over $F$ and an object $j \in J$, the composition of the coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the universal morphism $\text{colimit.desc}\, F\, c \colon \text{colimit}\, F \to c.\text{pt}$ equals the component $c.\iota_j \colon F(j) \to c.\text{pt}$ of the cocone $c$.

CategoryTheory.Limits.colimMap definition

{F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) : colimit F ⟶ colimit G

Full source

/-- Functoriality of colimits.

Usually this morphism should be accessed through `colim.map`,
but may be needed separately when you have specified colimits for the source and target functors,
but not necessarily for all functors of shape `J`.
-/
def colimMap {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) : colimitcolimit F ⟶ colimit G :=
  IsColimit.map (colimit.isColimit F) _ α

Morphism between colimits induced by a natural transformation

Informal description

Given functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits (i.e., `[HasColimit F]` and `[HasColimit G]`), and given a natural transformation $\alpha \colon F \Rightarrow G$, the function `colimMap` produces a morphism from the colimit object of $F$ to the colimit object of $G$. This morphism is constructed using the universal property of the colimit of $F$ applied to the cocone over $G$ obtained by composing $\alpha$ with the colimit cocone of $G$.

CategoryTheory.Limits.ι_colimMap theorem

 {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) (j : J) : colimit.ι F j ≫ colimMap α = α.app j ≫ colimit.ι G j

Full source

@[reassoc (attr := simp)]
theorem ι_colimMap {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) (j : J) :
    colimit.ιcolimit.ι F j ≫ colimMap α = α.app j ≫ colimit.ι G j :=
  colimit.ι_desc _ j

Commutativity of Coprojections with Induced Colimit Morphism

Informal description

Given functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits, and given a natural transformation $\alpha \colon F \Rightarrow G$, for each object $j \in J$, the composition of the coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the induced morphism $\text{colimMap}\, \alpha \colon \text{colimit}\, F \to \text{colimit}\, G$ equals the composition of the component $\alpha_j \colon F(j) \to G(j)$ with the coprojection $\iota_j \colon G(j) \to \text{colimit}\, G$.

CategoryTheory.Limits.colimit.coconeMorphism definition

{F : J ⥤ C} [HasColimit F] (c : Cocone F) : colimit.cocone F ⟶ c

Full source

/-- The cocone morphism from the arbitrary choice of colimit cocone to any cocone. -/
def colimit.coconeMorphism {F : J ⥤ C} [HasColimit F] (c : Cocone F) : colimit.coconecolimit.cocone F ⟶ c :=
  (colimit.isColimit F).descCoconeMorphism c

Universal cocone morphism from colimit

Informal description

Given a functor $ F \colon J \to C $ in a category $ C $ where the existence of a colimit for $ F $ is asserted (i.e., `[HasColimit F]`), and given any cocone $ c $ over $ F $, the function `colimit.coconeMorphism` produces the unique cocone morphism from the chosen colimit cocone `colimit.cocone F` to $ c $. This morphism is constructed using the universal property of the colimit cocone.

CategoryTheory.Limits.colimit.coconeMorphism_hom theorem

{F : J ⥤ C} [HasColimit F] (c : Cocone F) : (colimit.coconeMorphism c).hom = colimit.desc F c

Full source

@[simp]
theorem colimit.coconeMorphism_hom {F : J ⥤ C} [HasColimit F] (c : Cocone F) :
    (colimit.coconeMorphism c).hom = colimit.desc F c :=
  rfl

Universal cocone morphism equals colimit descent morphism

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit, and for any cocone $c$ over $F$, the homomorphism component of the universal cocone morphism from the colimit cocone to $c$ is equal to the universal morphism $\text{colimit.desc}\, F\, c$ from the colimit object to the apex of $c$.

CategoryTheory.Limits.colimit.ι_coconeMorphism theorem

{F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) : colimit.ι F j ≫ (colimit.coconeMorphism c).hom = c.ι.app j

Full source

theorem colimit.ι_coconeMorphism {F : J ⥤ C} [HasColimit F] (c : Cocone F) (j : J) :
    colimit.ιcolimit.ι F j ≫ (colimit.coconeMorphism c).hom = c.ι.app j := by simp

Commutativity of colimit coprojection with universal cocone morphism

Informal description

For a functor $F \colon J \to C$ in a category $C$ with a colimit, given any cocone $c$ over $F$ and an object $j \in J$, the composition of the colimit coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the universal morphism $\text{colimit.coconeMorphism}\, c \colon \text{colimit}\, F \to c.\text{pt}$ equals the component $c.\iota_j \colon F(j) \to c.\text{pt}$ of the cocone $c$. In symbols: $$ \iota_j \circ (\text{colimit.coconeMorphism}\, c).\text{hom} = c.\iota_j. $$

CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom theorem

 {F : J ⥤ C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) :
  colimit.ι F j ≫ (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) hc).hom = c.ι.app j

Full source

@[reassoc (attr := simp)]
theorem colimit.comp_coconePointUniqueUpToIso_hom {F : J ⥤ C} [HasColimit F] {c : Cocone F}
    (hc : IsColimit c) (j : J) :
    colimit.ιcolimit.ι F j ≫ (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) hc).hom = c.ι.app j :=
  IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _

Compatibility of colimit coprojections with the unique isomorphism between colimit cocones

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`). Given a colimit cocone $c$ for $F$ with the property `hc : IsColimit c`, and an object $j$ in the indexing category $J$, the composition of the coprojection $\iota_j \colon F(j) \to \text{colimit } F$ with the unique isomorphism $\text{colimit } F \cong c.pt$ (induced by the universal property of colimits) equals the cocone morphism $c.\iota_j \colon F(j) \to c.pt$. In symbols: $$ \iota_j \circ (\text{colimit } F \cong c.pt).\text{hom} = c.\iota_j. $$

CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv theorem

 {F : J ⥤ C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) :
  colimit.ι F j ≫ (IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)).inv = c.ι.app j

Full source

@[reassoc (attr := simp)]
theorem colimit.comp_coconePointUniqueUpToIso_inv {F : J ⥤ C} [HasColimit F] {c : Cocone F}
    (hc : IsColimit c) (j : J) :
    colimit.ιcolimit.ι F j ≫ (IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)).inv = c.ι.app j :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Compatibility of colimit coprojections with inverse apex isomorphism

Informal description

For a functor $F \colon J \to C$ in a category $C$ where a colimit exists (i.e., `[HasColimit F]`), given any colimit cocone $c$ of $F$ (with proof $hc$ that it is a colimit), and for any object $j$ in $J$, the composition of the colimit coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the inverse of the unique isomorphism between the apexes of $c$ and the standard colimit cocone equals the cocone morphism $c.\iota_j \colon F(j) \to c.pt$. In symbols: $$ \iota_j \circ (\text{coconePointUniqueUpToIso}\, hc\, (\text{colimit.isColimit}\, F))^{-1} = c.\iota_j. $$

CategoryTheory.Limits.colimit.existsUnique theorem

{F : J ⥤ C} [HasColimit F] (t : Cocone F) : ∃! d : colimit F ⟶ t.pt, ∀ j, colimit.ι F j ≫ d = t.ι.app j

Full source

theorem colimit.existsUnique {F : J ⥤ C} [HasColimit F] (t : Cocone F) :
    ∃! d : colimit F ⟶ t.pt, ∀ j, colimit.ι F j ≫ d = t.ι.app j :=
  (colimit.isColimit F).existsUnique _

Universal Property of Colimits: Unique Factorization Through Colimit Cocone

Informal description

For a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), and for any cocone $t$ over $F$, there exists a unique morphism $d \colon \text{colimit } F \to t.\text{pt}$ such that for every object $j$ in $J$, the composition $\iota_j \circ d$ equals $t.\iota.\text{app}\,j$, where $\iota_j$ is the coprojection from $F(j)$ to the colimit object.

CategoryTheory.Limits.colimit.isoColimitCocone definition

{F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) : colimit F ≅ t.cocone.pt

Full source

/--
Given any other colimit cocone for `F`, the chosen `colimit F` is isomorphic to the cocone point.
-/
def colimit.isoColimitCocone {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) :
    colimitcolimit F ≅ t.cocone.pt :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) t.isColimit

Isomorphism between chosen colimit and any other colimit cocone

Informal description

Given a functor $ F \colon J \to C $ in a category $ C $ where the existence of a colimit for $ F $ is asserted (i.e., `[HasColimit F]`), and given any other colimit cocone $ t $ for $ F $, there exists a canonical isomorphism between the chosen colimit object `colimit F` and the apex of $ t $. This isomorphism is uniquely determined by the universal property of colimits.

CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom theorem

 {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
  colimit.ι F j ≫ (colimit.isoColimitCocone t).hom = t.cocone.ι.app j

Full source

@[reassoc (attr := simp)]
theorem colimit.isoColimitCocone_ι_hom {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
    colimit.ιcolimit.ι F j ≫ (colimit.isoColimitCocone t).hom = t.cocone.ι.app j := by
  dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
  simp

Compatibility of colimit isomorphism with coprojections

Informal description

Given a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted (i.e., `[HasColimit F]`), and given a colimit cocone $t$ for $F$, for each object $j$ in $J$, the composition of the coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the isomorphism $\text{colimit.isoColimitCocone}\, t \colon \text{colimit}\, F \to t.\text{cocone}.\text{pt}$ equals the cocone morphism $t.\text{cocone}.\iota.\text{app}\, j \colon F(j) \to t.\text{cocone}.\text{pt}$.

CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv theorem

 {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
  t.cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j

Full source

@[reassoc (attr := simp)]
theorem colimit.isoColimitCocone_ι_inv {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
    t.cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j := by
  dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
  simp

Compatibility of colimit isomorphism inverse with coprojections

Informal description

Given a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted, and given a colimit cocone $t$ for $F$, for each object $j$ in $J$, the composition of the cocone morphism $t.\text{cocone}.\iota.\text{app} j$ with the inverse of the isomorphism $\text{colimit.isoColimitCocone } t$ equals the coprojection $\text{colimit.ι } F j$.

CategoryTheory.Limits.colimit.hom_ext theorem

 {F : J ⥤ C} [HasColimit F] {X : C} {f f' : colimit F ⟶ X} (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f'

Full source

@[ext]
theorem colimit.hom_ext {F : J ⥤ C} [HasColimit F] {X : C} {f f' : colimitcolimit F ⟶ X}
    (w : ∀ j, colimit.ιcolimit.ι F j ≫ f = colimit.ιcolimit.ι F j ≫ f') : f = f' :=
  (colimit.isColimit F).hom_ext w

Uniqueness of Morphisms from Colimit via Commuting Coprojections

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a colimit. For any object $X$ in $C$ and any pair of morphisms $f, f' \colon \text{colimit}\, F \to X$, if for every object $j$ in $J$ the compositions $\iota_j \circ f$ and $\iota_j \circ f'$ are equal (where $\iota_j \colon F(j) \to \text{colimit}\, F$ is the coprojection), then $f = f'$.

CategoryTheory.Limits.colimit.desc_cocone theorem

{F : J ⥤ C} [HasColimit F] : colimit.desc F (colimit.cocone F) = 𝟙 (colimit F)

Full source

@[simp]
theorem colimit.desc_cocone {F : J ⥤ C} [HasColimit F] :
    colimit.desc F (colimit.cocone F) = 𝟙 (colimit F) :=
  (colimit.isColimit _).desc_self

Identity as the Universal Morphism from Colimit to Itself

Informal description

For any functor $F \colon J \to C$ in a category $C$ that has a colimit, the universal morphism $\text{colimit.desc}\, F\, (\text{colimit.cocone}\, F)$ from the colimit object to itself is equal to the identity morphism on $\text{colimit}\, F$.

CategoryTheory.Limits.colimit.homIso definition

(F : J ⥤ C) [HasColimit F] (W : C) : ULift.{u₁} (colimit F ⟶ W : Type v) ≅ F.cocones.obj W

Full source

/-- The isomorphism (in `Type`) between
morphisms from the colimit object to a specified object `W`,
and cocones with cone point `W`.
-/
def colimit.homIso (F : J ⥤ C) [HasColimit F] (W : C) :
    ULiftULift.{u₁} (colimit F ⟶ W : Type v) ≅ F.cocones.obj W :=
  (colimit.isColimit F).homIso W

Isomorphism between morphisms from colimit and cocones with fixed apex

Informal description

Given a functor $ F \colon J \to C $ in a category $ C $ where the existence of a colimit for $ F $ is asserted (i.e., `[HasColimit F]`), and an object $ W $ in $ C $, the isomorphism `colimit.homIso F W` establishes a natural isomorphism between the lifted hom-set $ \text{ULift}(\text{colimit}\, F \to W) $ and the set of cocones over $ F $ with apex $ W $. This isomorphism is constructed from the universal property of the colimit cocone.

CategoryTheory.Limits.colimit.homIso_hom theorem

 (F : J ⥤ C) [HasColimit F] {W : C} (f : ULift (colimit F ⟶ W)) :
  (colimit.homIso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f.down

Full source

@[simp]
theorem colimit.homIso_hom (F : J ⥤ C) [HasColimit F] {W : C} (f : ULift (colimitcolimit F ⟶ W)) :
    (colimit.homIso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f.down :=
  (colimit.isColimit F).homIso_hom f

Isomorphism between morphisms from colimit and cocone morphisms composed with constant functor

Informal description

Given a functor $F \colon J \to C$ in a category $C$ where the existence of a colimit for $F$ is asserted, and an object $W$ in $C$, for any morphism $f \colon \mathrm{colimit}\, F \to W$ (lifted via $\mathrm{ULift}$), the application of the isomorphism $\mathrm{colimit.homIso}\, F\, W$ to $f$ yields the natural transformation obtained by composing the cocone morphisms $(colimit.cocone\, F).\iota$ with the constant functor applied to the unlifted morphism $f.down$.

CategoryTheory.Limits.colimit.homIso' definition

 (F : J ⥤ C) [HasColimit F] (W : C) :
  ULift.{u₁} (colimit F ⟶ W : Type v) ≅ { p : ∀ j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j }

Full source

/-- The isomorphism (in `Type`) between
morphisms from the colimit object to a specified object `W`,
and an explicit componentwise description of cocones with cone point `W`.
-/
def colimit.homIso' (F : J ⥤ C) [HasColimit F] (W : C) :
    ULiftULift.{u₁} (colimit F ⟶ W : Type v) ≅
      { p : ∀ j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
  (colimit.isColimit F).homIso' W

Isomorphism between morphisms from colimit and commuting families of morphisms

Informal description

Given a functor $ F \colon J \to C $ in a category $ C $ where the existence of a colimit for $ F $ is asserted (i.e., `[HasColimit F]`), and an object $ W $ in $ C $, there is an isomorphism between the lifted hom-set $\text{ULift}(\text{colimit}\, F \to W)$ and the set of all families of morphisms $ (p_j \colon F.obj\, j \to W)_{j \in J} $ that satisfy the commutativity condition $ F.map\, f \circ p_{j'} = p_j $ for every morphism $ f \colon j \to j' $ in $ J $.

CategoryTheory.Limits.colimit.desc_extend theorem

 (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) : colimit.desc F (c.extend f) = colimit.desc F c ≫ f

Full source

theorem colimit.desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) :
    colimit.desc F (c.extend f) = colimit.desccolimit.desc F c ≫ f := by ext1; rw [← Category.assoc]; simp

Universal Property of Colimit Applied to Extended Cocone

Informal description

Let $F \colon J \to C$ be a functor in a category $C$ that has a colimit. Given a cocone $c$ over $F$ and a morphism $f \colon c.\mathrm{pt} \to X$ in $C$, the universal morphism from the colimit to the extended cocone $c.\mathrm{extend}\, f$ equals the composition of the universal morphism from the colimit to $c$ with $f$. That is, the following diagram commutes: \[ \mathrm{colimit.desc}\, F\, (c.\mathrm{extend}\, f) = \mathrm{colimit.desc}\, F\, c \circ f \]

CategoryTheory.Limits.hasColimit_of_iso theorem

{F G : J ⥤ C} [HasColimit F] (α : G ≅ F) : HasColimit G

Full source

/-- If `F` has a colimit, so does any naturally isomorphic functor.
-/
theorem hasColimit_of_iso {F G : J ⥤ C} [HasColimit F] (α : G ≅ F) : HasColimit G :=
  HasColimit.mk
    { cocone := (Cocones.precompose α.hom).obj (colimit.cocone F)
      isColimit := (IsColimit.precomposeHomEquiv _ _).symm (colimit.isColimit F) }

Existence of colimits for naturally isomorphic functors

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$, if $F$ has a colimit, then $G$ also has a colimit.

CategoryTheory.Limits.hasColimit_iff_of_iso theorem

{F G : J ⥤ C} (α : F ≅ G) : HasColimit F ↔ HasColimit G

Full source

theorem hasColimit_iff_of_iso {F G : J ⥤ C} (α : F ≅ G) : HasColimitHasColimit F ↔ HasColimit G :=
  ⟨fun _ ↦ hasColimit_of_iso α.symm, fun _ ↦ hasColimit_of_iso α⟩

Equivalence of Colimit Existence for Naturally Isomorphic Functors

Informal description

For any two naturally isomorphic functors $F, G \colon J \to C$ in a category $\mathcal{C}$, the existence of a colimit for $F$ is equivalent to the existence of a colimit for $G$.

CategoryTheory.Limits.HasColimit.ofCoconesIso theorem

 {K : Type u₁} [Category.{v₂} K] (F : J ⥤ C) (G : K ⥤ C) (h : F.cocones ≅ G.cocones) [HasColimit F] : HasColimit G

Full source

/-- If a functor `G` has the same collection of cocones as a functor `F`
which has a colimit, then `G` also has a colimit. -/
theorem HasColimit.ofCoconesIso {K : Type u₁} [Category.{v₂} K] (F : J ⥤ C) (G : K ⥤ C)
    (h : F.cocones ≅ G.cocones) [HasColimit F] : HasColimit G :=
  HasColimit.mk ⟨_, IsColimit.ofNatIso (IsColimit.natIso (colimit.isColimit F) ≪≫ h)⟩

Existence of colimit via isomorphism of cocone functors

Informal description

Let $F \colon J \to C$ and $G \colon K \to C$ be functors between categories, and suppose there exists a natural isomorphism $h \colon F.\mathrm{cocones} \cong G.\mathrm{cocones}$ between their respective cocone functors. If $F$ has a colimit, then $G$ also has a colimit.

CategoryTheory.Limits.HasColimit.isoOfNatIso definition

{F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) : colimit F ≅ colimit G

Full source

/-- The colimits of `F : J ⥤ C` and `G : J ⥤ C` are isomorphic,
if the functors are naturally isomorphic.
-/
def HasColimit.isoOfNatIso {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) :
    colimitcolimit F ≅ colimit G :=
  IsColimit.coconePointsIsoOfNatIso (colimit.isColimit F) (colimit.isColimit G) w

Isomorphism of colimits induced by a natural isomorphism of functors

Informal description

Given two naturally isomorphic functors $ F, G \colon J \to C $ in a category $ C $, where both $ F $ and $ G $ have colimits, the colimit objects $ \text{colimit } F $ and $ \text{colimit } G $ are isomorphic. The isomorphism is induced by the natural isomorphism $ w \colon F \cong G $ and the universal properties of the colimits.

CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom theorem

 {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) :
  colimit.ι F j ≫ (HasColimit.isoOfNatIso w).hom = w.hom.app j ≫ colimit.ι G j

Full source

@[reassoc (attr := simp)]
theorem HasColimit.isoOfNatIso_ι_hom {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G)
    (j : J) : colimit.ιcolimit.ι F j ≫ (HasColimit.isoOfNatIso w).hom = w.hom.app j ≫ colimit.ι G j :=
  IsColimit.comp_coconePointsIsoOfNatIso_hom _ _ _ _

Naturality of colimit isomorphism with respect to coprojections

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$, where both $F$ and $G$ have colimits, and a natural isomorphism $w \colon F \cong G$, for any object $j \in J$, the diagram \[ \iota_j^F \circ \varphi = w_j \circ \iota_j^G \] commutes, where $\iota_j^F \colon F(j) \to \text{colimit } F$ and $\iota_j^G \colon G(j) \to \text{colimit } G$ are the coprojection morphisms, and $\varphi \colon \text{colimit } F \to \text{colimit } G$ is the isomorphism induced by $w$.

CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv theorem

 {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) :
  colimit.ι G j ≫ (HasColimit.isoOfNatIso w).inv = w.inv.app j ≫ colimit.ι F j

Full source

@[reassoc (attr := simp)]
theorem HasColimit.isoOfNatIso_ι_inv {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G)
    (j : J) : colimit.ιcolimit.ι G j ≫ (HasColimit.isoOfNatIso w).inv = w.inv.app j ≫ colimit.ι F j :=
  IsColimit.comp_coconePointsIsoOfNatIso_inv _ _ _ _

Naturality condition for inverse isomorphism between colimit coprojections

Informal description

For any two functors $F, G \colon J \to C$ in a category $C$ that have colimits, and any natural isomorphism $w \colon F \cong G$, the diagram \[ \iota_j^G \circ \varphi^{-1} = w_j^{-1} \circ \iota_j^F \] commutes for every object $j \in J$, where $\iota_j^F \colon F(j) \to \text{colimit } F$ and $\iota_j^G \colon G(j) \to \text{colimit } G$ are the colimit coprojections, and $\varphi \colon \text{colimit } F \cong \text{colimit } G$ is the isomorphism induced by $w$.

CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc theorem

 {F G : J ⥤ C} [HasColimit F] [HasColimit G] (t : Cocone G) (w : F ≅ G) :
  (HasColimit.isoOfNatIso w).hom ≫ colimit.desc G t = colimit.desc F ((Cocones.precompose w.hom).obj _)

Full source

@[reassoc (attr := simp)]
theorem HasColimit.isoOfNatIso_hom_desc {F G : J ⥤ C} [HasColimit F] [HasColimit G] (t : Cocone G)
    (w : F ≅ G) :
    (HasColimit.isoOfNatIso w).hom ≫ colimit.desc G t =
      colimit.desc F ((Cocones.precompose w.hom).obj _) :=
  IsColimit.coconePointsIsoOfNatIso_hom_desc _ _ _

Compatibility of colimit isomorphism with descending morphisms via natural isomorphism

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$, where both $F$ and $G$ have colimits, a cocone $t$ over $G$, and a natural isomorphism $w \colon F \cong G$, the composition of the isomorphism $\text{HasColimit.isoOfNatIso}\, w \colon \text{colimit}\, F \to \text{colimit}\, G$ with the universal morphism $\text{colimit.desc}\, G\, t \colon \text{colimit}\, G \to t.\text{pt}$ equals the universal morphism $\text{colimit.desc}\, F\, ((\text{Cocones.precompose}\, w.\text{hom}).\text{obj}\, t) \colon \text{colimit}\, F \to t.\text{pt}$.

CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc theorem

 {F G : J ⥤ C} [HasColimit F] [HasColimit G] (t : Cocone F) (w : F ≅ G) :
  (HasColimit.isoOfNatIso w).inv ≫ colimit.desc F t = colimit.desc G ((Cocones.precompose w.inv).obj _)

Full source

@[reassoc (attr := simp)]
theorem HasColimit.isoOfNatIso_inv_desc {F G : J ⥤ C} [HasColimit F] [HasColimit G] (t : Cocone F)
    (w : F ≅ G) :
    (HasColimit.isoOfNatIso w).inv ≫ colimit.desc F t =
      colimit.desc G ((Cocones.precompose w.inv).obj _) :=
  IsColimit.coconePointsIsoOfNatIso_inv_desc _ _ _

Compatibility of colimit descent with inverse isomorphism induced by natural isomorphism

Informal description

Given two naturally isomorphic functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits, for any cocone $t$ over $F$, the composition of the inverse isomorphism $(HasColimit.isoOfNatIso\, w)^{-1} \colon \text{colimit}\, G \to \text{colimit}\, F$ with the universal morphism $\text{colimit.desc}\, F\, t$ equals the universal morphism $\text{colimit.desc}\, G\, ((\text{Cocones.precompose}\, w^{-1})\, t)$.

CategoryTheory.Limits.HasColimit.isoOfEquivalence definition

 {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) : colimit F ≅ colimit G

Full source

/-- The colimits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
if there is an equivalence `e : J ≌ K` making the triangle commute up to natural isomorphism.
-/
def HasColimit.isoOfEquivalence {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K)
    (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) : colimitcolimit F ≅ colimit G :=
  IsColimit.coconePointsIsoOfEquivalence (colimit.isColimit F) (colimit.isColimit G) e w

Isomorphism of colimits under equivalence of indexing categories

Informal description

Given two functors $F \colon J \to C$ and $G \colon K \to C$ in a category $C$, where both $F$ and $G$ have colimits, an equivalence of categories $e \colon J \simeq K$, and a natural isomorphism $w \colon e.\text{functor} \circ G \cong F$, the colimit objects $\text{colimit}\, F$ and $\text{colimit}\, G$ are isomorphic in $C$.

CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π theorem

 {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) :
  colimit.ι F j ≫ (HasColimit.isoOfEquivalence e w).hom = F.map (e.unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _

Full source

@[simp]
theorem HasColimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
    (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) (j : J) :
    colimit.ιcolimit.ι F j ≫ (HasColimit.isoOfEquivalence e w).hom =
      F.map (e.unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _ := by
  simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]

Commutativity of colimit coprojection with equivalence-induced isomorphism

Informal description

Let $F \colon J \to C$ and $G \colon K \to C$ be functors in a category $C$ that have colimits, and let $e \colon J \simeq K$ be an equivalence of categories with a natural isomorphism $w \colon e.\text{functor} \circ G \cong F$. For any object $j \in J$, the composition of the coprojection $\iota_j \colon F(j) \to \text{colimit}\, F$ with the isomorphism $\text{HasColimit.isoOfEquivalence}\, e\, w \colon \text{colimit}\, F \to \text{colimit}\, G$ equals the composition: \[ F(e.\text{unit}_j) \circ w^{-1}_{e(j)} \circ \iota_{e(j)} \] where: - $e.\text{unit}_j \colon j \to e^{-1}(e(j))$ is the unit of the equivalence at $j$, - $w^{-1}_{e(j)} \colon F(j) \to G(e(j))$ is the component of the inverse natural isomorphism at $e(j)$, - $\iota_{e(j)} \colon G(e(j)) \to \text{colimit}\, G$ is the coprojection from $G(e(j))$.

CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π theorem

 {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) :
  colimit.ι G k ≫ (HasColimit.isoOfEquivalence e w).inv =
    G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)

Full source

@[simp]
theorem HasColimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
    (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) (k : K) :
    colimit.ιcolimit.ι G k ≫ (HasColimit.isoOfEquivalence e w).inv =
      G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k) := by
  simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]

Compatibility of Inverse Isomorphism with Coprojections under Equivalence of Indexing Categories

Informal description

Let $F \colon J \to C$ and $G \colon K \to C$ be functors in a category $C$ with colimits, $e \colon J \simeq K$ an equivalence of categories, and $w \colon e.\text{functor} \circ G \cong F$ a natural isomorphism. Then for any object $k \in K$, the composition of the coprojection $\iota_k \colon G(k) \to \text{colimit}\, G$ with the inverse of the isomorphism $\text{HasColimit.isoOfEquivalence}\, e\, w \colon \text{colimit}\, F \cong \text{colimit}\, G$ equals the composition: $$G(\epsilon^{-1}_k) \circ w_{\text{inv}(k)} \circ \iota_{\text{inv}(k)}$$ where: - $\epsilon^{-1}_k \colon k \to e(\text{inv}(k))$ is the inverse counit of $e$ at $k$, - $w_{\text{inv}(k)} \colon F(\text{inv}(k)) \to G(e(\text{inv}(k)))$ is the component of $w$ at $\text{inv}(k)$, - $\iota_{\text{inv}(k)} \colon F(\text{inv}(k)) \to \text{colimit}\, F$ is the coprojection.

CategoryTheory.Limits.colimit.pre definition

: colimit (E ⋙ F) ⟶ colimit F

Full source

/-- The canonical morphism from the colimit of `E ⋙ F` to the colimit of `F`.
-/
def colimit.pre : colimitcolimit (E ⋙ F) ⟶ colimit F :=
  colimit.desc (E ⋙ F) ((colimit.cocone F).whisker E)

Canonical morphism from colimit of composition to colimit

Informal description

Given functors $E \colon K \to J$ and $F \colon J \to C$ in a category $C$ where colimits exist for both $F$ and the composition $E \circ F$, the morphism $\text{colimit.pre}\, F\, E \colon \text{colimit}\, (E \circ F) \to \text{colimit}\, F$ is the canonical morphism from the colimit of the composition $E \circ F$ to the colimit of $F$. This is constructed by applying the universal property of the colimit of $E \circ F$ to the whiskered colimit cocone of $F$ along $E$.

CategoryTheory.Limits.colimit.ι_pre theorem

(k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k)

Full source

@[reassoc (attr := simp)]
theorem colimit.ι_pre (k : K) : colimit.ιcolimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) := by
  erw [IsColimit.fac]
  rfl

Compatibility of coprojections with precomposition: $\iota_k \circ \text{pre} = \iota_{E(k)}$

Informal description

For any object $k$ in the category $K$, the composition of the coprojection $\iota_k \colon (E \circ F)(k) \to \text{colimit}\, (E \circ F)$ with the canonical morphism $\text{colimit.pre}\, F\, E \colon \text{colimit}\, (E \circ F) \to \text{colimit}\, F$ equals the coprojection $\iota_{E(k)} \colon F(E(k)) \to \text{colimit}\, F$.

CategoryTheory.Limits.colimit.ι_inv_pre theorem

[IsIso (pre F E)] (k : K) : colimit.ι F (E.obj k) ≫ inv (colimit.pre F E) = colimit.ι (E ⋙ F) k

Full source

@[reassoc (attr := simp)]
theorem colimit.ι_inv_pre [IsIso (pre F E)] (k : K) :
    colimit.ιcolimit.ι F (E.obj k) ≫ inv (colimit.pre F E) = colimit.ι (E ⋙ F) k := by
  simp [IsIso.comp_inv_eq]

Inverse of Precomposition Colimit Morphism Interacts with Coprojections: $\iota_{E(k)} \circ (\text{pre}\, F\, E)^{-1} = \iota_k$

Informal description

Let $F \colon J \to C$ be a functor and $E \colon K \to J$ be another functor between categories, where $C$ has colimits for both $F$ and $E \circ F$. If the canonical morphism $\text{colimit.pre}\, F\, E \colon \text{colimit}\, (E \circ F) \to \text{colimit}\, F$ is an isomorphism, then for any object $k$ in $K$, the composition of the coprojection $\iota_{E(k)} \colon F(E(k)) \to \text{colimit}\, F$ with the inverse of $\text{colimit.pre}\, F\, E$ equals the coprojection $\iota_k \colon (E \circ F)(k) \to \text{colimit}\, (E \circ F)$.

CategoryTheory.Limits.colimit.pre_desc theorem

(c : Cocone F) : colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E)

Full source

@[reassoc (attr := simp)]
theorem colimit.pre_desc (c : Cocone F) :
    colimit.precolimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) := by
  ext; rw [← assoc, colimit.ι_pre]; simp

Compatibility of Precomposition and Descending Morphisms for Colimits

Informal description

Given a functor $F \colon J \to C$ in a category $C$ with colimits, a cocone $c$ over $F$, and a functor $E \colon K \to J$, the composition of the canonical morphism $\text{colimit.pre}\, F\, E \colon \text{colimit}\, (E \circ F) \to \text{colimit}\, F$ with the universal morphism $\text{colimit.desc}\, F\, c \colon \text{colimit}\, F \to c.\text{pt}$ equals the universal morphism $\text{colimit.desc}\, (E \circ F)\, (c.\text{whisker}\, E) \colon \text{colimit}\, (E \circ F) \to c.\text{pt}$.

CategoryTheory.Limits.colimit.pre_pre theorem

 [h : HasColimit (D ⋙ E ⋙ F)] :
  haveI : HasColimit ((D ⋙ E) ⋙ F) := h
  colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E)

Full source

@[simp]
theorem colimit.pre_pre [h : HasColimit (D ⋙ E ⋙ F)] :
    haveI : HasColimit ((D ⋙ E) ⋙ F) := h
    colimit.precolimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) := by
  ext j
  rw [← assoc, colimit.ι_pre, colimit.ι_pre]
  haveI : HasColimit ((D ⋙ E) ⋙ F) := h
  exact (colimit.ι_pre F (D ⋙ E) j).symm

Composition of Precomposition Morphisms for Colimits: $\text{pre}_{E \circ F, D} \circ \text{pre}_{F, E} = \text{pre}_{F, D \circ E}$

Informal description

Let $D \colon K \to J$, $E \colon J \to L$, and $F \colon L \to C$ be functors in a category $C$ where the colimit of the composition $D \circ E \circ F$ exists. Then the composition of the canonical morphisms \[ \text{colimit.pre}\, (E \circ F)\, D \circ \text{colimit.pre}\, F\, E \] equals the canonical morphism $\text{colimit.pre}\, F\, (D \circ E)$.

CategoryTheory.Limits.colimit.pre_eq theorem

 (s : ColimitCocone (E ⋙ F)) (t : ColimitCocone F) :
  colimit.pre F E =
    (colimit.isoColimitCocone s).hom ≫ s.isColimit.desc (t.cocone.whisker E) ≫ (colimit.isoColimitCocone t).inv

Full source

/-- -
If we have particular colimit cocones available for `E ⋙ F` and for `F`,
we obtain a formula for `colimit.pre F E`.
-/
theorem colimit.pre_eq (s : ColimitCocone (E ⋙ F)) (t : ColimitCocone F) :
    colimit.pre F E =
      (colimit.isoColimitCocone s).hom ≫
        s.isColimit.desc (t.cocone.whisker E) ≫ (colimit.isoColimitCocone t).inv := by
  aesop_cat

Decomposition of $\text{colimit.pre}\, F\, E$ via colimit cocones

Informal description

Given colimit cocones $s$ for the composition $E \circ F$ and $t$ for $F$, the canonical morphism $\text{colimit.pre}\, F\, E$ from the colimit of $E \circ F$ to the colimit of $F$ is equal to the composition of: 1. The isomorphism $\text{colimit.isoColimitCocone}\, s$ from the colimit of $E \circ F$ to the apex of $s$, 2. The universal morphism $s.\text{isColimit}.\text{desc}\, (t.\text{cocone}.\text{whisker}\, E)$ from the apex of $s$ to the apex of the whiskered cocone $t.\text{cocone}.\text{whisker}\, E$, and 3. The inverse of the isomorphism $\text{colimit.isoColimitCocone}\, t$ from the apex of $t$ to the colimit of $F$.

CategoryTheory.Limits.colimit.post definition

: colimit (F ⋙ G) ⟶ G.obj (colimit F)

Full source

/-- The canonical morphism from `G` applied to the colimit of `F ⋙ G`
to `G` applied to the colimit of `F`.
-/
def colimit.post : colimitcolimit (F ⋙ G) ⟶ G.obj (colimit F) :=
  colimit.desc (F ⋙ G) (G.mapCocone (colimit.cocone F))

Canonical morphism from colimit of composition to functor applied to colimit

Informal description

Given functors $F \colon J \to C$ and $G \colon C \to D$, the morphism $\text{colimit.post}\, F\, G \colon \text{colimit}\, (F \circ G) \to G(\text{colimit}\, F)$ is the canonical morphism from the colimit of the composition $F \circ G$ to $G$ applied to the colimit of $F$. This morphism is constructed using the universal property of the colimit of $F \circ G$ applied to the image under $G$ of the colimit cocone of $F$.

CategoryTheory.Limits.colimit.ι_post theorem

(j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j)

Full source

@[reassoc (attr := simp)]
theorem colimit.ι_post (j : J) :
    colimit.ιcolimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) := by
  erw [IsColimit.fac]
  rfl

Commutativity of coprojection with postcomposition morphism

Informal description

For any object $j$ in the indexing category $J$, the composition of the coprojection $\iota_j$ from $F \circ G(j)$ to the colimit of $F \circ G$ with the canonical morphism $\text{colimit.post}\, F\, G$ is equal to the image under $G$ of the coprojection $\iota_j$ from $F(j)$ to the colimit of $F$. In other words, the following diagram commutes: \[ \iota_j^{F \circ G} \circ \text{colimit.post}\, F\, G = G(\iota_j^F) \]

CategoryTheory.Limits.colimit.post_desc theorem

(c : Cocone F) : colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c)

Full source

@[simp]
theorem colimit.post_desc (c : Cocone F) :
    colimit.postcolimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c) := by
  ext
  rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
  rfl

Commutativity of Postcomposition with Descending Morphism from Colimit

Informal description

Given functors $F \colon J \to C$ and $G \colon C \to D$, and a cocone $c$ over $F$, the composition of the canonical morphism $\text{colimit.post}\, F\, G \colon \text{colimit}\, (F \circ G) \to G(\text{colimit}\, F)$ with $G$ applied to the universal morphism $\text{colimit.desc}\, F\, c \colon \text{colimit}\, F \to c.\text{pt}$ equals the universal morphism $\text{colimit.desc}\, (F \circ G)\, (G.\text{mapCocone}\, c) \colon \text{colimit}\, (F \circ G) \to G(c.\text{pt})$. In other words, the following diagram commutes: \[ \text{colimit.post}\, F\, G \circ G(\text{colimit.desc}\, F\, c) = \text{colimit.desc}\, (F \circ G)\, (G.\text{mapCocone}\, c) \]

CategoryTheory.Limits.colimit.post_post theorem

 {E : Type u''} [Category.{v''} E]
  (H : D ⥤ E)
    -- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals
        -- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H))
  [h : HasColimit ((F ⋙ G) ⋙ H)] :
  haveI : HasColimit (F ⋙ G ⋙ H) := h
  colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H)

Full source

@[simp]
theorem colimit.post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E)
    -- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals
    -- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H))
    [h : HasColimit ((F ⋙ G) ⋙ H)] : haveI : HasColimit (F ⋙ G ⋙ H) := h
    colimit.postcolimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H) := by
  ext j
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
  haveI : HasColimit (F ⋙ G ⋙ H) := h
  exact (colimit.ι_post F (G ⋙ H) j).symm

Commutativity of Postcomposition Morphisms for Colimits

Informal description

Let $C$, $D$, and $E$ be categories, and let $F \colon J \to C$, $G \colon C \to D$, and $H \colon D \to E$ be functors. Assume that the colimit of $(F \circ G) \circ H$ exists. Then the composition of the canonical morphism $\text{colimit.post}\, (F \circ G)\, H$ with $H$ applied to the canonical morphism $\text{colimit.post}\, F\, G$ is equal to the canonical morphism $\text{colimit.post}\, F\, (G \circ H)$. In other words, the following diagram commutes: \[ \text{colimit.post}\, (F \circ G)\, H \circ H(\text{colimit.post}\, F\, G) = \text{colimit.post}\, F\, (G \circ H) \]

CategoryTheory.Limits.colimit.pre_post theorem

 {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D) [HasColimit F] [HasColimit (E ⋙ F)]
  [HasColimit (F ⋙ G)] [h : HasColimit ((E ⋙ F) ⋙ G)] :
  -- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs
      -- G (colimit F) ⟶ colimit F ⋙ G ⟶ colimit (E ⋙ (F ⋙ G)) orhaveI : HasColimit (E ⋙ F ⋙ G) := h
  colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G

Full source

theorem colimit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
    [HasColimit F] [HasColimit (E ⋙ F)] [HasColimit (F ⋙ G)] [h : HasColimit ((E ⋙ F) ⋙ G)] :
    -- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs
    -- G (colimit F) ⟶ colimit F ⋙ G ⟶ colimit (E ⋙ (F ⋙ G)) or
    haveI : HasColimit (E ⋙ F ⋙ G) := h
    colimit.postcolimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) =
      colimit.precolimit.pre (F ⋙ G) E ≫ colimit.post F G := by
  ext j
  rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
  haveI : HasColimit (E ⋙ F ⋙ G) := h
  erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]

Commutation of Pre- and Post-composition Morphisms for Colimits

Informal description

Let $C$, $D$ be categories, $E \colon K \to J$ and $F \colon J \to C$ be functors, and $G \colon C \to D$ be another functor. Assume that: 1. $F$ has a colimit in $C$, 2. The composition $E \circ F$ has a colimit in $C$, 3. The composition $F \circ G$ has a colimit in $D$, 4. The composition $(E \circ F) \circ G$ has a colimit in $D$. Then the following diagram commutes: \[ \text{colimit.post}\, (E \circ F)\, G \circ G(\text{colimit.pre}\, F\, E) = \text{colimit.pre}\, (F \circ G)\, E \circ \text{colimit.post}\, F\, G \] where: - $\text{colimit.post}\, (E \circ F)\, G \colon \text{colimit}\, ((E \circ F) \circ G) \to G(\text{colimit}\, (E \circ F))$ is the canonical postcomposition morphism, - $\text{colimit.pre}\, F\, E \colon \text{colimit}\, (E \circ F) \to \text{colimit}\, F$ is the canonical precomposition morphism, - $\text{colimit.pre}\, (F \circ G)\, E \colon \text{colimit}\, (E \circ (F \circ G)) \to \text{colimit}\, (F \circ G)$ is the precomposition morphism for the composed functors, - $\text{colimit.post}\, F\, G \colon \text{colimit}\, (F \circ G) \to G(\text{colimit}\, F)$ is the postcomposition morphism for $F$ and $G$.

CategoryTheory.Limits.hasColimit_equivalence_comp instance

(e : K ≌ J) [HasColimit F] : HasColimit (e.functor ⋙ F)

Full source

instance hasColimit_equivalence_comp (e : K ≌ J) [HasColimit F] : HasColimit (e.functor ⋙ F) :=
  HasColimit.mk
    { cocone := Cocone.whisker e.functor (colimit.cocone F)
      isColimit := IsColimit.whiskerEquivalence (colimit.isColimit F) e }

Preservation of Colimits under Equivalence of Categories

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a functor $F \colon J \to C$ that has a colimit in $C$, the composition $e \circ F \colon K \to C$ also has a colimit in $C$.

CategoryTheory.Limits.hasColimit_of_equivalence_comp theorem

(e : K ≌ J) [HasColimit (e.functor ⋙ F)] : HasColimit F

Full source

/-- If a `E ⋙ F` has a colimit, and `E` is an equivalence, we can construct a colimit of `F`.
-/
theorem hasColimit_of_equivalence_comp (e : K ≌ J) [HasColimit (e.functor ⋙ F)] : HasColimit F := by
  haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm
  apply hasColimit_of_iso (e.invFunIdAssoc F).symm

Existence of Colimit for Functor Composed with Equivalence Inverse

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a functor $F \colon J \to C$, if the composition $e \circ F \colon K \to C$ has a colimit in $C$, then $F$ itself also has a colimit in $C$.

CategoryTheory.Limits.colim definition

: (J ⥤ C) ⥤ C

Full source

/-- `colimit F` is functorial in `F`, when `C` has all colimits of shape `J`. -/
@[simps]
def colim : (J ⥤ C) ⥤ C where
  obj F := colimit F
  map α := colimMap α

Colimit functor

Informal description

The functor that sends each functor $F \colon J \to C$ to its colimit object $\text{colimit}\, F$ in the category $C$, where $C$ has all colimits of shape $J$. For any natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon J \to C$, the functor maps $\alpha$ to the induced morphism $\text{colimMap}\, \alpha$ between the colimit objects of $F$ and $G$.

CategoryTheory.Limits.colimMap_eq theorem

: colimMap α = colim.map α

Full source

theorem colimMap_eq : colimMap α = colim.map α := rfl

Equality of Colimit Morphisms Induced by Natural Transformation

Informal description

Given functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits, and given a natural transformation $\alpha \colon F \Rightarrow G$, the morphism `colimMap α` from the colimit of $F$ to the colimit of $G$ is equal to the morphism `colim.map α` induced by the colimit functor.

CategoryTheory.Limits.colimit.ι_map theorem

(j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j

Full source

@[reassoc]
theorem colimit.ι_map (j : J) : colimit.ιcolimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j := by simp

Commutativity of Coprojections with Colimit Morphism

Informal description

For any functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits, and for any natural transformation $\alpha \colon F \Rightarrow G$, the diagram \[ F(j) \xrightarrow{\iota_j} \text{colimit}\, F \] \[ \downarrow{\alpha_j} \quad \downarrow{\text{colim.map}\, \alpha} \] \[ G(j) \xrightarrow{\iota_j} \text{colimit}\, G \] commutes for every object $j \in J$. Here $\iota_j$ denotes the coprojection morphism from $F(j)$ (resp. $G(j)$) to the colimit of $F$ (resp. $G$), and $\alpha_j$ is the component of $\alpha$ at $j$.

CategoryTheory.Limits.colimit.map_desc theorem

(c : Cocone G) : colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c)

Full source

@[reassoc (attr := simp)]
theorem colimit.map_desc (c : Cocone G) :
    colimMapcolimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c) := by
  ext j
  simp [← assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]

Commutativity of Colimit Morphism with Descending Morphism via Precomposition

Informal description

Given functors $F, G \colon J \to C$ in a category $C$ where both $F$ and $G$ have colimits, a natural transformation $\alpha \colon F \Rightarrow G$, and a cocone $c$ over $G$, the composition of the induced morphism $\text{colimMap}\, \alpha \colon \text{colimit}\, F \to \text{colimit}\, G$ with the universal morphism $\text{colimit.desc}\, G\, c \colon \text{colimit}\, G \to c.\text{pt}$ equals the universal morphism from the colimit of $F$ to the cocone obtained by precomposing $c$ with $\alpha$.

CategoryTheory.Limits.colimit.pre_map theorem

 [HasColimitsOfShape K C] (E : K ⥤ J) : colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E

Full source

theorem colimit.pre_map [HasColimitsOfShape K C] (E : K ⥤ J) :
    colimit.precolimit.pre F E ≫ colim.map α = colimcolim.map (whiskerLeft E α) ≫ colimit.pre G E := by
  ext
  rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
  rfl

Commutativity of Precomposition and Mapping for Colimits: $\text{pre}_F \circ \text{map}_\alpha = \text{map}_{\alpha \circ E} \circ \text{pre}_G$

Informal description

Let $C$ be a category with colimits of shape $K$, and let $F, G \colon J \to C$ be functors with a natural transformation $\alpha \colon F \Rightarrow G$. For any functor $E \colon K \to J$, the diagram \[ \text{colimit}\, (E \circ F) \xrightarrow{\text{colimit.pre}\, F\, E} \text{colimit}\, F \] \[ \downarrow{\text{colim.map}\, (\text{whiskerLeft}\, E\, \alpha)} \quad \downarrow{\text{colim.map}\, \alpha} \] \[ \text{colimit}\, (E \circ G) \xrightarrow{\text{colimit.pre}\, G\, E} \text{colimit}\, G \] commutes. Here $\text{whiskerLeft}\, E\, \alpha$ denotes the whiskering of $\alpha$ with $E$ on the left.

CategoryTheory.Limits.colimit.pre_map' theorem

 [HasColimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
  colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂

Full source

theorem colimit.pre_map' [HasColimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
    colimit.pre F E₁ = colimcolim.map (whiskerRight α F) ≫ colimit.pre F E₂ := by
  ext1
  simp [← assoc, assoc]

Compatibility of precomposition with colimits under natural transformations: $\text{pre}_{E_1} = \text{map}(\alpha \circ F) \circ \text{pre}_{E_2}$

Informal description

Let $C$ be a category with colimits of shape $K$, and let $F \colon J \to C$ be a functor. For any pair of functors $E_1, E_2 \colon K \to J$ and a natural transformation $\alpha \colon E_1 \Rightarrow E_2$, the canonical morphism $\text{colimit.pre}\, F\, E_1$ from the colimit of $F \circ E_1$ to the colimit of $F$ equals the composition of the morphism $\text{colim.map}\, (\alpha \circ F)$ (induced by whiskering $\alpha$ with $F$) with the canonical morphism $\text{colimit.pre}\, F\, E_2$.

CategoryTheory.Limits.colimit.pre_id theorem

(F : J ⥤ C) : colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom

Full source

theorem colimit.pre_id (F : J ⥤ C) :
    colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom := by aesop_cat

Canonical Morphism from Colimit of Composition with Identity Functor Equals Left Unitor Morphism

Informal description

For any functor $F \colon J \to C$, the canonical morphism $\text{colimit.pre}\, F\, \text{id}_J$ from the colimit of $F$ composed with the identity functor $\text{id}_J$ to the colimit of $F$ is equal to the morphism induced by the left unitor natural isomorphism of $F$.

CategoryTheory.Limits.colimit.map_post theorem

 {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D] (H : C ⥤ D) :
  /- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
               H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/colimit.post F H ≫ H.map (colim.map α) =
    colim.map (whiskerRight α H) ≫ colimit.post G H

Full source

theorem colimit.map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D]
    (H : C ⥤ D) :/- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
             H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
          colimit.postcolimit.post
          F H ≫
        H.map (colim.map α) =
      colimcolim.map (whiskerRight α H) ≫ colimit.post G H := by
  ext
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
  rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
  rfl

Commutativity of Postcomposition and Colimit Morphisms: $H(\text{colim}\, \alpha) \circ \text{post}_F = \text{post}_G \circ \text{colim}(\alpha \circ H)$

Informal description

Let $C$ and $D$ be categories where $D$ has colimits of shape $J$, and let $H \colon C \to D$ be a functor. For any natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon J \to C$, the following diagram commutes: \[ \text{colimit.post}\, F\, H \circ H(\text{colim.map}\, \alpha) = \text{colim.map}\, (\alpha \circ H) \circ \text{colimit.post}\, G\, H \] Here: - $\text{colimit.post}\, F\, H$ is the canonical morphism from $\text{colimit}\, (F \circ H)$ to $H(\text{colimit}\, F)$, - $\text{colim.map}\, \alpha$ is the morphism between colimits induced by $\alpha$, - $\alpha \circ H$ denotes the whiskering of $\alpha$ with $H$.

CategoryTheory.Limits.colimCoyoneda definition

: colim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cocones J C

Full source

/-- The isomorphism between
morphisms from the cone point of the colimit cocone for `F` to `W`
and cocones over `F` with cone point `W`
is natural in `F`.
-/
def colimCoyoneda : colimcolim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}colim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}
    ≅ CategoryTheory.cocones J C :=
  NatIso.ofComponents fun F => NatIso.ofComponents fun W => colimit.homIso (unop F) W

Natural isomorphism between colimit-coyoneda composition and cocone functor

Informal description

The natural isomorphism `colimCoyoneda` establishes an equivalence between the composition of three functors: the opposite of the colimit functor, the co-Yoneda embedding, and the type lifting functor; and the functor of cocones over diagrams of shape $J$ in category $C$. More precisely, for any functor $F \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$ (viewed as an object in $(J \to C)^{\mathrm{op}}$) and object $W$ in $C$, there is a natural isomorphism between: 1. The lifted hom-set $\mathrm{ULift}(\mathrm{colimit}\, F \to W)$ (obtained by first taking colimits, then applying co-Yoneda and type lifting) 2. The set of cocones over $F$ with apex $W$ This isomorphism arises from the universal property of colimits and the Yoneda lemma.

CategoryTheory.Limits.colimConstAdj definition

: (colim : (J ⥤ C) ⥤ C) ⊣ const J

Full source

/-- The colimit functor and constant functor are adjoint to each other
-/
def colimConstAdj : (colim : (J ⥤ C) ⥤ C) ⊣ const J := Adjunction.mk' {
  homEquiv := fun f c ↦
    { toFun := fun g =>
        { app := fun _ => colimit.ιcolimit.ι _ _ ≫ g }
      invFun := fun g => colimit.desc _ ⟨_, g⟩
      left_inv := by aesop_cat
      right_inv := by aesop_cat }
  unit := { app := fun g => { app := colimit.ι _ } }
  counit := { app := fun _ => colimit.desc _ ⟨_, 𝟙 _⟩ } }

Adjunction between colimit and constant functors

Informal description

The colimit functor $\text{colim} \colon (J \to C) \to C$ is left adjoint to the constant functor $\text{const}_J \colon C \to (J \to C)$. This means there is a natural bijection between morphisms $\text{colim}\, F \to c$ in $C$ and natural transformations $F \Rightarrow \text{const}_J\, c$ for any functor $F \colon J \to C$ and object $c \in C$. The adjunction is constructed explicitly via: - The unit $\eta \colon \text{id} \Rightarrow \text{const}_J \circ \text{colim}$ with components $\eta_F \colon F \Rightarrow \text{const}_J (\text{colim}\, F)$ given by the colimit coprojections $\text{colimit.ι}\, F\, j \colon F(j) \to \text{colim}\, F$. - The counit $\epsilon \colon \text{colim} \circ \text{const}_J \Rightarrow \text{id}$ with components $\epsilon_c \colon \text{colim}\, (\text{const}_J\, c) \to c$ given by the universal property of the colimit.

CategoryTheory.Limits.instIsLeftAdjointFunctorColim instance

: IsLeftAdjoint (colim : (J ⥤ C) ⥤ C)

Full source

instance : IsLeftAdjoint (colim : (J ⥤ C) ⥤ C) :=
  ⟨_, ⟨colimConstAdj⟩⟩

Colimit Functor is Left Adjoint

Informal description

The colimit functor $\text{colim} \colon (J \to C) \to C$ is a left adjoint functor.

CategoryTheory.Limits.colimMap_epi' instance

{F G : J ⥤ C} [HasColimitsOfShape J C] (α : F ⟶ G) [Epi α] : Epi (colimMap α)

Full source

instance colimMap_epi' {F G : J ⥤ C} [HasColimitsOfShape J C] (α : F ⟶ G) [Epi α] :
    Epi (colimMap α) :=
  (colim : (J ⥤ C) ⥤ C).map_epi α

Epimorphic Natural Transformation Induces Epimorphism on Colimits (Functor Category Version)

Informal description

For any functors $F, G \colon J \to C$ in a category $C$ with colimits of shape $J$, if the natural transformation $\alpha \colon F \Rightarrow G$ is an epimorphism in the functor category, then the induced morphism $\text{colimMap}\, \alpha \colon \text{colim}\, F \to \text{colim}\, G$ is an epimorphism in $C$.

CategoryTheory.Limits.colimMap_epi instance

{F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) [∀ j, Epi (α.app j)] : Epi (colimMap α)

Full source

instance colimMap_epi {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) [∀ j, Epi (α.app j)] :
    Epi (colimMap α) :=
  ⟨fun {Z} u v h =>
    colimit.hom_ext fun j => (cancel_epi (α.app j)).1 <| by simpa using colimit.ι _ j ≫= h⟩

Epimorphic Natural Transformation Induces Epimorphism on Colimits

Informal description

Let $F, G \colon J \to C$ be functors in a category $C$ that have colimits, and let $\alpha \colon F \Rightarrow G$ be a natural transformation. If for every object $j$ in $J$, the component $\alpha_j \colon F(j) \to G(j)$ is an epimorphism, then the induced morphism $\text{colimMap}\, \alpha \colon \text{colimit}\, F \to \text{colimit}\, G$ is also an epimorphism.

CategoryTheory.Limits.hasColimitsOfShape_of_equivalence theorem

{J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J') [HasColimitsOfShape J C] : HasColimitsOfShape J' C

Full source

/-- We can transport colimits of shape `J` along an equivalence `J ≌ J'`.
-/
theorem hasColimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
    [HasColimitsOfShape J C] : HasColimitsOfShape J' C := by
  constructor
  intro F
  apply hasColimit_of_equivalence_comp e

Transport of Colimits Along Equivalence of Categories

Informal description

Let $J$ and $J'$ be categories with an equivalence $e \colon J \simeq J'$. If a category $C$ has colimits of shape $J$, then it also has colimits of shape $J'$.

CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE theorem

[UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfSize.{v₂, u₂} C

Full source

/-- A category that has larger colimits also has smaller colimits. -/
theorem hasColimitsOfSizeOfUnivLE [UnivLEUnivLE.{v₂, v₁}] [UnivLEUnivLE.{u₂, u₁}]
    [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfSize.{v₂, u₂} C where
  has_colimits_of_shape J {_} := hasColimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Existence of Smaller Colimits from Larger Colimits under Universe Constraints

Informal description

Let $\mathcal{C}$ be a category with colimits of size $(v₁, u₁)$. If the universe levels $v₂$ and $u₂$ are less than or equal to $v₁$ and $u₁$ respectively (denoted by $\text{UnivLE}\{v₂, v₁\}$ and $\text{UnivLE}\{u₂, u₁\}$), then $\mathcal{C}$ also has colimits of size $(v₂, u₂)$.

CategoryTheory.Limits.hasColimitsOfSizeShrink theorem

[HasColimitsOfSize.{max v₁ v₂, max u₁ u₂} C] : HasColimitsOfSize.{v₁, u₁} C

Full source

/-- `hasColimitsOfSizeShrink.{v u} C` tries to obtain `HasColimitsOfSize.{v u} C`
from some other `HasColimitsOfSize C`.
-/
theorem hasColimitsOfSizeShrink [HasColimitsOfSize.{max v₁ v₂, max u₁ u₂} C] :
    HasColimitsOfSize.{v₁, u₁} C := hasColimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

Existence of Smaller Colimits via Universe Shrinkage

Informal description

If a category $\mathcal{C}$ has colimits of size $(\max(v₁, v₂), \max(u₁, u₂))$, then it also has colimits of size $(v₁, u₁)$.

CategoryTheory.Limits.hasSmallestColimitsOfHasColimits instance

[HasColimits C] : HasColimitsOfSize.{0, 0} C

Full source

instance (priority := 100) hasSmallestColimitsOfHasColimits [HasColimits C] :
    HasColimitsOfSize.{0, 0} C :=
  hasColimitsOfSizeShrink.{0, 0} C

Existence of Smallest Colimits in Categories with All Colimits

Informal description

Every category $\mathcal{C}$ that has all (small) colimits also has colimits indexed by the smallest possible categories (those of size $(0, 0)$).

CategoryTheory.Limits.IsLimit.op definition

{t : Cone F} (P : IsLimit t) : IsColimit t.op

Full source

/-- If `t : Cone F` is a limit cone, then `t.op : Cocone F.op` is a colimit cocone.
-/
def IsLimit.op {t : Cone F} (P : IsLimit t) : IsColimit t.op where
  desc s := (P.lift s.unop).op
  fac s j := congrArg Quiver.Hom.op (P.fac s.unop (unop j))
  uniq s m w := by
    dsimp
    rw [← P.uniq s.unop m.unop]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Opposite of a limit cone is a colimit cocone

Informal description

Given a cone $ t $ over a functor $ F \colon J \to C $ that is a limit cone, the opposite cocone $ t^{\mathrm{op}} $ is a colimit cocone for the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $. Specifically: - For any cocone $ s $ over $ F^{\mathrm{op}} $, the colimit morphism $ s.\mathrm{pt} \to t^{\mathrm{op}}.\mathrm{pt} $ is obtained by taking the limit morphism of the unopposite cone $ s^{\mathrm{unop}} $ and applying the opposite operation. - The factorization property follows from the corresponding property of the limit cone $ t $. - The uniqueness property is derived from the uniqueness of the limit cone $ t $.

CategoryTheory.Limits.IsColimit.op definition

{t : Cocone F} (P : IsColimit t) : IsLimit t.op

Full source

/-- If `t : Cocone F` is a colimit cocone, then `t.op : Cone F.op` is a limit cone.
-/
def IsColimit.op {t : Cocone F} (P : IsColimit t) : IsLimit t.op where
  lift s := (P.desc s.unop).op
  fac s j := congrArg Quiver.Hom.op (P.fac s.unop (unop j))
  uniq s m w := by
    dsimp
    rw [← P.uniq s.unop m.unop]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Opposite of a colimit cocone is a limit cone

Informal description

Given a cocone $ t $ over a functor $ F \colon J \to C $ that is a colimit cocone, the opposite cone $ t^{\mathrm{op}} $ is a limit cone for the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $. Specifically: - For any cone $ s $ over $ F^{\mathrm{op}} $, the limit morphism $ t^{\mathrm{op}}.\mathrm{pt} \to s.\mathrm{pt} $ is obtained by taking the colimit morphism of the unopposite cocone $ s^{\mathrm{unop}} $ and applying the opposite operation. - The factorization property follows from the corresponding property of the colimit cocone $ t $. - The uniqueness property is derived from the uniqueness of the colimit cocone $ t $.

CategoryTheory.Limits.IsLimit.unop definition

{t : Cone F.op} (P : IsLimit t) : IsColimit t.unop

Full source

/-- If `t : Cone F.op` is a limit cone, then `t.unop : Cocone F` is a colimit cocone.
-/
def IsLimit.unop {t : Cone F.op} (P : IsLimit t) : IsColimit t.unop where
  desc s := (P.lift s.op).unop
  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (.op j))
  uniq s m w := by
    dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Colimit cocone from opposite limit cone

Informal description

Given a cone $ t $ over the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $ that is a limit cone, the unopposite cocone $ t.\mathrm{unop} $ is a colimit cocone for the original functor $ F \colon J \to C $. Specifically: - For any cocone $ s $ over $ F $, the colimit morphism $ s.\mathrm{pt} \to t.\mathrm{unop}.\mathrm{pt} $ is obtained by taking the limit morphism of the opposite cone $ s^{\mathrm{op}} $ and applying the unopposite operation. - The factorization property follows from the corresponding property of the limit cone $ t $. - The uniqueness property is derived from the uniqueness of the limit cone $ t $.

CategoryTheory.Limits.IsColimit.unop definition

{t : Cocone F.op} (P : IsColimit t) : IsLimit t.unop

Full source

/-- If `t : Cocone F.op` is a colimit cocone, then `t.unop : Cone F` is a limit cone.
-/
def IsColimit.unop {t : Cocone F.op} (P : IsColimit t) : IsLimit t.unop where
  lift s := (P.desc s.op).unop
  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (.op j))
  uniq s m w := by
    dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Limit cone from opposite colimit cocone

Informal description

Given a cocone $t$ over the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$ that is a colimit cocone, the unopposite cone $t.\mathrm{unop}$ is a limit cone for the original functor $F \colon J \to C$. Specifically: - For any cone $s$ over $F$, the lift morphism is obtained by taking the desc morphism of the opposite cocone $s^{\mathrm{op}}$ and applying the unopposite operation. - The factorization property follows from the corresponding property of the colimit cocone $t$. - The uniqueness property is derived from the uniqueness of the colimit cocone $t$.

CategoryTheory.Limits.isLimitOfOp definition

{t : Cone F} (P : IsColimit t.op) : IsLimit t

Full source

/-- If `t.op : Cocone F.op` is a colimit cocone, then `t : Cone F` is a limit cone. -/
def isLimitOfOp {t : Cone F} (P : IsColimit t.op) : IsLimit t :=
  P.unop

Limit cone from opposite colimit cocone

Informal description

Given a cone $t$ over a functor $F \colon J \to C$, if the opposite cocone $t^{\mathrm{op}}$ is a colimit cocone for the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$, then $t$ is a limit cone for $F$.

CategoryTheory.Limits.isColimitOfOp definition

{t : Cocone F} (P : IsLimit t.op) : IsColimit t

Full source

/-- If `t.op : Cone F.op` is a limit cone, then `t : Cocone F` is a colimit cocone. -/
def isColimitOfOp {t : Cocone F} (P : IsLimit t.op) : IsColimit t :=
  P.unop

Colimit cocone from opposite limit cone

Informal description

Given a cocone $ t $ over a functor $ F \colon J \to C $, if the opposite cone $ t^{\mathrm{op}} $ is a limit cone in the opposite category $ C^{\mathrm{op}} $, then $ t $ is a colimit cocone in $ C $.

CategoryTheory.Limits.isLimitOfUnop definition

{t : Cone F.op} (P : IsColimit t.unop) : IsLimit t

Full source

/-- If `t.unop : Cocone F` is a colimit cocone, then `t : Cone F.op` is a limit cone. -/
def isLimitOfUnop {t : Cone F.op} (P : IsColimit t.unop) : IsLimit t :=
  P.op

Limit cone from unopposed colimit cocone

Informal description

Given a cone $ t $ over the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $, if the unopposed cocone $ t.\mathrm{unop} $ is a colimit cocone for $ F \colon J \to C $, then $ t $ is a limit cone for $ F^{\mathrm{op}} $.

CategoryTheory.Limits.isColimitOfUnop definition

{t : Cocone F.op} (P : IsLimit t.unop) : IsColimit t

Full source

/-- If `t.unop : Cone F` is a limit cone, then `t : Cocone F.op` is a colimit cocone. -/
def isColimitOfUnop {t : Cocone F.op} (P : IsLimit t.unop) : IsColimit t :=
  P.op

Colimit cocone from opposite limit cone

Informal description

Given a cocone $t$ over the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$, if the unopposite cone $t^{\mathrm{unop}}$ is a limit cone for $F \colon J \to C$, then $t$ is a colimit cocone for $F^{\mathrm{op}}$.

CategoryTheory.Limits.isLimitEquivIsColimitOp definition

{t : Cone F} : IsLimit t ≃ IsColimit t.op

Full source

/-- `t : Cone F` is a limit cone if and only if `t.op : Cocone F.op` is a colimit cocone.
-/
def isLimitEquivIsColimitOp {t : Cone F} : IsLimitIsLimit t ≃ IsColimit t.op :=
  equivOfSubsingletonOfSubsingleton IsLimit.op isLimitOfOp

Equivalence between limit cones and opposite colimit cocones

Informal description

For any cone $ t $ over a functor $ F \colon J \to C $, the property of $ t $ being a limit cone is equivalent to the property of its opposite cocone $ t^{\mathrm{op}} $ being a colimit cocone for the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $.

CategoryTheory.Limits.isColimitEquivIsLimitOp definition

{t : Cocone F} : IsColimit t ≃ IsLimit t.op

Full source

/-- `t : Cocone F` is a colimit cocone if and only if `t.op : Cone F.op` is a limit cone.
-/
def isColimitEquivIsLimitOp {t : Cocone F} : IsColimitIsColimit t ≃ IsLimit t.op :=
  equivOfSubsingletonOfSubsingleton IsColimit.op isColimitOfOp

Equivalence between colimit cocones and opposite limit cones

Informal description

A cocone $ t $ over a functor $ F \colon J \to C $ is a colimit cocone if and only if the opposite cone $ t^{\mathrm{op}} $ is a limit cone for the opposite functor $ F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}} $.

Mathlib.CategoryTheory.Limits.HasLimits

Implementation

References