Mathlib.CategoryTheory.Limits.IsLimit

CategoryTheory.Limits.IsLimit structure

(t : Cone F)

Full source

/-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
cone morphism to `t`. -/
@[stacks 002E]
structure IsLimit (t : Cone F) where
  /-- There is a morphism from any cone point to `t.pt` -/
  lift : ∀ s : Cone F, s.pt ⟶ t.pt
  /-- The map makes the triangle with the two natural transformations commute -/
  fac : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j := by aesop_cat
  /-- It is the unique such map to do this -/
  uniq : ∀ (s : Cone F) (m : s.pt ⟶ t.pt) (_ : ∀ j : J, m ≫ t.π.app j = s.π.app j), m = lift s := by
    aesop_cat

Limit cone

Informal description

A cone $ t $ on a functor $ F \colon J \to C $ is called a *limit cone* if for every other cone $ s $ on $ F $, there exists a unique morphism of cones from $ s $ to $ t $. This means $ t $ is universal among all cones on $ F $.

CategoryTheory.Limits.IsLimit.subsingleton instance

{t : Cone F} : Subsingleton (IsLimit t)

Full source

instance subsingleton {t : Cone F} : Subsingleton (IsLimit t) :=
  ⟨by intro P Q; cases P; cases Q; congr; aesop_cat⟩

Uniqueness of Limit Cones

Informal description

For any cone $t$ over a functor $F \colon J \to C$, the type of proofs that $t$ is a limit cone is a subsingleton (i.e., has at most one element). This means that the property of being a limit cone is unique up to unique isomorphism.

CategoryTheory.Limits.IsLimit.map definition

{F G : J ⥤ C} (s : Cone F) {t : Cone G} (P : IsLimit t) (α : F ⟶ G) : s.pt ⟶ t.pt

Full source

/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cone point
of any cone over `F` to the cone point of a limit cone over `G`. -/
def map {F G : J ⥤ C} (s : Cone F) {t : Cone G} (P : IsLimit t) (α : F ⟶ G) : s.pt ⟶ t.pt :=
  P.lift ((Cones.postcompose α).obj s)

Induced morphism between cone vertices via natural transformation

Informal description

Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon J \to C$, and a cone $s$ over $F$, the morphism $\text{IsLimit.map}\ s\ P\ \alpha$ is the unique morphism from the vertex of $s$ to the vertex of a limit cone $t$ over $G$ (where $P$ witnesses that $t$ is a limit cone), induced by the universal property of the limit cone $t$.

CategoryTheory.Limits.IsLimit.map_π theorem

 {F G : J ⥤ C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) :
  hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j

Full source

@[reassoc (attr := simp)]
theorem map_π {F G : J ⥤ C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) :
    hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j :=
  fac _ _ _

Commutativity of Induced Morphism with Cone Projections

Informal description

Given functors $F, G \colon J \to C$, a cone $c$ over $F$, a limit cone $d$ over $G$ (witnessed by $hd$), a natural transformation $\alpha \colon F \to G$, and an object $j \in J$, the following diagram commutes: \[ hd.\text{map}\ c\ \alpha \circ d.\pi_j = c.\pi_j \circ \alpha_j \] where $hd.\text{map}\ c\ \alpha$ is the induced morphism from the vertex of $c$ to the vertex of $d$, $d.\pi_j$ is the projection from the vertex of $d$ to $G(j)$, and $c.\pi_j$ is the projection from the vertex of $c$ to $F(j)$.

CategoryTheory.Limits.IsLimit.lift_self theorem

{c : Cone F} (t : IsLimit c) : t.lift c = 𝟙 c.pt

Full source

@[simp]
theorem lift_self {c : Cone F} (t : IsLimit c) : t.lift c = 𝟙 c.pt :=
  (t.uniq _ _ fun _ => id_comp _).symm

Identity Lift of a Limit Cone to Itself

Informal description

For any limit cone $ c $ of a functor $ F \colon J \to C $, the lift of $ c $ to itself via the limit property is the identity morphism on the vertex of $ c $, i.e., $ t.\text{lift}\ c = \text{id}_{c.\text{pt}} $.

CategoryTheory.Limits.IsLimit.liftConeMorphism definition

{t : Cone F} (h : IsLimit t) (s : Cone F) : s ⟶ t

Full source

/-- The universal morphism from any other cone to a limit cone. -/
@[simps]
def liftConeMorphism {t : Cone F} (h : IsLimit t) (s : Cone F) : s ⟶ t where hom := h.lift s

Universal morphism from a cone to a limit cone

Informal description

Given a limit cone $ t $ for a functor $ F \colon J \to C $ and another cone $ s $ over $ F $, there exists a unique morphism of cones from $ s $ to $ t $. This morphism is constructed using the universal property of the limit cone $ t $.

CategoryTheory.Limits.IsLimit.uniq_cone_morphism theorem

{s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f'

Full source

theorem uniq_cone_morphism {s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f' :=
  have : ∀ {g : s ⟶ t}, g = h.liftConeMorphism s := by
    intro g; apply ConeMorphism.ext; exact h.uniq _ _ g.w
  this.trans this.symm

Uniqueness of Morphisms to a Limit Cone

Informal description

Given a limit cone $t$ for a functor $F \colon J \to C$ and two morphisms of cones $f, f' \colon s \to t$ from another cone $s$ to $t$, the morphisms $f$ and $f'$ are equal. This expresses the uniqueness part of the universal property of a limit cone.

CategoryTheory.Limits.IsLimit.existsUnique theorem

{t : Cone F} (h : IsLimit t) (s : Cone F) : ∃! l : s.pt ⟶ t.pt, ∀ j, l ≫ t.π.app j = s.π.app j

Full source

/-- Restating the definition of a limit cone in terms of the ∃! operator. -/
theorem existsUnique {t : Cone F} (h : IsLimit t) (s : Cone F) :
    ∃! l : s.pt ⟶ t.pt, ∀ j, l ≫ t.π.app j = s.π.app j :=
  ⟨h.lift s, h.fac s, h.uniq s⟩

Unique Factorization Property of Limit Cones

Informal description

Given a limit cone $t$ for a functor $F \colon J \to C$ and another cone $s$ over $F$, there exists a unique morphism $l \colon s.pt \to t.pt$ such that for every object $j$ in $J$, the composition $l \circ t.\pi_j = s.\pi_j$.

CategoryTheory.Limits.IsLimit.ofExistsUnique definition

{t : Cone F} (ht : ∀ s : Cone F, ∃! l : s.pt ⟶ t.pt, ∀ j, l ≫ t.π.app j = s.π.app j) : IsLimit t

Full source

/-- Noncomputably make a limit cone from the existence of unique factorizations. -/
def ofExistsUnique {t : Cone F}
    (ht : ∀ s : Cone F, ∃! l : s.pt ⟶ t.pt, ∀ j, l ≫ t.π.app j = s.π.app j) : IsLimit t := by
  choose s hs hs' using ht
  exact ⟨s, hs, hs'⟩

Characterization of limit cone via unique factorization

Informal description

Given a cone $ t $ on a functor $ F \colon J \to C $, if for every other cone $ s $ on $ F $ there exists a unique morphism $ l \colon s.pt \to t.pt $ such that for all $ j $, the composition $ l \circ t.\pi_j = s.\pi_j $, then $ t $ is a limit cone.

CategoryTheory.Limits.IsLimit.mkConeMorphism definition

{t : Cone F} (lift : ∀ s : Cone F, s ⟶ t) (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t

Full source

/-- Alternative constructor for `isLimit`,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
-/
@[simps]
def mkConeMorphism {t : Cone F} (lift : ∀ s : Cone F, s ⟶ t)
    (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t where
  lift s := (lift s).hom
  uniq s m w :=
    have : ConeMorphism.mk m w = lift s := by apply uniq
    congrArg ConeMorphism.hom this

Limit cone via cone morphisms

Informal description

Given a cone $ t $ on a functor $ F \colon J \to C $, if there exists a function that assigns to every other cone $ s $ on $ F $ a morphism of cones from $ s $ to $ t $, and this assignment is unique (i.e., any other morphism of cones from $ s $ to $ t $ must equal the assigned one), then $ t $ is a limit cone.

CategoryTheory.Limits.IsLimit.uniqueUpToIso definition

{s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s ≅ t

Full source

/-- Limit cones on `F` are unique up to isomorphism. -/
@[simps]
def uniqueUpToIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s ≅ t where
  hom := Q.liftConeMorphism s
  inv := P.liftConeMorphism t
  hom_inv_id := P.uniq_cone_morphism
  inv_hom_id := Q.uniq_cone_morphism

Uniqueness of limit cones up to isomorphism

Informal description

Given two limit cones $ s $ and $ t $ for a functor $ F \colon J \to C $, there exists an isomorphism between $ s $ and $ t $ in the category of cones over $ F $. This isomorphism is constructed using the universal properties of the limit cones, with the morphisms given by the unique cone morphisms from each limit cone to the other.

CategoryTheory.Limits.IsLimit.hom_isIso theorem

{s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (f : s ⟶ t) : IsIso f

Full source

/-- Any cone morphism between limit cones is an isomorphism. -/
theorem hom_isIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (f : s ⟶ t) : IsIso f :=
  ⟨⟨P.liftConeMorphism t, ⟨P.uniq_cone_morphism, Q.uniq_cone_morphism⟩⟩⟩

Morphism between limit cones is an isomorphism

Informal description

Given two limit cones $s$ and $t$ for a functor $F \colon J \to C$, any morphism of cones $f \colon s \to t$ is an isomorphism.

CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso definition

{s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s.pt ≅ t.pt

Full source

/-- Limits of `F` are unique up to isomorphism. -/
def conePointUniqueUpToIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s.pt ≅ t.pt :=
  (Cones.forget F).mapIso (uniqueUpToIso P Q)

Isomorphism between apexes of limit cones

Informal description

Given two limit cones $ s $ and $ t $ for a functor $ F \colon J \to C $, there exists an isomorphism between their apex objects $ s.pt $ and $ t.pt $ in the category $ C $. This isomorphism is induced by the unique cone morphisms provided by the universal properties of the limit cones.

CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp theorem

{s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) : (conePointUniqueUpToIso P Q).hom ≫ t.π.app j = s.π.app j

Full source

@[reassoc (attr := simp)]
theorem conePointUniqueUpToIso_hom_comp {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) :
    (conePointUniqueUpToIso P Q).hom ≫ t.π.app j = s.π.app j :=
  (uniqueUpToIso P Q).hom.w _

Compatibility of limit cone isomorphism with projections

Informal description

Given two limit cones $s$ and $t$ for a functor $F \colon J \to C$, the isomorphism between their apex objects $\varphi \colon s.pt \to t.pt$ (induced by their universal properties) satisfies $\varphi \circ t.\pi_j = s.\pi_j$ for every object $j$ in $J$, where $s.\pi_j$ and $t.\pi_j$ are the projection morphisms from the respective cones.

CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp theorem

{s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) : (conePointUniqueUpToIso P Q).inv ≫ s.π.app j = t.π.app j

Full source

@[reassoc (attr := simp)]
theorem conePointUniqueUpToIso_inv_comp {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) :
    (conePointUniqueUpToIso P Q).inv ≫ s.π.app j = t.π.app j :=
  (uniqueUpToIso P Q).inv.w _

Inverse Isomorphism of Limit Cones Commutes with Projections

Informal description

For any two limit cones $s$ and $t$ of a functor $F \colon J \to C$ and any object $j$ in $J$, the composition of the inverse of the isomorphism between the apexes of $s$ and $t$ with the projection morphism $s.\pi_j$ equals the projection morphism $t.\pi_j$.

CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom theorem

{r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : P.lift r ≫ (conePointUniqueUpToIso P Q).hom = Q.lift r

Full source

@[reassoc (attr := simp)]
theorem lift_comp_conePointUniqueUpToIso_hom {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
    P.lift r ≫ (conePointUniqueUpToIso P Q).hom = Q.lift r :=
  Q.uniq _ _ (by simp)

Compatibility of limit cone lifts with apex isomorphism

Informal description

Given three cones $r$, $s$, and $t$ over a functor $F \colon J \to C$, where $s$ and $t$ are limit cones, the composition of the unique morphism $P.\text{lift}(r)$ from $r$ to $s$ with the isomorphism $\varphi \colon s.\text{pt} \to t.\text{pt}$ (induced by the limit properties) equals the unique morphism $Q.\text{lift}(r)$ from $r$ to $t$. In other words, the following diagram commutes: \[ P.\text{lift}(r) \circ \varphi = Q.\text{lift}(r). \]

CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv theorem

{r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r

Full source

@[reassoc (attr := simp)]
theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
    Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
  P.uniq _ _ (by simp)

Compatibility of lift with inverse apex isomorphism in limit cones

Informal description

Given three cones $r$, $s$, and $t$ over a functor $F \colon J \to C$, where $s$ and $t$ are limit cones, the composition of the lift morphism from $r$ to $t$ (via $Q$) with the inverse of the isomorphism between the apexes of $s$ and $t$ equals the lift morphism from $r$ to $s$ (via $P$). In symbols: $$ Q.\text{lift}(r) \circ (\text{conePointUniqueUpToIso}\ P\ Q)^{-1} = P.\text{lift}(r). $$

CategoryTheory.Limits.IsLimit.ofIsoLimit definition

{r t : Cone F} (P : IsLimit r) (i : r ≅ t) : IsLimit t

Full source

/-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
def ofIsoLimit {r t : Cone F} (P : IsLimit r) (i : r ≅ t) : IsLimit t :=
  IsLimit.mkConeMorphism (fun s => P.liftConeMorphism s ≫ i.hom) fun s m => by
    rw [← i.comp_inv_eq]; apply P.uniq_cone_morphism

Limit cone transport along isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cones $r$ and $t$ over a functor $F \colon J \to C$, if $r$ is a limit cone, then $t$ is also a limit cone. The limit structure on $t$ is constructed by transporting the universal property of $r$ along the isomorphism $i$.

CategoryTheory.Limits.IsLimit.ofIsoLimit_lift theorem

{r t : Cone F} (P : IsLimit r) (i : r ≅ t) (s) : (P.ofIsoLimit i).lift s = P.lift s ≫ i.hom.hom

Full source

@[simp]
theorem ofIsoLimit_lift {r t : Cone F} (P : IsLimit r) (i : r ≅ t) (s) :
    (P.ofIsoLimit i).lift s = P.lift s ≫ i.hom.hom :=
  rfl

Lift Morphism Transport Along Cone Isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cones $r$ and $t$ over a functor $F \colon J \to C$, if $r$ is a limit cone, then for any cone $s$ over $F$, the lift morphism from $s$ to $t$ (via the transported limit structure) is equal to the composition of the lift morphism from $s$ to $r$ with the forward component of the isomorphism $i$. In other words, $(P.\text{ofIsoLimit}\ i).\text{lift}\ s = P.\text{lift}\ s \circ i.\text{hom}.\text{hom}$.

CategoryTheory.Limits.IsLimit.equivIsoLimit definition

{r t : Cone F} (i : r ≅ t) : IsLimit r ≃ IsLimit t

Full source

/-- Isomorphism of cones preserves whether or not they are limiting cones. -/
def equivIsoLimit {r t : Cone F} (i : r ≅ t) : IsLimitIsLimit r ≃ IsLimit t where
  toFun h := h.ofIsoLimit i
  invFun h := h.ofIsoLimit i.symm
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of limit cone properties under cone isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cones $r$ and $t$ over a functor $F \colon J \to C$, there is an equivalence between the types asserting that $r$ is a limit cone and that $t$ is a limit cone. This equivalence is constructed by transporting the limit structure along the isomorphism $i$ in both directions.

CategoryTheory.Limits.IsLimit.equivIsoLimit_apply theorem

{r t : Cone F} (i : r ≅ t) (P : IsLimit r) : equivIsoLimit i P = P.ofIsoLimit i

Full source

@[simp]
theorem equivIsoLimit_apply {r t : Cone F} (i : r ≅ t) (P : IsLimit r) :
    equivIsoLimit i P = P.ofIsoLimit i :=
  rfl

Limit Cone Equivalence Application via Isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cones $r$ and $t$ over a functor $F \colon J \to C$, and given that $r$ is a limit cone, the application of the equivalence `equivIsoLimit i` to $P$ yields the transported limit structure $P.\text{ofIsoLimit}\ i$ on $t$.

CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply theorem

{r t : Cone F} (i : r ≅ t) (P : IsLimit t) : (equivIsoLimit i).symm P = P.ofIsoLimit i.symm

Full source

@[simp]
theorem equivIsoLimit_symm_apply {r t : Cone F} (i : r ≅ t) (P : IsLimit t) :
    (equivIsoLimit i).symm P = P.ofIsoLimit i.symm :=
  rfl

Inverse of Limit Cone Equivalence via Isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cones $r$ and $t$ over a functor $F \colon J \to C$, and given that $t$ is a limit cone, the inverse of the equivalence `equivIsoLimit i` applied to $P$ (the proof that $t$ is a limit cone) is equal to transporting the limit structure along the inverse isomorphism $i^{-1} \colon t \cong r$.

CategoryTheory.Limits.IsLimit.ofPointIso definition

{r t : Cone F} (P : IsLimit r) [i : IsIso (P.lift t)] : IsLimit t

Full source

/-- If the canonical morphism from a cone point to a limiting cone point is an iso, then the
first cone was limiting also.
-/
def ofPointIso {r t : Cone F} (P : IsLimit r) [i : IsIso (P.lift t)] : IsLimit t :=
  ofIsoLimit P (by
    haveI : IsIso (P.liftConeMorphism t).hom := i
    haveI : IsIso (P.liftConeMorphism t) := Cones.cone_iso_of_hom_iso _
    symm
    apply asIso (P.liftConeMorphism t))

Limit cone via isomorphism of vertices

Informal description

Given a limit cone $ r $ for a functor $ F \colon J \to C $ and another cone $ t $ over $ F $, if the canonical morphism $ P.\mathrm{lift}\, t $ from the vertex of $ t $ to the vertex of $ r $ is an isomorphism, then $ t $ is also a limit cone for $ F $.

CategoryTheory.Limits.IsLimit.hom_lift theorem

(h : IsLimit t) {W : C} (m : W ⟶ t.pt) : m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } }

Full source

theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.pt) :
    m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } } :=
  h.uniq { pt := W, π := { app := fun b => m ≫ t.π.app b } } m fun _ => rfl

Morphism to Limit Cone Factors Through Lifting

Informal description

Let $h$ be a limit cone for a functor $F \colon J \to C$, and let $m \colon W \to t.\mathrm{pt}$ be a morphism in $C$. Then $m$ is equal to the unique morphism obtained by lifting the cone $\{ \mathrm{pt} := W, \pi := \{ \mathrm{app} := \lambda b \mapsto m \circ t.\pi.\mathrm{app}\, b \} \}$ to the limit cone $t$.

CategoryTheory.Limits.IsLimit.hom_ext theorem

(h : IsLimit t) {W : C} {f f' : W ⟶ t.pt} (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) : f = f'

Full source

/-- Two morphisms into a limit are equal if their compositions with
  each cone morphism are equal. -/
theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.pt}
    (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) :
    f = f' := by
  rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w

Uniqueness of Morphisms into Limit Cone via Commutativity Condition

Informal description

Let $t$ be a limit cone for a functor $F \colon J \to C$, and let $f, f' \colon W \to t.\mathrm{pt}$ be two morphisms in $C$. If for every object $j$ in $J$, the compositions $f \circ t.\pi.\mathrm{app}\, j$ and $f' \circ t.\pi.\mathrm{app}\, j$ are equal, then $f = f'$.

CategoryTheory.Limits.IsLimit.ofRightAdjoint definition

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} {left : Cone F ⥤ Cone G} {right : Cone G ⥤ Cone F} (adj : left ⊣ right)
  {c : Cone G} (t : IsLimit c) : IsLimit (right.obj c)

Full source

/-- Given a right adjoint functor between categories of cones,
the image of a limit cone is a limit cone.
-/
def ofRightAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} {left : ConeCone F ⥤ Cone G}
    {right : ConeCone G ⥤ Cone F}
    (adj : left ⊣ right) {c : Cone G} (t : IsLimit c) : IsLimit (right.obj c) :=
  mkConeMorphism (fun s => adj.homEquiv s c (t.liftConeMorphism _))
    fun _ _ => (Adjunction.eq_homEquiv_apply _ _ _).2 t.uniq_cone_morphism

Limit cone preservation under right adjoint functor between cone categories

Informal description

Given a right adjoint functor `right` between categories of cones, if `c` is a limit cone for a functor `G : K ⥤ D`, then the image of `c` under `right` is a limit cone for the corresponding functor in the original category. More precisely, let `left : Cone F ⥤ Cone G` and `right : Cone G ⥤ Cone F` be functors between categories of cones, with `left` being left adjoint to `right`. If `c` is a limit cone for `G`, then `right.obj c` is a limit cone for `F`.

CategoryTheory.Limits.IsLimit.ofConeEquiv definition

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G} : IsLimit (h.functor.obj c) ≃ IsLimit c

Full source

/-- Given two functors which have equivalent categories of cones, we can transport a limiting cone
across the equivalence.
-/
def ofConeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : ConeCone G ≌ Cone F) {c : Cone G} :
    IsLimitIsLimit (h.functor.obj c) ≃ IsLimit c where
  toFun P := ofIsoLimit (ofRightAdjoint h.toAdjunction P) (h.unitIso.symm.app c)
  invFun := ofRightAdjoint h.symm.toAdjunction
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Limit cone equivalence under equivalence of cone categories

Informal description

Given an equivalence of categories $h \colon \text{Cone}(G) \simeq \text{Cone}(F)$ between the categories of cones over functors $G \colon K \to D$ and $F \colon J \to C$, there is a natural equivalence between the propositions that $h.\text{functor}(c)$ is a limit cone for $F$ and that $c$ is a limit cone for $G$. More precisely, for any cone $c$ over $G$, the equivalence $h$ induces a bijection between: - The property that $h.\text{functor}(c)$ is a limit cone for $F$, and - The property that $c$ is a limit cone for $G$. This bijection is constructed using the adjunction associated to $h$ and its symmetric counterpart.

CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc theorem

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G} (P : IsLimit (h.functor.obj c)) (s) :
  (ofConeEquiv h P).lift s =
    ((h.unitIso.hom.app s).hom ≫ (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) ≫ (h.unitIso.inv.app c).hom

Full source

@[simp]
theorem ofConeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : ConeCone G ≌ Cone F)
    {c : Cone G} (P : IsLimit (h.functor.obj c)) (s) :
    (ofConeEquiv h P).lift s =
      ((h.unitIso.hom.app s).hom ≫ (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) ≫
        (h.unitIso.inv.app c).hom :=
  rfl

Limit cone lifting formula under equivalence of cone categories

Informal description

Given an equivalence of categories $h \colon \text{Cone}(G) \simeq \text{Cone}(F)$ between the categories of cones over functors $G \colon K \to D$ and $F \colon J \to C$, and given a limit cone $c$ for $G$ such that $h.\text{functor}(c)$ is a limit cone for $F$, the lifting morphism for any cone $s$ under the induced limit structure satisfies: \[ \text{lift}(s) = \left(h.\text{unitIso}.\text{hom}_s \circ h.\text{inverse}\left(\text{liftConeMorphism}(h.\text{functor}(s))\right)\right) \circ h.\text{unitIso}.\text{inv}_c \] where: - $h.\text{unitIso}.\text{hom}_s$ is the component of the unit isomorphism at $s$, - $\text{liftConeMorphism}$ is the universal morphism from $h.\text{functor}(s)$ to $h.\text{functor}(c)$, - $h.\text{unitIso}.\text{inv}_c$ is the inverse component of the unit isomorphism at $c$.

CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc theorem

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G} (P : IsLimit c) (s) :
  ((ofConeEquiv h).symm P).lift s =
    (h.counitIso.inv.app s).hom ≫ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom

Full source

@[simp]
theorem ofConeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
    (h : ConeCone G ≌ Cone F) {c : Cone G} (P : IsLimit c) (s) :
    ((ofConeEquiv h).symm P).lift s =
      (h.counitIso.inv.app s).hom ≫ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom :=
  rfl

Limit Cone Equivalence Symmetry: Lifting Morphism Formula

Informal description

Given an equivalence of categories $h \colon \text{Cone}(G) \simeq \text{Cone}(F)$ between the categories of cones over functors $G \colon K \to D$ and $F \colon J \to C$, and given a limit cone $c$ for $G$ with limit property $P$, the lifting morphism for the symmetric application of the equivalence $(h.\text{symm} P).\text{lift} s$ is equal to the composition of: 1. The inverse of the counit isomorphism of $h$ applied to $s$, and 2. The image under $h.\text{functor}$ of the universal morphism from $h.\text{inverse}(s)$ to $c$ given by $P$. In symbols: $$(h^{-1}(P)).\text{lift}(s) = (h.\text{counitIso}^{-1}_s) \circ h.\text{functor}(P.\text{liftConeMorphism}(h^{-1}(s)))$$

CategoryTheory.Limits.IsLimit.postcomposeHomEquiv definition

{F G : J ⥤ C} (α : F ≅ G) (c : Cone F) : IsLimit ((Cones.postcompose α.hom).obj c) ≃ IsLimit c

Full source

/--
A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.
-/
def postcomposeHomEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) :
    IsLimitIsLimit ((Cones.postcompose α.hom).obj c) ≃ IsLimit c :=
  ofConeEquiv (Cones.postcomposeEquivalence α)

Limit cone equivalence under postcomposition with a natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$ and a cone $c$ over $F$, there is an equivalence between the property that the postcomposition of $c$ with $\alpha$ is a limit cone and the property that $c$ itself is a limit cone. More precisely, the equivalence states that the cone obtained by postcomposing $c$ with the natural transformation $\alpha$ is a limit cone if and only if $c$ is a limit cone.

CategoryTheory.Limits.IsLimit.postcomposeInvEquiv definition

{F G : J ⥤ C} (α : F ≅ G) (c : Cone G) : IsLimit ((Cones.postcompose α.inv).obj c) ≃ IsLimit c

Full source

/-- A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if
the original cone is.
-/
def postcomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone G) :
    IsLimitIsLimit ((Cones.postcompose α.inv).obj c) ≃ IsLimit c :=
  postcomposeHomEquiv α.symm c

Limit cone equivalence under postcomposition with inverse natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$ and a cone $c$ over $G$, there is an equivalence between the property that the postcomposition of $c$ with $\alpha^{-1}$ is a limit cone and the property that $c$ itself is a limit cone. More precisely, the equivalence states that the cone obtained by postcomposing $c$ with the inverse natural transformation $\alpha^{-1}$ is a limit cone if and only if $c$ is a limit cone.

CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso definition

 {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) (d : Cone G) (w : (Cones.postcompose α.hom).obj c ≅ d) : IsLimit c ≃ IsLimit d

Full source

/-- Constructing an equivalence `IsLimit c ≃ IsLimit d` from a natural isomorphism
between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
-/
def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) (d : Cone G)
    (w : (Cones.postcompose α.hom).obj c ≅ d) : IsLimitIsLimit c ≃ IsLimit d :=
  (postcomposeHomEquiv α _).symm.trans (equivIsoLimit w)

Equivalence of limit cone properties under natural isomorphism and cone isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$, a cone $c$ over $F$, and a cone $d$ over $G$ such that the postcomposition of $c$ with $\alpha$ is isomorphic to $d$ (via $w$), there is an equivalence between the properties that $c$ is a limit cone and that $d$ is a limit cone. This equivalence is constructed by first using the inverse of the equivalence from `postcomposeHomEquiv` (which relates the limit property of $c$ and its postcomposition with $\alpha$), and then transporting this along the isomorphism $w$ via `equivIsoLimit`.

CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso definition

{F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) : s.pt ≅ t.pt

Full source

/-- The cone points of two limit cones for naturally isomorphic functors
are themselves isomorphic.
-/
@[simps]
def conePointsIsoOfNatIso {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
    (w : F ≅ G) : s.pt ≅ t.pt where
  hom := Q.map s w.hom
  inv := P.map t w.inv
  hom_inv_id := P.hom_ext (by simp)
  inv_hom_id := Q.hom_ext (by simp)

Isomorphism between limit cone vertices for naturally isomorphic functors

Informal description

Given two functors $F, G \colon J \to C$ that are naturally isomorphic via $w \colon F \cong G$, and two cones $s$ over $F$ and $t$ over $G$ that are limit cones (witnessed by $P$ and $Q$ respectively), there is an isomorphism between the vertices $s.pt$ and $t.pt$ of the cones. The isomorphism is constructed using the universal properties of the limit cones, with the forward map induced by $w.hom$ and the backward map induced by $w.inv$.

CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp theorem

 {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) :
  (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j

Full source

@[reassoc]
theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
    (Q : IsLimit t) (w : F ≅ G) (j : J) :
    (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j := by simp

Commutativity of Limit Cone Vertex Isomorphism with Projections via Natural Isomorphism

Informal description

Given two functors $F, G \colon J \to C$ that are naturally isomorphic via $w \colon F \cong G$, two cones $s$ over $F$ and $t$ over $G$ that are limit cones (witnessed by $P$ and $Q$ respectively), and an object $j \in J$, the following diagram commutes: \[ (\text{conePointsIsoOfNatIso}\ P\ Q\ w).\text{hom} \circ t.\pi_j = s.\pi_j \circ w.\text{hom}_j \] where $\text{conePointsIsoOfNatIso}\ P\ Q\ w$ is the isomorphism between the vertices of $s$ and $t$ induced by the natural isomorphism $w$, $t.\pi_j$ is the projection from the vertex of $t$ to $G(j)$, and $s.\pi_j$ is the projection from the vertex of $s$ to $F(j)$.

CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp theorem

 {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) :
  (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j

Full source

@[reassoc]
theorem conePointsIsoOfNatIso_inv_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
    (Q : IsLimit t) (w : F ≅ G) (j : J) :
    (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j := by simp

Commutativity of Inverse Limit Cone Vertex Isomorphism with Projections via Natural Isomorphism

Informal description

Given two functors $F, G \colon J \to C$ that are naturally isomorphic via $w \colon F \cong G$, two cones $s$ over $F$ and $t$ over $G$ that are limit cones (witnessed by $P$ and $Q$ respectively), and an object $j \in J$, the following diagram commutes: \[ (\text{conePointsIsoOfNatIso}\ P\ Q\ w)^{-1} \circ s.\pi_j = t.\pi_j \circ w^{-1}_j \] where $\text{conePointsIsoOfNatIso}\ P\ Q\ w$ is the isomorphism between the vertices of $s$ and $t$ induced by the natural isomorphism $w$, $s.\pi_j$ is the projection from the vertex of $s$ to $F(j)$, and $t.\pi_j$ is the projection from the vertex of $t$ to $G(j)$.

CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom theorem

 {F G : J ⥤ C} {r s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) :
  P.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom

Full source

@[reassoc]
theorem lift_comp_conePointsIsoOfNatIso_hom {F G : J ⥤ C} {r s : Cone F} {t : Cone G}
    (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) :
    P.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom :=
  Q.hom_ext (by simp)

Compatibility of Limit Cone Lifting with Vertex Isomorphism via Natural Isomorphism

Informal description

Given two functors $F, G \colon J \to C$ that are naturally isomorphic via $w \colon F \cong G$, two cones $s$ over $F$ and $t$ over $G$ that are limit cones (witnessed by $P$ and $Q$ respectively), and another cone $r$ over $F$, the following equality holds: \[ P.\text{lift}(r) \circ (\text{conePointsIsoOfNatIso}\ P\ Q\ w).\text{hom} = Q.\text{map}(r, w.\text{hom}) \] where $P.\text{lift}(r)$ is the unique morphism from the vertex of $r$ to the vertex of $s$ induced by the universal property of the limit cone $s$, $\text{conePointsIsoOfNatIso}\ P\ Q\ w$ is the isomorphism between the vertices of $s$ and $t$ induced by the natural isomorphism $w$, and $Q.\text{map}(r, w.\text{hom})$ is the unique morphism from the vertex of $r$ to the vertex of $t$ induced by the natural transformation $w.\text{hom} \colon F \to G$.

CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv theorem

 {F G : J ⥤ C} {r s : Cone G} {t : Cone F} (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) :
  Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv

Full source

@[reassoc]
theorem lift_comp_conePointsIsoOfNatIso_inv {F G : J ⥤ C} {r s : Cone G} {t : Cone F}
    (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) :
    Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv :=
  P.hom_ext (by simp)

Compatibility of Lift and Map with Cone Vertex Isomorphism via Natural Isomorphism

Informal description

Given two functors $F, G \colon J \to C$ that are naturally isomorphic via $w \colon F \cong G$, two cones $s$ over $G$ and $t$ over $F$ that are limit cones (witnessed by $Q$ and $P$ respectively), and any cone $r$ over $G$, the following equality holds: \[ Q.\text{lift}(r) \circ (\text{conePointsIsoOfNatIso}\ P\ Q\ w)^{-1} = P.\text{map}(r, w^{-1}) \] where $Q.\text{lift}(r)$ is the unique morphism from the vertex of $r$ to the vertex of $s$ induced by the universal property of the limit cone $s$, $\text{conePointsIsoOfNatIso}\ P\ Q\ w$ is the isomorphism between the vertices of $t$ and $s$ induced by $w$, and $P.\text{map}(r, w^{-1})$ is the unique morphism from the vertex of $r$ to the vertex of $t$ induced by the natural transformation $w^{-1} \colon G \to F$.

CategoryTheory.Limits.IsLimit.whiskerEquivalence definition

{s : Cone F} (P : IsLimit s) (e : K ≌ J) : IsLimit (s.whisker e.functor)

Full source

/-- If `s : Cone F` is a limit cone, so is `s` whiskered by an equivalence `e`.
-/
def whiskerEquivalence {s : Cone F} (P : IsLimit s) (e : K ≌ J) : IsLimit (s.whisker e.functor) :=
  ofRightAdjoint (Cones.whiskeringEquivalence e).symm.toAdjunction P

Limit cone preservation under whiskering by equivalence

Informal description

Given a limit cone $ s $ for a functor $ F \colon J \to C $ and an equivalence of categories $ e \colon K \simeq J $, the whiskered cone $ s.\text{whisker} e.\text{functor} $ is also a limit cone for the functor $ F \circ e.\text{functor} \colon K \to C $. In other words, whiskering a limit cone by an equivalence of categories preserves the limit property.

CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence definition

{s : Cone F} (e : K ≌ J) (P : IsLimit (s.whisker e.functor)) : IsLimit s

Full source

/-- If `s : Cone F` whiskered by an equivalence `e` is a limit cone, so is `s`.
-/
def ofWhiskerEquivalence {s : Cone F} (e : K ≌ J) (P : IsLimit (s.whisker e.functor)) : IsLimit s :=
  equivIsoLimit ((Cones.whiskeringEquivalence e).unitIso.app s).symm
    (ofRightAdjoint (Cones.whiskeringEquivalence e).toAdjunction P)

Limit cone property preserved under whiskering by equivalence

Informal description

Given a cone $ s $ over a functor $ F \colon J \to C $ and an equivalence of categories $ e \colon K \simeq J $, if the whiskered cone $ s.\text{whisker} e.\text{functor} $ is a limit cone, then $ s $ itself is a limit cone. In other words, if a cone becomes a limit cone after whiskering by an equivalence of categories, then the original cone was already a limit cone.

CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv definition

{s : Cone F} (e : K ≌ J) : IsLimit s ≃ IsLimit (s.whisker e.functor)

Full source

/-- Given an equivalence of diagrams `e`, `s` is a limit cone iff `s.whisker e.functor` is.
-/
def whiskerEquivalenceEquiv {s : Cone F} (e : K ≌ J) : IsLimitIsLimit s ≃ IsLimit (s.whisker e.functor) :=
  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by aesop_cat, by aesop_cat⟩

Equivalence between limit cone properties under whiskering by equivalence

Informal description

Given a cone $ s $ over a functor $ F \colon J \to C $ and an equivalence of categories $ e \colon K \simeq J $, there is a natural equivalence between the property of $ s $ being a limit cone and the property of the whiskered cone $ s.\text{whisker} e.\text{functor} $ being a limit cone. In other words, the whiskering operation by an equivalence of categories induces a bijection between limit cone properties.

CategoryTheory.Limits.IsLimit.extendIso definition

{s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit s) : IsLimit (s.extend i)

Full source

/-- A limit cone extended by an isomorphism is a limit cone. -/
def extendIso {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit s) :
    IsLimit (s.extend i) :=
  IsLimit.ofIsoLimit hs (Cones.extendIso s (asIso i)).symm

Limit cone extension by isomorphism

Informal description

Given a cone $ s $ over a functor $ F \colon J \to C $, a morphism $ i \colon X \to s.\text{pt} $ that is an isomorphism, and a proof $ hs $ that $ s $ is a limit cone, then the extended cone $ s.\text{extend} i $ is also a limit cone. This means that extending a limit cone by an isomorphism preserves its universal property as a limit.

CategoryTheory.Limits.IsLimit.ofExtendIso definition

{s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit (s.extend i)) : IsLimit s

Full source

/-- A cone is a limit cone if its extension by an isomorphism is. -/
def ofExtendIso {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit (s.extend i)) :
    IsLimit s :=
  IsLimit.ofIsoLimit hs (Cones.extendIso s (asIso i))

Limit cone from extended cone isomorphism

Informal description

Given a cone $s$ over a functor $F \colon J \to C$, an object $X$ in $C$, and an isomorphism $i \colon X \to s.\mathrm{pt}$ from $X$ to the apex of $s$, if the extended cone $s.\mathrm{extend}\, i$ is a limit cone, then $s$ itself is a limit cone.

CategoryTheory.Limits.IsLimit.extendIsoEquiv definition

{s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] : IsLimit s ≃ IsLimit (s.extend i)

Full source

/-- A cone is a limit cone iff its extension by an isomorphism is. -/
def extendIsoEquiv {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] :
    IsLimitIsLimit s ≃ IsLimit (s.extend i) :=
  equivOfSubsingletonOfSubsingleton (extendIso i) (ofExtendIso i)

Equivalence of limit cone properties under extension by isomorphism

Informal description

Given a cone $ s $ over a functor $ F \colon J \to C $, an object $ X $ in $ C $, and an isomorphism $ i \colon X \to s.\mathrm{pt} $, there is an equivalence between the propositions that $ s $ is a limit cone and that the extended cone $ s.\mathrm{extend}\, i $ is a limit cone. This means that extending a cone by an isomorphism preserves its status as a limit cone, and conversely, if the extended cone is a limit cone, then the original cone must also be a limit cone.

CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence definition

 {F : J ⥤ C} {s : Cone F} {G : K ⥤ C} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (e : J ≌ K) (w : e.functor ⋙ G ≅ F) :
  s.pt ≅ t.pt

Full source

/-- We can prove two cone points `(s : Cone F).pt` and `(t : Cone G).pt` are isomorphic if
* both cones are limit cones
* their indexing categories are equivalent via some `e : J ≌ K`,
* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.

This is the most general form of uniqueness of cone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
-/
@[simps]
def conePointsIsoOfEquivalence {F : J ⥤ C} {s : Cone F} {G : K ⥤ C} {t : Cone G} (P : IsLimit s)
    (Q : IsLimit t) (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) : s.pt ≅ t.pt :=
  let w' : e.inverse ⋙ Fe.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ invFunIdAssoc e G
  { hom := Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s)
    inv := P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t)
    hom_inv_id := by
      apply hom_ext P; intro j
      dsimp [w']
      simp only [Limits.Cone.whisker_π, Limits.Cones.postcompose_obj_π, fac, whiskerLeft_app,
        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
      rw [counit_app_functor, ← Functor.comp_map]
      have l :
        NatTrans.app w.hom j = NatTrans.app w.hom (Prefunctor.obj (𝟭 J).toPrefunctor j) := by dsimp
      rw [l,w.hom.naturality]
      simp
    inv_hom_id := by
      apply hom_ext Q
      aesop_cat }

Isomorphism of limit cone apexes under equivalence of indexing categories

Informal description

Given two limit cones $s$ and $t$ for functors $F \colon J \to C$ and $G \colon K \to C$ respectively, and an equivalence of categories $e \colon J \simeq K$ such that the triangle of functors commutes up to a natural isomorphism $e.\text{functor} \circ G \cong F$, the apexes $s.\text{pt}$ and $t.\text{pt}$ of the cones are isomorphic in $C$. More precisely, there exists an isomorphism between the apexes constructed via the universal properties of the limit cones, where: - The forward morphism is induced by lifting the cone $s$ through the equivalence to a cone over $G$. - The inverse morphism is induced by lifting the cone $t$ through the equivalence to a cone over $F$. - The composition of these morphisms yields the identity in both directions, establishing the isomorphism.

CategoryTheory.Limits.IsLimit.homEquiv definition

(h : IsLimit t) {W : C} : (W ⟶ t.pt) ≃ ((Functor.const J).obj W ⟶ F)

Full source

/-- The universal property of a limit cone: a wap `W ⟶ t.pt` is the same as
  a cone on `F` with cone point `W`. -/
@[simps apply]
def homEquiv (h : IsLimit t) {W : C} : (W ⟶ t.pt) ≃ ((Functor.const J).obj W ⟶ F) where
  toFun f := (t.extend f).π
  invFun π := h.lift (Cone.mk _ π)
  left_inv f := h.hom_ext (by simp)
  right_inv π := by aesop_cat

Universal property of a limit cone: morphisms into the limit correspond to cones

Informal description

Given a limit cone $ t $ for a functor $ F \colon J \to C $, the equivalence `homEquiv h` establishes a bijection between morphisms $ W \to t.\text{pt} $ and natural transformations from the constant functor at $ W $ to $ F $. More precisely, for any object $ W $ in $ C $, there is a natural equivalence: \[ (W \to t.\text{pt}) \simeq (\text{const } J(W) \Rightarrow F), \] where: - The forward map sends a morphism $ f \colon W \to t.\text{pt} $ to the natural transformation $ (t.\text{extend } f).\pi $. - The inverse map sends a natural transformation $ \pi \colon \text{const } J(W) \Rightarrow F $ to the unique morphism $ h.\text{lift } (\text{Cone.mk } W \pi) $ induced by the universal property of the limit cone $ t $.

CategoryTheory.Limits.IsLimit.homIso definition

(h : IsLimit t) (W : C) : ULift.{u₁} (W ⟶ t.pt : Type v₃) ≅ (const J).obj W ⟶ F

Full source

/-- The universal property of a limit cone: a map `W ⟶ X` is the same as
  a cone on `F` with cone point `W`. -/
def homIso (h : IsLimit t) (W : C) : ULiftULift.{u₁} (W ⟶ t.pt : Type v₃) ≅ (const J).obj W ⟶ F :=
  Equiv.toIso (Equiv.ulift.trans h.homEquiv)

Universal property isomorphism for limit cones

Informal description

Given a limit cone $ t $ for a functor $ F \colon J \to C $ and an object $ W $ in $ C $, the isomorphism `homIso h W` establishes a natural isomorphism between the lifted hom-set $ \text{ULift}(W \to t.\text{pt}) $ and the set of natural transformations from the constant functor at $ W $ to $ F $. This isomorphism is constructed by composing the lifting equivalence $ \text{ULift}(W \to t.\text{pt}) \simeq (W \to t.\text{pt}) $ with the universal property equivalence $ (W \to t.\text{pt}) \simeq (\text{const } J(W) \Rightarrow F) $ from `homEquiv`.

CategoryTheory.Limits.IsLimit.homIso_hom theorem

(h : IsLimit t) {W : C} (f : ULift.{u₁} (W ⟶ t.pt)) : (IsLimit.homIso h W).hom f = (t.extend f.down).π

Full source

@[simp]
theorem homIso_hom (h : IsLimit t) {W : C} (f : ULift.{u₁} (W ⟶ t.pt)) :
    (IsLimit.homIso h W).hom f = (t.extend f.down).π :=
  rfl

Forward map of universal property isomorphism for limit cones

Informal description

Given a limit cone $t$ for a functor $F \colon J \to C$ and an object $W$ in $C$, the forward map of the isomorphism $\text{homIso}\, h\, W$ applied to a lifted morphism $f \colon \text{ULift}(W \to t.\text{pt})$ equals the natural transformation $(t.\text{extend}\, f.\text{down}).\pi$ from the constant functor at $W$ to $F$.

CategoryTheory.Limits.IsLimit.natIso definition

(h : IsLimit t) : yoneda.obj t.pt ⋙ uliftFunctor.{u₁} ≅ F.cones

Full source

/-- The limit of `F` represents the functor taking `W` to
  the set of cones on `F` with cone point `W`. -/
def natIso (h : IsLimit t) : yonedayoneda.obj t.pt ⋙ uliftFunctor.{u₁}yoneda.obj t.pt ⋙ uliftFunctor.{u₁} ≅ F.cones :=
  NatIso.ofComponents fun W => IsLimit.homIso h (unop W)

Natural isomorphism for the universal property of a limit cone

Informal description

Given a limit cone $ t $ for a functor $ F \colon J \to C $, the natural isomorphism `natIso h` establishes an isomorphism between the functor $ \text{yoneda}(t.\text{pt}) \circ \text{uliftFunctor} $ and the functor of cones over $ F $. Here, $ \text{yoneda}(t.\text{pt}) $ is the Yoneda embedding applied to the apex of the cone $ t $, and $ \text{uliftFunctor} $ lifts types to a higher universe. This isomorphism expresses the universal property of the limit cone $ t $ in terms of natural transformations.

CategoryTheory.Limits.IsLimit.homIso' definition

 (h : IsLimit t) (W : C) :
  ULift.{u₁} (W ⟶ t.pt : Type v₃) ≅ { p : ∀ j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' }

Full source

/-- Another, more explicit, formulation of the universal property of a limit cone.
See also `homIso`. -/
def homIso' (h : IsLimit t) (W : C) :
    ULiftULift.{u₁} (W ⟶ t.pt : Type v₃) ≅
      { p : ∀ j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
  h.homIso W ≪≫
    { hom := fun π =>
        ⟨fun j => π.app j, fun f => by convert ← (π.naturality f).symm; apply id_comp⟩
      inv := fun p =>
        { app := fun j => p.1 j
          naturality := fun j j' f => by dsimp; rw [id_comp]; exact (p.2 f).symm } }

Universal property isomorphism for limit cones (explicit formulation)

Informal description

Given a limit cone $ t $ for a functor $ F \colon J \to C $ and an object $ W $ in $ C $, the isomorphism $\text{homIso}'\, h\, W$ establishes a natural bijection between the lifted hom-set $\text{ULift}(W \to t.\text{pt})$ and the set of cones over $ F $ with apex $ W $. More precisely, it maps a lifted morphism $ f \colon W \to t.\text{pt} $ to the cone whose components $ p_j \colon W \to F.obj\, j $ satisfy the compatibility condition $ p_j \circ F.map\, f = p_{j'} $ for every morphism $ f \colon j \to j' $ in $ J $. Conversely, it maps a compatible family of morphisms $ \{p_j\}_{j \in J} $ back to a morphism $ W \to t.\text{pt} $.

CategoryTheory.Limits.IsLimit.ofFaithful definition

 {t : Cone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [G.Faithful] (ht : IsLimit (mapCone G t))
  (lift : ∀ s : Cone F, s.pt ⟶ t.pt) (h : ∀ s, G.map (lift s) = ht.lift (mapCone G s)) : IsLimit t

Full source

/-- If G : C → D is a faithful functor which sends t to a limit cone,
  then it suffices to check that the induced maps for the image of t
  can be lifted to maps of C. -/
def ofFaithful {t : Cone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [G.Faithful]
    (ht : IsLimit (mapCone G t)) (lift : ∀ s : Cone F, s.pt ⟶ t.pt)
    (h : ∀ s, G.map (lift s) = ht.lift (mapCone G s)) : IsLimit t :=
  { lift
    fac := fun s j => by apply G.map_injective; rw [G.map_comp, h]; apply ht.fac
    uniq := fun s m w => by
      apply G.map_injective; rw [h]
      refine ht.uniq (mapCone G s) _ fun j => ?_
      convert ← congrArg (fun f => G.map f) (w j)
      apply G.map_comp }

Faithful functor criterion for limit cones

Informal description

Given a faithful functor $ G \colon C \to D $ that maps a cone $ t $ over $ F \colon J \to C $ to a limit cone in $ D $, then $ t $ is a limit cone in $ C $ if there exists a lifting of the induced maps from the image of $ t $ back to $ C $. Specifically, for every cone $ s $ over $ F $, there must exist a morphism $ \text{lift}(s) \colon s.pt \to t.pt $ in $ C $ such that $ G(\text{lift}(s)) $ equals the limit-induced morphism $ \text{ht.lift}(G(s)) $ in $ D $.

CategoryTheory.Limits.IsLimit.mapConeEquiv definition

 {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : Cone K} (t : IsLimit (mapCone F c)) :
  IsLimit (mapCone G c)

Full source

/-- If `F` and `G` are naturally isomorphic, then `F.mapCone c` being a limit implies
`G.mapCone c` is also a limit.
-/
def mapConeEquiv {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : Cone K}
    (t : IsLimit (mapCone F c)) : IsLimit (mapCone G c) := by
  apply postcomposeInvEquiv (isoWhiskerLeft K h :) (mapCone G c) _
  apply t.ofIsoLimit (postcomposeWhiskerLeftMapCone h.symm c).symm

Limit cone preservation under naturally isomorphic functors

Informal description

Given a natural isomorphism $h \colon F \cong G$ between functors $F, G \colon C \to D$, and a cone $c$ over a functor $K \colon J \to C$, if the image of $c$ under $F$ is a limit cone, then the image of $c$ under $G$ is also a limit cone. More precisely, if $\text{mapCone}\, F\, c$ is a limit cone, then $\text{mapCone}\, G\, c$ is also a limit cone. This result follows from the fact that the property of being a limit cone is preserved under postcomposition with the inverse of the natural isomorphism $h$ and the whiskering of $h$ with $K$.

CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism definition

{t : Cone F} : IsLimit t ≅ ∀ s, Unique (s ⟶ t)

Full source

/-- A cone is a limit cone exactly if
there is a unique cone morphism from any other cone.
-/
def isoUniqueConeMorphism {t : Cone F} : IsLimitIsLimit t ≅ ∀ s, Unique (s ⟶ t) where
  hom h s :=
    { default := h.liftConeMorphism s
      uniq := fun _ => h.uniq_cone_morphism }
  inv h :=
    { lift := fun s => (h s).default.hom
      uniq := fun s f w => congrArg ConeMorphism.hom ((h s).uniq ⟨f, w⟩) }

Limit cone characterization via unique cone morphisms

Informal description

A cone $ t $ over a functor $ F \colon J \to C $ is a limit cone if and only if for every other cone $ s $ over $ F $, there exists a unique morphism of cones from $ s $ to $ t $. This establishes an isomorphism between the property of being a limit cone and the property of having unique cone morphisms from any other cone.

CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom definition

{Y : C} (f : Y ⟶ X) : Cone F

Full source

/-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point
`Y`. -/
def coneOfHom {Y : C} (f : Y ⟶ X) : Cone F where
  pt := Y
  π := h.hom.app (op Y) ⟨f⟩

Cone construction from morphism via natural isomorphism

Informal description

Given a natural isomorphism `h` between the functor of cones over `F` and the representable functor at `X`, and a morphism `f : Y → X`, the function constructs a cone over `F` with apex `Y`. The projections of this cone are obtained by applying the natural isomorphism `h` to the morphism `f`.

CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone definition

(s : Cone F) : s.pt ⟶ X

Full source

/-- If `F.cones` is represented by `X`, each cone `s` gives a morphism `s.pt ⟶ X`. -/
def homOfCone (s : Cone F) : s.pt ⟶ X :=
  (h.inv.app (op s.pt) s.π).down

Morphism from cone apex to limit object via natural isomorphism

Informal description

Given a cone `s` over a functor `F`, the morphism `homOfCone s` from the apex `s.pt` of the cone to the object `X` is obtained by applying the inverse of the natural isomorphism `h` to the cone's natural transformation `s.π` and then projecting down to the underlying morphism.

CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone theorem

(s : Cone F) : coneOfHom h (homOfCone h s) = s

Full source

@[simp]
theorem coneOfHom_homOfCone (s : Cone F) : coneOfHom h (homOfCone h s) = s := by
  dsimp [coneOfHom, homOfCone]
  match s with
  | .mk s_pt s_π =>
    congr; dsimp
    convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_pt)) s_π using 1

Cone Reconstruction via Natural Isomorphism

Informal description

Given a cone $s$ over a functor $F$ and a natural isomorphism $h$ between the functor of cones over $F$ and the representable functor at $X$, the cone constructed from the morphism $\text{homOfCone}(s)$ is equal to $s$.

CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom theorem

{Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f

Full source

@[simp]
theorem homOfCone_coneOfHom {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f :=
  congrArg ULift.down (congrFun (congrFun (congrArg NatTrans.app h.hom_inv_id) (op Y)) ⟨f⟩ :)

Reconstruction of Morphism from Its Associated Cone via Natural Isomorphism

Informal description

Given a natural isomorphism $h$ between the functor of cones over $F$ and the representable functor at $X$, and a morphism $f \colon Y \to X$, the morphism obtained from the cone constructed via $f$ equals $f$ itself. In other words, $\text{homOfCone}_h(\text{coneOfHom}_h(f)) = f$.

CategoryTheory.Limits.IsLimit.OfNatIso.limitCone definition

: Cone F

Full source

/-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X`
will be a limit cone. -/
def limitCone : Cone F :=
  coneOfHom h (𝟙 X)

Limit cone via natural isomorphism

Informal description

Given a natural isomorphism `h` between the functor of cones over `F` and the representable functor at `X`, the limit cone is constructed as the cone corresponding to the identity morphism on `X` via this isomorphism. This cone serves as a universal cone for the functor `F`, meaning it satisfies the universal property of being a limit cone.

CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac theorem

{Y : C} (f : Y ⟶ X) : coneOfHom h f = (limitCone h).extend f

Full source

/-- If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is
the limit cone extended by `f`. -/
theorem coneOfHom_fac {Y : C} (f : Y ⟶ X) : coneOfHom h f = (limitCone h).extend f := by
  dsimp [coneOfHom, limitCone, Cone.extend]
  congr with j
  have t := congrFun (h.hom.naturality f.op) ⟨𝟙 X⟩
  dsimp at t
  simp only [comp_id] at t
  rw [congrFun (congrArg NatTrans.app t) j]
  rfl

Equality of Constructed Cone and Extended Limit Cone via Natural Isomorphism

Informal description

Given a natural isomorphism $h$ between the functor of cones over $F$ and the representable functor at $X$, and a morphism $f : Y \to X$, the cone constructed from $f$ via $h$ is equal to the extension of the limit cone along $f$.

CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac theorem

(s : Cone F) : (limitCone h).extend (homOfCone h s) = s

Full source

/-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
corresponding morphism. -/
theorem cone_fac (s : Cone F) : (limitCone h).extend (homOfCone h s) = s := by
  rw [← coneOfHom_homOfCone h s]
  conv_lhs => simp only [homOfCone_coneOfHom]
  apply (coneOfHom_fac _ _).symm

Factorization of Cone via Limit Cone Extension

Informal description

Given a cone $s$ over a functor $F$ and a natural isomorphism $h$ between the functor of cones over $F$ and the representable functor at $X$, the extension of the limit cone along the morphism $\text{homOfCone}_h(s)$ is equal to $s$. In other words, $(\text{limitCone}\, h).\text{extend}(\text{homOfCone}_h(s)) = s$.

CategoryTheory.Limits.IsLimit.ofNatIso definition

{X : C} (h : yoneda.obj X ⋙ uliftFunctor.{u₁} ≅ F.cones) : IsLimit (limitCone h)

Full source

/-- If `F.cones` is representable, then the cone corresponding to the identity morphism on
the representing object is a limit cone.
-/
def ofNatIso {X : C} (h : yonedayoneda.obj X ⋙ uliftFunctor.{u₁}yoneda.obj X ⋙ uliftFunctor.{u₁} ≅ F.cones) : IsLimit (limitCone h) where
  lift s := homOfCone h s
  fac s j := by
    have h := cone_fac h s
    cases s
    injection h with h₁ h₂
    simp only [heq_iff_eq] at h₂
    conv_rhs => rw [← h₂]
    rfl
  uniq s m w := by
    rw [← homOfCone_coneOfHom h m]
    congr
    rw [coneOfHom_fac]
    dsimp [Cone.extend]; cases s; congr with j; exact w j

Limit cone via natural isomorphism with representable functor

Informal description

Given a natural isomorphism $ h $ between the Yoneda embedding of an object $ X $ in category $ C $ (composed with the type lifting functor) and the functor of cones over $ F $, the cone corresponding to the identity morphism on $ X $ via $ h $ is a limit cone for the functor $ F $. More precisely, if $ h \colon \mathrm{Hom}(-, X) \circ \mathrm{ULift} \cong F.\mathrm{cones} $ is a natural isomorphism, then the cone $ \mathrm{limitCone}\, h $ constructed from $ h $ satisfies the universal property of a limit cone for $ F $. This means that for any other cone $ s $ over $ F $, there exists a unique morphism $ \mathrm{homOfCone}\, h\, s \colon s.\mathrm{pt} \to X $ that factors $ s $ through $ \mathrm{limitCone}\, h $.

CategoryTheory.Limits.IsColimit structure

(t : Cocone F)

Full source

/-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
cocone morphism from `t`. -/
@[stacks 002F]
structure IsColimit (t : Cocone F) where
  /-- `t.pt` maps to all other cocone covertices -/
  desc : ∀ s : Cocone F, t.pt ⟶ s.pt
  /-- The map `desc` makes the diagram with the natural transformations commute -/
  fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j := by aesop_cat
  /-- `desc` is the unique such map -/
  uniq :
    ∀ (s : Cocone F) (m : t.pt ⟶ s.pt) (_ : ∀ j : J, t.ι.app j ≫ m = s.ι.app j), m = desc s := by
    aesop_cat

Colimit cocone

Informal description

A cocone $ t $ on a functor $ F \colon J \to C $ is a colimit cocone if for every cocone $ s $ on $ F $, there exists a unique morphism of cocones from $ t $ to $ s $.

CategoryTheory.Limits.IsColimit.subsingleton instance

{t : Cocone F} : Subsingleton (IsColimit t)

Full source

instance subsingleton {t : Cocone F} : Subsingleton (IsColimit t) :=
  ⟨by intro P Q; cases P; cases Q; congr; aesop_cat⟩

Uniqueness of Colimit Cocone Proofs

Informal description

For any cocone $t$ of a functor $F \colon J \to C$, the type of proofs that $t$ is a colimit cocone is a subsingleton (i.e., any two such proofs are equal).

CategoryTheory.Limits.IsColimit.map definition

{F G : J ⥤ C} {s : Cocone F} (P : IsColimit s) (t : Cocone G) (α : F ⟶ G) : s.pt ⟶ t.pt

Full source

/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cocone point
of a colimit cocone over `F` to the cocone point of any cocone over `G`. -/
def map {F G : J ⥤ C} {s : Cocone F} (P : IsColimit s) (t : Cocone G) (α : F ⟶ G) : s.pt ⟶ t.pt :=
  P.desc ((Cocones.precompose α).obj t)

Morphism between colimit cocones induced by a natural transformation

Informal description

Given a natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon J \to C$, and a colimit cocone $s$ of $F$, the function `IsColimit.map` constructs a morphism from the vertex of $s$ to the vertex of any cocone $t$ over $G$.

CategoryTheory.Limits.IsColimit.ι_map theorem

 {F G : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) :
  c.ι.app j ≫ IsColimit.map hc d α = α.app j ≫ d.ι.app j

Full source

@[reassoc (attr := simp)]
theorem ι_map {F G : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) :
    c.ι.app j ≫ IsColimit.map hc d α = α.app j ≫ d.ι.app j :=
  fac _ _ _

Naturality of Colimit Cocone Morphism Induced by a Natural Transformation

Informal description

Let $F, G \colon J \to C$ be functors, $c$ a colimit cocone for $F$, and $d$ a cocone for $G$. Given a natural transformation $\alpha \colon F \Rightarrow G$ and an object $j \in J$, the diagram \[ c.\iota_j \circ \text{IsColimit.map } hc\ d\ \alpha = \alpha_j \circ d.\iota_j \] commutes, where $c.\iota_j$ and $d.\iota_j$ are the cocone morphisms for $j$, and $\text{IsColimit.map } hc\ d\ \alpha$ is the induced morphism between the vertices of $c$ and $d$.

CategoryTheory.Limits.IsColimit.desc_self theorem

{t : Cocone F} (h : IsColimit t) : h.desc t = 𝟙 t.pt

Full source

@[simp]
theorem desc_self {t : Cocone F} (h : IsColimit t) : h.desc t = 𝟙 t.pt :=
  (h.uniq _ _ fun _ => comp_id _).symm

Identity Morphism is the Descent from a Colimit Cocone to Itself

Informal description

For any colimit cocone $ t $ of a functor $ F \colon J \to C $, the morphism $ h.desc\ t $ induced by the colimit property $ h $ is equal to the identity morphism on the vertex $ t.pt $ of the cocone. In other words, the unique morphism from the colimit cocone to itself is the identity morphism.

CategoryTheory.Limits.IsColimit.descCoconeMorphism definition

{t : Cocone F} (h : IsColimit t) (s : Cocone F) : t ⟶ s

Full source

/-- The universal morphism from a colimit cocone to any other cocone. -/
@[simps]
def descCoconeMorphism {t : Cocone F} (h : IsColimit t) (s : Cocone F) : t ⟶ s where hom := h.desc s

Universal cocone morphism from a colimit cocone

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and another cocone $ s $ for $ F $, this defines the unique morphism of cocones from $ t $ to $ s $.

CategoryTheory.Limits.IsColimit.uniq_cocone_morphism theorem

{s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f'

Full source

theorem uniq_cocone_morphism {s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f' :=
  have : ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s := by
    intro g; ext; exact h.uniq _ _ g.w
  this.trans this.symm

Uniqueness of Cocone Morphism from Colimit Cocone

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and another cocone $ s $ for $ F $, any two morphisms of cocones $ f, f' \colon t \to s $ are equal.

CategoryTheory.Limits.IsColimit.existsUnique theorem

{t : Cocone F} (h : IsColimit t) (s : Cocone F) : ∃! d : t.pt ⟶ s.pt, ∀ j, t.ι.app j ≫ d = s.ι.app j

Full source

/-- Restating the definition of a colimit cocone in terms of the ∃! operator. -/
theorem existsUnique {t : Cocone F} (h : IsColimit t) (s : Cocone F) :
    ∃! d : t.pt ⟶ s.pt, ∀ j, t.ι.app j ≫ d = s.ι.app j :=
  ⟨h.desc s, h.fac s, h.uniq s⟩

Unique Factorization Property of Colimit Cocones

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and another cocone $ s $ for $ F $, there exists a unique morphism $ d \colon t.\mathrm{pt} \to s.\mathrm{pt} $ such that for every object $ j $ in $ J $, the composition $ t.\iota.\mathrm{app}\,j \circ d $ equals $ s.\iota.\mathrm{app}\,j $.

CategoryTheory.Limits.IsColimit.ofExistsUnique definition

{t : Cocone F} (ht : ∀ s : Cocone F, ∃! d : t.pt ⟶ s.pt, ∀ j, t.ι.app j ≫ d = s.ι.app j) : IsColimit t

Full source

/-- Noncomputably make a colimit cocone from the existence of unique factorizations. -/
def ofExistsUnique {t : Cocone F}
    (ht : ∀ s : Cocone F, ∃! d : t.pt ⟶ s.pt, ∀ j, t.ι.app j ≫ d = s.ι.app j) : IsColimit t := by
  choose s hs hs' using ht
  exact ⟨s, hs, hs'⟩

Characterization of colimit cocone via unique factorization

Informal description

Given a cocone $ t $ on a functor $ F \colon J \to C $, if for every cocone $ s $ on $ F $ there exists a unique morphism $ d \colon t.\mathrm{pt} \to s.\mathrm{pt} $ such that for all $ j $, the composition $ t.\iota.\mathrm{app}\,j \circ d $ equals $ s.\iota.\mathrm{app}\,j $, then $ t $ is a colimit cocone.

CategoryTheory.Limits.IsColimit.mkCoconeMorphism definition

{t : Cocone F} (desc : ∀ s : Cocone F, t ⟶ s) (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) : IsColimit t

Full source

/-- Alternative constructor for `IsColimit`,
providing a morphism of cocones rather than a morphism between the cocone points
and separately the factorisation condition.
-/
@[simps]
def mkCoconeMorphism {t : Cocone F} (desc : ∀ s : Cocone F, t ⟶ s)
    (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) : IsColimit t where
  desc s := (desc s).hom
  uniq s m w :=
    have : CoconeMorphism.mk m w = desc s := by apply uniq'
    congrArg CoconeMorphism.hom this

Alternative construction of colimit cocone via cocone morphisms

Informal description

Given a cocone $ t $ on a functor $ F \colon J \to C $, if there exists a function that assigns to every cocone $ s $ on $ F $ a morphism of cocones from $ t $ to $ s $, and this assignment is unique (i.e., any other morphism of cocones from $ t $ to $ s $ must equal this assigned morphism), then $ t $ is a colimit cocone.

CategoryTheory.Limits.IsColimit.uniqueUpToIso definition

{s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s ≅ t

Full source

/-- Colimit cocones on `F` are unique up to isomorphism. -/
@[simps]
def uniqueUpToIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s ≅ t where
  hom := P.descCoconeMorphism t
  inv := Q.descCoconeMorphism s
  hom_inv_id := P.uniq_cocone_morphism
  inv_hom_id := Q.uniq_cocone_morphism

Uniqueness of colimit cocones up to isomorphism

Informal description

Given two colimit cocones $ s $ and $ t $ for a functor $ F \colon J \to C $, there exists a unique isomorphism between $ s $ and $ t $ in the category of cocones over $ F $. This isomorphism is constructed using the universal property of colimit cocones, with its inverse similarly defined by swapping the roles of $ s $ and $ t $.

CategoryTheory.Limits.IsColimit.hom_isIso theorem

{s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t) : IsIso f

Full source

/-- Any cocone morphism between colimit cocones is an isomorphism. -/
theorem hom_isIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t) : IsIso f :=
  ⟨⟨Q.descCoconeMorphism s, ⟨P.uniq_cocone_morphism, Q.uniq_cocone_morphism⟩⟩⟩

Cocone Morphism Between Colimit Cocones is an Isomorphism

Informal description

Given two colimit cocones $s$ and $t$ for a functor $F \colon J \to C$ and a cocone morphism $f \colon s \to t$, the morphism $f$ is an isomorphism.

CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso definition

{s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s.pt ≅ t.pt

Full source

/-- Colimits of `F` are unique up to isomorphism. -/
def coconePointUniqueUpToIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s.pt ≅ t.pt :=
  (Cocones.forget F).mapIso (uniqueUpToIso P Q)

Unique isomorphism between apexes of colimit cocones

Informal description

Given two colimit cocones $ s $ and $ t $ for a functor $ F \colon J \to C $, there exists a unique isomorphism between their apex objects $ s.pt $ and $ t.pt $ in the category $ C $. This isomorphism is induced by the universal property of colimit cocones.

CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom theorem

 {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) :
  s.ι.app j ≫ (coconePointUniqueUpToIso P Q).hom = t.ι.app j

Full source

@[reassoc (attr := simp)]
theorem comp_coconePointUniqueUpToIso_hom {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t)
    (j : J) : s.ι.app j ≫ (coconePointUniqueUpToIso P Q).hom = t.ι.app j :=
  (uniqueUpToIso P Q).hom.w _

Compatibility of cocone morphisms with the unique isomorphism between colimit cocones

Informal description

Let $F \colon J \to C$ be a functor, and let $s$ and $t$ be colimit cocones for $F$ with corresponding colimit properties $P$ and $Q$. For any object $j$ in the indexing category $J$, the composition of the cocone morphism $s.\iota_j$ (from $F(j)$ to the apex $s.pt$) with the unique isomorphism $(s.pt \cong t.pt)$ (induced by the universal property of colimits) equals the cocone morphism $t.\iota_j$ (from $F(j)$ to the apex $t.pt$). In symbols: $$ s.\iota_j \circ (s.pt \cong t.pt).\text{hom} = t.\iota_j. $$

CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv theorem

 {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) :
  t.ι.app j ≫ (coconePointUniqueUpToIso P Q).inv = s.ι.app j

Full source

@[reassoc (attr := simp)]
theorem comp_coconePointUniqueUpToIso_inv {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t)
    (j : J) : t.ι.app j ≫ (coconePointUniqueUpToIso P Q).inv = s.ι.app j :=
  (uniqueUpToIso P Q).inv.w _

Compatibility of cocone morphisms with inverse apex isomorphism

Informal description

For any two colimit cocones $s$ and $t$ of a functor $F \colon J \to C$, with $P$ and $Q$ being proofs that $s$ and $t$ are colimit cocones respectively, and for any object $j$ in $J$, the composition of the cocone morphism $t.\iota_j$ with the inverse of the unique isomorphism between the apexes of $s$ and $t$ equals the cocone morphism $s.\iota_j$. In symbols: $$ t.\iota_j \circ (\text{coconePointUniqueUpToIso}\, P\, Q)^{-1} = s.\iota_j. $$

CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc theorem

{r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : (coconePointUniqueUpToIso P Q).hom ≫ Q.desc r = P.desc r

Full source

@[reassoc (attr := simp)]
theorem coconePointUniqueUpToIso_hom_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
    (coconePointUniqueUpToIso P Q).hom ≫ Q.desc r = P.desc r :=
  P.uniq _ _ (by simp)

Compatibility of colimit-induced morphisms with apex isomorphism

Informal description

Let $F \colon J \to C$ be a functor, and let $r$, $s$, and $t$ be cocones for $F$ with $P$ and $Q$ being proofs that $s$ and $t$ are colimit cocones, respectively. Then the composition of the unique isomorphism $(s.pt \cong t.pt)$ (induced by the universal property of colimits) with the colimit-induced morphism $Q.desc\, r$ (from $t.pt$ to $r.pt$) equals the colimit-induced morphism $P.desc\, r$ (from $s.pt$ to $r.pt$). In symbols: $$ (s.pt \cong t.pt).\text{hom} \circ Q.desc\, r = P.desc\, r. $$

CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc theorem

{r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : (coconePointUniqueUpToIso P Q).inv ≫ P.desc r = Q.desc r

Full source

@[reassoc (attr := simp)]
theorem coconePointUniqueUpToIso_inv_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
    (coconePointUniqueUpToIso P Q).inv ≫ P.desc r = Q.desc r :=
  Q.uniq _ _ (by simp)

Compatibility of descending morphisms with inverse apex isomorphism for colimits

Informal description

Given three cocones $r$, $s$, and $t$ over a functor $F \colon J \to C$, where $s$ and $t$ are colimit cocones (with proofs $P$ and $Q$ respectively), the composition of the inverse of the unique isomorphism between the apexes of $s$ and $t$ with the descending morphism from $s$ to $r$ equals the descending morphism from $t$ to $r$. In symbols: $$ (\text{coconePointUniqueUpToIso}\, P\, Q)^{-1} \circ P.\text{desc}\, r = Q.\text{desc}\, r. $$

CategoryTheory.Limits.IsColimit.ofIsoColimit definition

{r t : Cocone F} (P : IsColimit r) (i : r ≅ t) : IsColimit t

Full source

/-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/
def ofIsoColimit {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) : IsColimit t :=
  IsColimit.mkCoconeMorphism (fun s => i.inv ≫ P.descCoconeMorphism s) fun s m => by
    rw [i.eq_inv_comp]; apply P.uniq_cocone_morphism

Colimit cocone property preserved under isomorphism

Informal description

Given a cocone $ r $ that is a colimit cocone for a functor $ F \colon J \to C $, and an isomorphism $ i \colon r \cong t $ of cocones, then $ t $ is also a colimit cocone for $ F $. This transports the colimit property across an isomorphism of cocones.

CategoryTheory.Limits.IsColimit.ofIsoColimit_desc theorem

{r t : Cocone F} (P : IsColimit r) (i : r ≅ t) (s) : (P.ofIsoColimit i).desc s = i.inv.hom ≫ P.desc s

Full source

@[simp]
theorem ofIsoColimit_desc {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) (s) :
    (P.ofIsoColimit i).desc s = i.inv.hom ≫ P.desc s :=
  rfl

Descending Morphism Formula for Isomorphic Colimit Cocones

Informal description

Let $F \colon J \to C$ be a functor, and let $r$ and $t$ be cocones over $F$ with $r$ being a colimit cocone. Given an isomorphism $i \colon r \cong t$ of cocones, the descending morphism $(P.\text{ofIsoColimit}~i).\text{desc}~s$ from the colimit cocone $t$ to any other cocone $s$ is equal to the composition $i^{-1} \circ P.\text{desc}~s$, where $P.\text{desc}~s$ is the descending morphism from $r$ to $s$.

CategoryTheory.Limits.IsColimit.equivIsoColimit definition

{r t : Cocone F} (i : r ≅ t) : IsColimit r ≃ IsColimit t

Full source

/-- Isomorphism of cocones preserves whether or not they are colimiting cocones. -/
def equivIsoColimit {r t : Cocone F} (i : r ≅ t) : IsColimitIsColimit r ≃ IsColimit t where
  toFun h := h.ofIsoColimit i
  invFun h := h.ofIsoColimit i.symm
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of colimit properties under cocone isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cocones $r$ and $t$ for a functor $F \colon J \to C$, there is an equivalence between the property of $r$ being a colimit cocone and the property of $t$ being a colimit cocone. This equivalence is given by transporting the colimit property along the isomorphism $i$ and its inverse.

CategoryTheory.Limits.IsColimit.equivIsoColimit_apply theorem

{r t : Cocone F} (i : r ≅ t) (P : IsColimit r) : equivIsoColimit i P = P.ofIsoColimit i

Full source

@[simp]
theorem equivIsoColimit_apply {r t : Cocone F} (i : r ≅ t) (P : IsColimit r) :
    equivIsoColimit i P = P.ofIsoColimit i :=
  rfl

Equivalence Application for Colimit Cocone Isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cocones $r$ and $t$ for a functor $F \colon J \to C$, and given that $r$ is a colimit cocone (witnessed by $P$), the application of the equivalence `equivIsoColimit i` to $P$ yields the same result as transporting the colimit property along $i$ via `P.ofIsoColimit i`.

CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply theorem

{r t : Cocone F} (i : r ≅ t) (P : IsColimit t) : (equivIsoColimit i).symm P = P.ofIsoColimit i.symm

Full source

@[simp]
theorem equivIsoColimit_symm_apply {r t : Cocone F} (i : r ≅ t) (P : IsColimit t) :
    (equivIsoColimit i).symm P = P.ofIsoColimit i.symm :=
  rfl

Inverse Equivalence of Colimit Properties under Cocone Isomorphism

Informal description

Given an isomorphism $i \colon r \cong t$ between two cocones $r$ and $t$ for a functor $F \colon J \to C$, and given that $t$ is a colimit cocone, the inverse of the equivalence `equivIsoColimit i` applied to $P$ (the proof that $t$ is a colimit) equals the proof that $r$ is a colimit obtained by transporting $P$ along the inverse isomorphism $i^{-1} \colon t \cong r$.

CategoryTheory.Limits.IsColimit.ofPointIso definition

{r t : Cocone F} (P : IsColimit r) [i : IsIso (P.desc t)] : IsColimit t

Full source

/-- If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the
first cocone was colimiting also.
-/
def ofPointIso {r t : Cocone F} (P : IsColimit r) [i : IsIso (P.desc t)] : IsColimit t :=
  ofIsoColimit P (by
    haveI : IsIso (P.descCoconeMorphism t).hom := i
    haveI : IsIso (P.descCoconeMorphism t) := Cocones.cocone_iso_of_hom_iso _
    apply asIso (P.descCoconeMorphism t))

Colimit cocone via isomorphism of descent morphism

Informal description

Given a cocone $ r $ that is a colimit cocone for a functor $ F \colon J \to C $, and another cocone $ t $ for $ F $, if the canonical morphism $ P.desc t $ from the colimit object of $ r $ to the apex of $ t $ is an isomorphism, then $ t $ is also a colimit cocone for $ F $.

CategoryTheory.Limits.IsColimit.hom_desc theorem

 (h : IsColimit t) {W : C} (m : t.pt ⟶ W) :
  m =
    h.desc
      { pt := W
        ι := { app := fun b => t.ι.app b ≫ m } }

Full source

theorem hom_desc (h : IsColimit t) {W : C} (m : t.pt ⟶ W) :
    m =
      h.desc
        { pt := W
          ι := { app := fun b => t.ι.app b ≫ m } } :=
  h.uniq
    { pt := W
      ι := { app := fun b => t.ι.app b ≫ m } }
    m fun _ => rfl

Universal Property of Colimit: Morphism Factorization

Informal description

Let $t$ be a colimit cocone for a functor $F \colon J \to C$, and let $h$ be a proof that $t$ is indeed a colimit. For any object $W$ in $C$ and any morphism $m \colon t.\mathrm{pt} \to W$, the morphism $m$ is equal to the unique morphism induced by the universal property of the colimit, applied to the cocone with apex $W$ whose morphisms are given by composing the cocone morphisms of $t$ with $m$.

CategoryTheory.Limits.IsColimit.hom_ext theorem

(h : IsColimit t) {W : C} {f f' : t.pt ⟶ W} (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f'

Full source

/-- Two morphisms out of a colimit are equal if their compositions with
  each cocone morphism are equal. -/
theorem hom_ext (h : IsColimit t) {W : C} {f f' : t.pt ⟶ W}
    (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f' := by
  rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w

Uniqueness of Morphisms from Colimit via Commuting Diagrams

Informal description

Let $t$ be a colimit cocone for a functor $F \colon J \to C$, and let $h$ be a proof that $t$ is indeed a colimit. For any object $W$ in $C$ and any pair of morphisms $f, f' \colon t.\mathrm{pt} \to W$, if for every object $j$ in $J$ the compositions $t.\iota_j \circ f$ and $t.\iota_j \circ f'$ are equal, then $f = f'$.

CategoryTheory.Limits.IsColimit.ofLeftAdjoint definition

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} {left : Cocone G ⥤ Cocone F} {right : Cocone F ⥤ Cocone G}
  (adj : left ⊣ right) {c : Cocone G} (t : IsColimit c) : IsColimit (left.obj c)

Full source

/-- Given a left adjoint functor between categories of cocones,
the image of a colimit cocone is a colimit cocone.
-/
def ofLeftAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} {left : CoconeCocone G ⥤ Cocone F}
    {right : CoconeCocone F ⥤ Cocone G} (adj : left ⊣ right) {c : Cocone G} (t : IsColimit c) :
    IsColimit (left.obj c) :=
  mkCoconeMorphism
    (fun s => (adj.homEquiv c s).symm (t.descCoconeMorphism _)) fun _ _ =>
    (Adjunction.homEquiv_apply_eq _ _ _).1 t.uniq_cocone_morphism

Colimit cocone under left adjoint functor

Informal description

Given a left adjoint functor `left` between categories of cocones, if `c` is a colimit cocone for a functor `G : K ⥤ D`, then the image of `c` under `left` is a colimit cocone for the corresponding functor `F : J ⥤ C`.

CategoryTheory.Limits.IsColimit.ofCoconeEquiv definition

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F) {c : Cocone G} :
  IsColimit (h.functor.obj c) ≃ IsColimit c

Full source

/-- Given two functors which have equivalent categories of cocones,
we can transport a colimiting cocone across the equivalence.
-/
def ofCoconeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : CoconeCocone G ≌ Cocone F)
    {c : Cocone G} : IsColimitIsColimit (h.functor.obj c) ≃ IsColimit c where
  toFun P := ofIsoColimit (ofLeftAdjoint h.symm.toAdjunction P) (h.unitIso.symm.app c)
  invFun := ofLeftAdjoint h.toAdjunction
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of colimit properties under cocone category equivalence

Informal description

Given an equivalence of categories $h \colon \text{Cocone}(G) \simeq \text{Cocone}(F)$ between the categories of cocones for functors $G \colon K \to D$ and $F \colon J \to C$, and a cocone $c$ for $G$, there is an equivalence between: 1. The property that $h.\text{functor}(c)$ is a colimit cocone for $F$ 2. The property that $c$ is a colimit cocone for $G$ This equivalence transports the colimit property across the equivalence of cocone categories.

CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc theorem

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit (h.functor.obj c))
  (s) :
  (ofCoconeEquiv h P).desc s =
    (h.unit.app c).hom ≫ (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom ≫ (h.unitInv.app s).hom

Full source

@[simp]
theorem ofCoconeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
    (h : CoconeCocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit (h.functor.obj c)) (s) :
    (ofCoconeEquiv h P).desc s =
      (h.unit.app c).hom ≫
        (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom ≫ (h.unitInv.app s).hom :=
  rfl

Descent Morphism Formula under Cocone Category Equivalence

Informal description

Given an equivalence of categories $h \colon \text{Cocone}(G) \simeq \text{Cocone}(F)$ between the categories of cocones for functors $G \colon K \to D$ and $F \colon J \to C$, a cocone $c$ for $G$, and a proof $P$ that $h.\text{functor}(c)$ is a colimit cocone for $F$, the descent morphism for any cocone $s$ under the equivalence is given by the composition: $$(h.\text{unit}.c).\text{hom} \circ (h.\text{inverse}.(P.\text{descCoconeMorphism}(h.\text{functor}(s)))).\text{hom} \circ (h.\text{unitInv}.s).\text{hom}$$

CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc theorem

 {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit c) (s) :
  ((ofCoconeEquiv h).symm P).desc s =
    (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom ≫ (h.counit.app s).hom

Full source

@[simp]
theorem ofCoconeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
    (h : CoconeCocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit c) (s) :
    ((ofCoconeEquiv h).symm P).desc s =
      (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom ≫ (h.counit.app s).hom :=
  rfl

Description of Colimit Cocone under Inverse Equivalence of Cocone Categories

Informal description

Given an equivalence of categories $h \colon \text{Cocone}(G) \simeq \text{Cocone}(F)$ between the categories of cocones for functors $G \colon K \to D$ and $F \colon J \to C$, and a cocone $c$ for $G$ that is a colimit cocone, the description of the colimit cocone property under the inverse equivalence $h^{-1}$ is given by: \[ (h^{-1}(P)).\text{desc}(s) = h.\text{functor}(P.\text{descCoconeMorphism}(h^{-1}(s))) \circ h.\text{counit}(s) \] where: - $P$ is the proof that $c$ is a colimit cocone for $G$, - $s$ is any cocone in $\text{Cocone}(F)$, - $\text{desc}$ denotes the universal property morphism from the colimit cocone, - $\text{counit}$ is the counit natural transformation of the equivalence $h$.

CategoryTheory.Limits.IsColimit.precomposeHomEquiv definition

{F G : J ⥤ C} (α : F ≅ G) (c : Cocone G) : IsColimit ((Cocones.precompose α.hom).obj c) ≃ IsColimit c

Full source

/-- A cocone precomposed with a natural isomorphism is a colimit cocone
if and only if the original cocone is.
-/
def precomposeHomEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cocone G) :
    IsColimitIsColimit ((Cocones.precompose α.hom).obj c) ≃ IsColimit c :=
  ofCoconeEquiv (Cocones.precomposeEquivalence α)

Equivalence of colimit properties under precomposition with natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$ and a cocone $c$ for $G$, there is an equivalence between: 1. The property that the cocone obtained by precomposing $c$ with $\alpha.\text{hom}$ is a colimit cocone for $F$ 2. The property that $c$ itself is a colimit cocone for $G$ This equivalence holds because precomposition with a natural isomorphism induces an equivalence of cocone categories.

CategoryTheory.Limits.IsColimit.precomposeInvEquiv definition

{F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) : IsColimit ((Cocones.precompose α.inv).obj c) ≃ IsColimit c

Full source

/-- A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone
if and only if the original cocone is.
-/
def precomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) :
    IsColimitIsColimit ((Cocones.precompose α.inv).obj c) ≃ IsColimit c :=
  precomposeHomEquiv α.symm c

Equivalence of colimit properties under precomposition with inverse natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$ and a cocone $c$ for $F$, there is an equivalence between: 1. The property that the cocone obtained by precomposing $c$ with $\alpha^{-1}$ is a colimit cocone for $G$ 2. The property that $c$ itself is a colimit cocone for $F$ This equivalence holds because precomposition with the inverse of a natural isomorphism induces an equivalence of cocone categories.

CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso definition

 {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) (d : Cocone G) (w : (Cocones.precompose α.inv).obj c ≅ d) :
  IsColimit c ≃ IsColimit d

Full source

/-- Constructing an equivalence `is_colimit c ≃ is_colimit d` from a natural isomorphism
between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
-/
def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) (d : Cocone G)
    (w : (Cocones.precompose α.inv).obj c ≅ d) : IsColimitIsColimit c ≃ IsColimit d :=
  (precomposeInvEquiv α _).symm.trans (equivIsoColimit w)

Equivalence of colimit properties under natural isomorphism and cocone isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$, a cocone $c$ for $F$, a cocone $d$ for $G$, and an isomorphism $w \colon (Cocones.precompose \alpha^{-1}).obj c \cong d$ between the precomposed cocone and $d$, there is an equivalence between: 1. The property that $c$ is a colimit cocone for $F$ 2. The property that $d$ is a colimit cocone for $G$ This equivalence is constructed by combining the equivalence from precomposing with $\alpha^{-1}$ and the equivalence induced by the cocone isomorphism $w$.

CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso definition

{F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) : s.pt ≅ t.pt

Full source

/-- The cocone points of two colimit cocones for naturally isomorphic functors
are themselves isomorphic.
-/
@[simps]
def coconePointsIsoOfNatIso {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s)
    (Q : IsColimit t) (w : F ≅ G) : s.pt ≅ t.pt where
  hom := P.map t w.hom
  inv := Q.map s w.inv
  hom_inv_id := P.hom_ext (by simp)
  inv_hom_id := Q.hom_ext (by simp)

Isomorphism between colimit cocone vertices induced by a natural isomorphism of functors

Informal description

Given two functors $ F, G \colon J \to C $ that are naturally isomorphic via $ w \colon F \cong G $, and two colimit cocones $ s $ for $ F $ and $ t $ for $ G $, the vertices $ s.\mathrm{pt} $ and $ t.\mathrm{pt} $ are isomorphic in the category $ C $. The isomorphism is constructed using the universal properties of the colimit cocones $ s $ and $ t $, with the morphisms induced by the natural isomorphism $ w $.

CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom theorem

 {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
  s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).hom = w.hom.app j ≫ t.ι.app j

Full source

@[reassoc]
theorem comp_coconePointsIsoOfNatIso_hom {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
    s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).hom = w.hom.app j ≫ t.ι.app j := by simp

Naturality of the isomorphism between colimit cocones

Informal description

Given functors $F, G \colon J \to C$, colimit cocones $s$ for $F$ and $t$ for $G$, and a natural isomorphism $w \colon F \cong G$, for any object $j \in J$, the diagram \[ s.\iota_j \circ \varphi = w_j \circ t.\iota_j \] commutes, where $\varphi \colon s.\mathrm{pt} \cong t.\mathrm{pt}$ is the isomorphism induced by $w$ via the universal properties of $s$ and $t$, and $\iota_j$ denotes the cocone morphisms.

CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv theorem

 {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
  t.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).inv = w.inv.app j ≫ s.ι.app j

Full source

@[reassoc]
theorem comp_coconePointsIsoOfNatIso_inv {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
    t.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).inv = w.inv.app j ≫ s.ι.app j := by simp

Naturality of the inverse isomorphism between colimit cocones

Informal description

Given functors $F, G \colon J \to C$, colimit cocones $s$ for $F$ and $t$ for $G$, and a natural isomorphism $w \colon F \cong G$, for any object $j \in J$, the diagram \[ t.\iota_j \circ \varphi^{-1} = w^{-1}_j \circ s.\iota_j \] commutes, where $\varphi \colon s.\mathrm{pt} \cong t.\mathrm{pt}$ is the isomorphism induced by $w$ via the universal properties of $s$ and $t$, and $\iota_j$ denotes the cocone morphisms.

CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc theorem

 {F G : J ⥤ C} {s : Cocone F} {r t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) :
  (coconePointsIsoOfNatIso P Q w).hom ≫ Q.desc r = P.map _ w.hom

Full source

@[reassoc]
theorem coconePointsIsoOfNatIso_hom_desc {F G : J ⥤ C} {s : Cocone F} {r t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) :
    (coconePointsIsoOfNatIso P Q w).hom ≫ Q.desc r = P.map _ w.hom :=
  P.hom_ext (by simp)

Compatibility of Colimit Isomorphism with Descending Morphisms via Natural Isomorphism

Informal description

Given functors $F, G \colon J \to C$, a colimit cocone $s$ for $F$ with proof $P$ that it is a colimit, a colimit cocone $t$ for $G$ with proof $Q$, and a natural isomorphism $w \colon F \cong G$, the composition of the isomorphism $\varphi \colon s.\mathrm{pt} \cong t.\mathrm{pt}$ (induced by $w$) with the colimit morphism $Q.\mathrm{desc}\ r$ equals the morphism $P.\mathrm{map}\ r\ w.\mathrm{hom}$ induced by $w.\mathrm{hom}$.

CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc theorem

 {F G : J ⥤ C} {s : Cocone G} {r t : Cocone F} (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) :
  (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map _ w.inv

Full source

@[reassoc]
theorem coconePointsIsoOfNatIso_inv_desc {F G : J ⥤ C} {s : Cocone G} {r t : Cocone F}
    (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) :
    (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map _ w.inv :=
  Q.hom_ext (by simp)

Compatibility of Inverse Isomorphism with Colimit Descriptions via Natural Isomorphism

Informal description

Given functors $F, G \colon J \to C$, colimit cocones $t$ for $F$ and $s$ for $G$, and a natural isomorphism $w \colon F \cong G$, the composition of the inverse isomorphism $\varphi^{-1} \colon t.\mathrm{pt} \to s.\mathrm{pt}$ (induced by $w$) with the universal morphism $P.\mathrm{desc}\ r$ equals the morphism $Q.\mathrm{map}\ r\ w^{-1}$, where $r$ is any cocone over $F$.

CategoryTheory.Limits.IsColimit.whiskerEquivalence definition

{s : Cocone F} (P : IsColimit s) (e : K ≌ J) : IsColimit (s.whisker e.functor)

Full source

/-- If `s : Cocone F` is a colimit cocone, so is `s` whiskered by an equivalence `e`.
-/
def whiskerEquivalence {s : Cocone F} (P : IsColimit s) (e : K ≌ J) :
    IsColimit (s.whisker e.functor) :=
  ofLeftAdjoint (Cocones.whiskeringEquivalence e).toAdjunction P

Colimit cocone under whiskering by equivalence

Informal description

Given a colimit cocone $ s $ for a functor $ F \colon J \to C $ and an equivalence of categories $ e \colon K \simeq J $, the whiskered cocone $ s \circ e $ is also a colimit cocone for the functor $ F \circ e \colon K \to C $.

CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence definition

{s : Cocone F} (e : K ≌ J) (P : IsColimit (s.whisker e.functor)) : IsColimit s

Full source

/-- If `s : Cocone F` whiskered by an equivalence `e` is a colimit cocone, so is `s`.
-/
def ofWhiskerEquivalence {s : Cocone F} (e : K ≌ J) (P : IsColimit (s.whisker e.functor)) :
    IsColimit s :=
  equivIsoColimit ((Cocones.whiskeringEquivalence e).unitIso.app s).symm
    (ofLeftAdjoint (Cocones.whiskeringEquivalence e).symm.toAdjunction P)

Colimit cocone property preserved under whiskering equivalence

Informal description

Given a cocone $ s $ over a functor $ F \colon J \to C $, an equivalence of categories $ e \colon K \simeq J $, and a proof that the whiskered cocone $ s \circ e $ is a colimit cocone for $ F \circ e $, then $ s $ itself is a colimit cocone for $ F $.

CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv definition

{s : Cocone F} (e : K ≌ J) : IsColimit s ≃ IsColimit (s.whisker e.functor)

Full source

/-- Given an equivalence of diagrams `e`, `s` is a colimit cocone iff `s.whisker e.functor` is.
-/
def whiskerEquivalenceEquiv {s : Cocone F} (e : K ≌ J) :
    IsColimitIsColimit s ≃ IsColimit (s.whisker e.functor) :=
  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by aesop_cat, by aesop_cat⟩

Equivalence of colimit properties under whiskering by category equivalence

Informal description

Given a cocone $ s $ over a functor $ F \colon J \to C $ and an equivalence of categories $ e \colon K \simeq J $, there is a natural equivalence between the property of $ s $ being a colimit cocone for $ F $ and the property of the whiskered cocone $ s \circ e $ being a colimit cocone for $ F \circ e $.

CategoryTheory.Limits.IsColimit.extendIso definition

{s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit s) : IsColimit (s.extend i)

Full source

/-- A colimit cocone extended by an isomorphism is a colimit cocone. -/
def extendIso {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit s) :
    IsColimit (s.extend i) :=
  IsColimit.ofIsoColimit hs (Cocones.extendIso s (asIso i))

Colimit cocone extended by an isomorphism is a colimit cocone

Informal description

Given a cocone $ s $ over a functor $ F \colon J \to C $, a morphism $ i \colon s.\mathrm{pt} \to X $ that is an isomorphism, and a proof $ hs $ that $ s $ is a colimit cocone, then the extended cocone $ s.\mathrm{extend}\, i $ is also a colimit cocone.

CategoryTheory.Limits.IsColimit.ofExtendIso definition

{s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit (s.extend i)) : IsColimit s

Full source

/-- A cocone is a colimit cocone if its extension by an isomorphism is. -/
def ofExtendIso {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit (s.extend i)) :
    IsColimit s :=
  IsColimit.ofIsoColimit hs (Cocones.extendIso s (asIso i)).symm

Colimit cocone property from extended isomorphism

Informal description

Given a cocone $ s $ for a functor $ F \colon J \to C $, a morphism $ i \colon s.\mathrm{pt} \to X $ that is an isomorphism, and the assumption that the extended cocone $ s.\mathrm{extend}\, i $ is a colimit cocone, then $ s $ itself is a colimit cocone for $ F $. This is established by transporting the colimit property back along the isomorphism between $ s $ and its extension.

CategoryTheory.Limits.IsColimit.extendIsoEquiv definition

{s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] : IsColimit s ≃ IsColimit (s.extend i)

Full source

/-- A cocone is a colimit cocone iff its extension by an isomorphism is. -/
def extendIsoEquiv {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] :
    IsColimitIsColimit s ≃ IsColimit (s.extend i) :=
  equivOfSubsingletonOfSubsingleton (extendIso i) (ofExtendIso i)

Equivalence of colimit cocone proofs under isomorphism extension

Informal description

Given a cocone $ s $ for a functor $ F \colon J \to C $, a morphism $ i \colon s.\mathrm{pt} \to X $ that is an isomorphism, there is an equivalence between the type of proofs that $ s $ is a colimit cocone and the type of proofs that the extended cocone $ s.\mathrm{extend}\, i $ is a colimit cocone. This equivalence is established by the functions `extendIso` and `ofExtendIso`, which respectively extend a colimit cocone by an isomorphism and recover the original colimit cocone from its extension.

CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence definition

 {F : J ⥤ C} {s : Cocone F} {G : K ⥤ C} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K)
  (w : e.functor ⋙ G ≅ F) : s.pt ≅ t.pt

Full source

/-- We can prove two cocone points `(s : Cocone F).pt` and `(t : Cocone G).pt` are isomorphic if
* both cocones are colimit cocones
* their indexing categories are equivalent via some `e : J ≌ K`,
* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.

This is the most general form of uniqueness of cocone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
-/
@[simps]
def coconePointsIsoOfEquivalence {F : J ⥤ C} {s : Cocone F} {G : K ⥤ C} {t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K) (w : e.functor ⋙ Ge.functor ⋙ G ≅ F) : s.pt ≅ t.pt :=
  let w' : e.inverse ⋙ Fe.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ invFunIdAssoc e G
  { hom := P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t)
    inv := Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s)
    hom_inv_id := by
      apply hom_ext P; intro j
      dsimp [w']
      simp only [Limits.Cocone.whisker_ι, fac, invFunIdAssoc_inv_app, whiskerLeft_app, assoc,
        comp_id, Limits.Cocones.precompose_obj_ι, fac_assoc, NatTrans.comp_app]
      rw [counitInv_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
      dsimp
      simp
    inv_hom_id := by
      apply hom_ext Q
      aesop_cat }

Isomorphism of colimit cocone points under equivalence of indexing categories

Informal description

Given two colimit cocones $s$ and $t$ for functors $F \colon J \to C$ and $G \colon K \to C$ respectively, and an equivalence of categories $e \colon J \simeq K$ such that the composition $e.\text{functor} \circ G$ is naturally isomorphic to $F$, then the apex objects $s.\text{pt}$ and $t.\text{pt}$ are isomorphic in $C$. More precisely, the isomorphism is constructed as follows: 1. The forward morphism is induced by the universal property of $s$ applied to the cocone obtained by reindexing $t$ along $e$. 2. The inverse morphism is induced by the universal property of $t$ applied to the cocone obtained by reindexing $s$ along the symmetric equivalence $e^{-1}$ and the natural isomorphism $e^{-1} \circ F \cong G$. 3. The compositions are shown to be identities using the uniqueness properties of the colimit cocones.

CategoryTheory.Limits.IsColimit.homEquiv definition

(h : IsColimit t) (W : C) : (t.pt ⟶ W) ≃ (F ⟶ (const J).obj W)

Full source

/-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
  a cocone on `F` with cone point `W`. -/
def homEquiv (h : IsColimit t) (W : C) : (t.pt ⟶ W) ≃ (F ⟶ (const J).obj W) where
  toFun f := (t.extend f).ι
  invFun ι := h.desc
      { pt := W
        ι }
  left_inv f := h.hom_ext (by simp)
  right_inv ι := by aesop_cat

Universal property of colimit cocone: morphism-natural transformation equivalence

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and an object $ W $ in $ C $, the equivalence `homEquiv h W` establishes a bijection between morphisms $ t.pt \to W $ and natural transformations $ F \to \Delta_W $, where $ \Delta_W $ is the constant functor at $ W $. The forward direction maps a morphism $ f $ to the cocone $ t.extend f $, while the inverse direction maps a natural transformation $ \iota $ to the unique morphism $ h.desc $ induced by the colimit property.

CategoryTheory.Limits.IsColimit.homEquiv_apply theorem

(h : IsColimit t) {W : C} (f : t.pt ⟶ W) : h.homEquiv W f = (t.extend f).ι

Full source

@[simp]
lemma homEquiv_apply (h : IsColimit t) {W : C} (f : t.pt ⟶ W) :
    h.homEquiv W f = (t.extend f).ι := rfl

Application of the Homomorphism-Natural Transformation Equivalence for Colimits

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and a morphism $ f \colon t.pt \to W $ in $ C $, the application of the equivalence `homEquiv` to $ f $ yields the natural transformation $ (t.extend f).\iota $, where $ t.extend f $ is the cocone obtained by extending $ t $ along $ f $.

CategoryTheory.Limits.IsColimit.homIso definition

(h : IsColimit t) (W : C) : ULift.{u₁} (t.pt ⟶ W : Type v₃) ≅ F ⟶ (const J).obj W

Full source

/-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
  a cocone on `F` with cone point `W`. -/
def homIso (h : IsColimit t) (W : C) : ULiftULift.{u₁} (t.pt ⟶ W : Type v₃) ≅ F ⟶ (const J).obj W :=
  Equiv.toIso (Equiv.ulift.trans (h.homEquiv W))

Isomorphism between lifted hom-set and natural transformations for colimits

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and an object $ W $ in $ C $, the isomorphism `homIso h W` establishes an isomorphism between the lifted hom-set $ \text{ULift}(t.pt \to W) $ and the set of natural transformations $ F \to \Delta_W $, where $ \Delta_W $ is the constant functor at $ W $. This isomorphism is constructed from the equivalence `homEquiv h W` via lifting.

CategoryTheory.Limits.IsColimit.homIso_hom theorem

(h : IsColimit t) {W : C} (f : ULift (t.pt ⟶ W)) : (IsColimit.homIso h W).hom f = (t.extend f.down).ι

Full source

@[simp]
theorem homIso_hom (h : IsColimit t) {W : C} (f : ULift (t.pt ⟶ W)) :
    (IsColimit.homIso h W).hom f = (t.extend f.down).ι :=
  rfl

Homomorphism-Natural Transformation Isomorphism for Colimits

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and a morphism $ f \colon t.pt \to W $ in $ C $ (lifted via `ULift`), the application of the isomorphism `homIso h W` to $ f $ yields the natural transformation $ (t.extend f.down).\iota $, where $ t.extend f.down $ is the cocone obtained by extending $ t $ along the unlifted morphism $ f.down $.

CategoryTheory.Limits.IsColimit.natIso definition

(h : IsColimit t) : coyoneda.obj (op t.pt) ⋙ uliftFunctor.{u₁} ≅ F.cocones

Full source

/-- The colimit of `F` represents the functor taking `W` to
  the set of cocones on `F` with cone point `W`. -/
def natIso (h : IsColimit t) : coyonedacoyoneda.obj (op t.pt) ⋙ uliftFunctor.{u₁}coyoneda.obj (op t.pt) ⋙ uliftFunctor.{u₁} ≅ F.cocones :=
  NatIso.ofComponents (IsColimit.homIso h)

Natural isomorphism between representable functor and cocone functor for colimits

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $, the natural isomorphism `natIso h` establishes an isomorphism between the composition of the co-Yoneda embedding applied to the opposite of the cocone's apex $ t.pt $ followed by the type lifting functor, and the functor of cocones over $ F $. In other words, it shows that the representable functor $ \mathrm{Hom}(t.pt, -) $ composed with lifting is naturally isomorphic to the functor sending an object $ W $ to the set of cocones on $ F $ with apex $ W $.

CategoryTheory.Limits.IsColimit.homIso' definition

 (h : IsColimit t) (W : C) :
  ULift.{u₁} (t.pt ⟶ W : Type v₃) ≅ { p : ∀ j, F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }

Full source

/-- Another, more explicit, formulation of the universal property of a colimit cocone.
See also `homIso`. -/
def homIso' (h : IsColimit t) (W : C) :
    ULiftULift.{u₁} (t.pt ⟶ W : Type v₃) ≅
      { p : ∀ j, F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
  h.homIso W ≪≫
    { hom := fun ι =>
        ⟨fun j => ι.app j, fun {j} {j'} f => by convert ← ι.naturality f; apply comp_id⟩
      inv := fun p =>
        { app := fun j => p.1 j
          naturality := fun j j' f => by dsimp; rw [comp_id]; exact p.2 f } }

Isomorphism between lifted hom-set and commuting families for colimits

Informal description

Given a colimit cocone $ t $ for a functor $ F \colon J \to C $ and an object $ W $ in $ C $, the isomorphism $\text{homIso}'\, h\, W$ establishes an equivalence between the lifted hom-set $\text{ULift}(t.pt \to W)$ and the set of all families of morphisms $ (p_j \colon F.obj\, j \to W)_{j \in J} $ that commute with the morphisms $ F.map\, f $ for all $ f \colon j \to j' $ in $ J $. More precisely, the isomorphism is constructed by composing the isomorphism $\text{homIso}\, h\, W$ with another isomorphism that identifies natural transformations $ F \to \Delta_W $ with such commuting families of morphisms.

CategoryTheory.Limits.IsColimit.ofFaithful definition

 {t : Cocone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [G.Faithful] (ht : IsColimit (mapCocone G t))
  (desc : ∀ s : Cocone F, t.pt ⟶ s.pt) (h : ∀ s, G.map (desc s) = ht.desc (mapCocone G s)) : IsColimit t

Full source

/-- If G : C → D is a faithful functor which sends t to a colimit cocone,
  then it suffices to check that the induced maps for the image of t
  can be lifted to maps of C. -/
def ofFaithful {t : Cocone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [G.Faithful]
    (ht : IsColimit (mapCocone G t)) (desc : ∀ s : Cocone F, t.pt ⟶ s.pt)
    (h : ∀ s, G.map (desc s) = ht.desc (mapCocone G s)) : IsColimit t :=
  { desc
    fac := fun s j => by apply G.map_injective; rw [G.map_comp, h]; apply ht.fac
    uniq := fun s m w => by
      apply G.map_injective; rw [h]
      refine ht.uniq (mapCocone G s) _ fun j => ?_
      convert ← congrArg (fun f => G.map f) (w j)
      apply G.map_comp }

Lifting colimit cocones along faithful functors

Informal description

Given a faithful functor $ G \colon C \to D $ that maps a cocone $ t $ on $ F \colon J \to C $ to a colimit cocone in $ D $, then $ t $ is a colimit cocone in $ C $ if for every cocone $ s $ on $ F $, the induced maps $ G \circ t \to G \circ s $ lift to maps $ t \to s $ in $ C $, and these lifts are compatible with the functor $ G $.

CategoryTheory.Limits.IsColimit.mapCoconeEquiv definition

 {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : Cocone K} (t : IsColimit (mapCocone F c)) :
  IsColimit (mapCocone G c)

Full source

/-- If `F` and `G` are naturally isomorphic, then `F.mapCocone c` being a colimit implies
`G.mapCocone c` is also a colimit.
-/
def mapCoconeEquiv {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G)
    {c : Cocone K} (t : IsColimit (mapCocone F c)) : IsColimit (mapCocone G c) := by
  apply IsColimit.ofIsoColimit _ (precomposeWhiskerLeftMapCocone h c)
  apply (precomposeInvEquiv (isoWhiskerLeft K h :) _).symm t

Colimit cocone property preserved under postcomposition with naturally isomorphic functors

Informal description

Given a natural isomorphism $ h \colon F \cong G $ between functors $ F, G \colon \mathcal{C} \to \mathcal{D} $, and a cocone $ c $ over a functor $ K \colon \mathcal{J} \to \mathcal{C} $, if the image of $ c $ under $ F $ is a colimit cocone in $ \mathcal{D} $, then the image of $ c $ under $ G $ is also a colimit cocone. More precisely, this states that the property of being a colimit cocone is preserved under postcomposition with naturally isomorphic functors.

CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism definition

{t : Cocone F} : IsColimit t ≅ ∀ s, Unique (t ⟶ s)

Full source

/-- A cocone is a colimit cocone exactly if
there is a unique cocone morphism from any other cocone.
-/
def isoUniqueCoconeMorphism {t : Cocone F} : IsColimitIsColimit t ≅ ∀ s, Unique (t ⟶ s) where
  hom h s :=
    { default := h.descCoconeMorphism s
      uniq := fun _ => h.uniq_cocone_morphism }
  inv h :=
    { desc := fun s => (h s).default.hom
      uniq := fun s f w => congrArg CoconeMorphism.hom ((h s).uniq ⟨f, w⟩) }

Isomorphism between colimit property and unique cocone morphisms

Informal description

For a cocone $ t $ over a functor $ F \colon J \to C $, the property of $ t $ being a colimit cocone is equivalent to the property that for every cocone $ s $ over $ F $, there exists a unique morphism of cocones from $ t $ to $ s $. More precisely, the isomorphism states that: 1. Given $ t $ is a colimit cocone, for any cocone $ s $, the set of morphisms $ t \to s $ is uniquely determined by the universal property of $ t $. 2. Conversely, if for every cocone $ s $ there is a unique morphism $ t \to s $, then $ t $ is a colimit cocone.

CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom definition

{Y : C} (f : X ⟶ Y) : Cocone F

Full source

/-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone
point `Y`. -/
def coconeOfHom {Y : C} (f : X ⟶ Y) : Cocone F where
  pt := Y
  ι := h.hom.app Y ⟨f⟩

Cocone construction from a morphism via natural isomorphism

Informal description

Given an object $Y$ in a category $\mathcal{C}$ and a morphism $f \colon X \to Y$, this constructs a cocone over the functor $F$ with apex $Y$. The cocone's injection maps are determined by applying the natural isomorphism $h$ to the morphism $f$ (viewed as an element of the hom-set $\mathrm{Hom}(X, Y)$).

CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone definition

(s : Cocone F) : X ⟶ s.pt

Full source

/-- If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.pt`. -/
def homOfCocone (s : Cocone F) : X ⟶ s.pt :=
  (h.inv.app s.pt s.ι).down

Morphism from representing object to cocone apex via natural isomorphism

Informal description

Given a cocone $s$ over a functor $F$, the morphism $\text{homOfCocone}\, h\, s$ is the unique morphism from the representing object $X$ to the apex of $s$ obtained by applying the inverse of the natural isomorphism $h$ to the cocone's injection maps.

CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone theorem

(s : Cocone F) : coconeOfHom h (homOfCocone h s) = s

Full source

@[simp]
theorem coconeOfHom_homOfCocone (s : Cocone F) : coconeOfHom h (homOfCocone h s) = s := by
  dsimp [coconeOfHom, homOfCocone]
  have ⟨s_pt,s_ι⟩ := s
  congr; dsimp
  convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) s_pt) s_ι using 1

Cocone Construction and Morphism Extraction are Inverse Operations

Informal description

Given a cocone $s$ over a functor $F$ in a category $\mathcal{C}$, the cocone constructed from the morphism obtained from $s$ via the natural isomorphism $h$ is equal to $s$ itself. That is, $\text{coconeOfHom}\, h\, (\text{homOfCocone}\, h\, s) = s$.

CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom theorem

{Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f

Full source

@[simp]
theorem homOfCocone_cooneOfHom {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f :=
  congrArg ULift.down (congrFun (congrFun (congrArg NatTrans.app h.hom_inv_id) Y) ⟨f⟩ :)

Inverse Property of Cocone Construction and Morphism Extraction

Informal description

Given an object $Y$ in a category $\mathcal{C}$ and a morphism $f \colon X \to Y$, the composition of the functions `homOfCocone` and `coconeOfHom` applied to $f$ yields back $f$, i.e., $\text{homOfCocone}\, h\, (\text{coconeOfHom}\, h\, f) = f$.

CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone definition

: Cocone F

Full source

/-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X`
will be a colimit cocone. -/
def colimitCocone : Cocone F :=
  coconeOfHom h (𝟙 X)

Colimit cocone from corepresenting isomorphism

Informal description

Given a natural isomorphism $h$ that corepresents the cocones of a functor $F$ by an object $X$ in a category $\mathcal{C}$, the colimit cocone is constructed as the cocone corresponding to the identity morphism $\mathrm{id}_X$ on $X$ via the isomorphism $h$.

CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac theorem

{Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f

Full source

/-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
the colimit cocone extended by `f`. -/
theorem coconeOfHom_fac {Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f := by
  dsimp [coconeOfHom, colimitCocone, Cocone.extend]
  congr with j
  have t := congrFun (h.hom.naturality f) ⟨𝟙 X⟩
  dsimp at t
  simp only [id_comp] at t
  rw [congrFun (congrArg NatTrans.app t) j]
  rfl

Cocone Construction as Extension of Colimit Cocone

Informal description

For any object $Y$ in a category $\mathcal{C}$ and any morphism $f \colon X \to Y$, the cocone constructed from $f$ via the natural isomorphism $h$ is equal to the extension of the colimit cocone by $f$. That is, $\text{coconeOfHom}\, h\, f = (\text{colimitCocone}\, h).\text{extend}\, f$.

CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac theorem

(s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = s

Full source

/-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
corresponding morphism. -/
theorem cocone_fac (s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = s := by
  rw [← coconeOfHom_homOfCocone h s]
  conv_lhs => simp only [homOfCocone_cooneOfHom]
  apply (coconeOfHom_fac _ _).symm

Extension of Colimit Cocone by Induced Morphism Recovers Original Cocone

Informal description

Given a cocone $s$ over a functor $F$ in a category $\mathcal{C}$, the extension of the colimit cocone (constructed via the natural isomorphism $h$) by the morphism $\text{homOfCocone}\, h\, s$ is equal to $s$. That is, $(\text{colimitCocone}\, h).\text{extend}\, (\text{homOfCocone}\, h\, s) = s$.

CategoryTheory.Limits.IsColimit.ofNatIso definition

{X : C} (h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁} ≅ F.cocones) : IsColimit (colimitCocone h)

Full source

/-- If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on
the representing object is a colimit cocone.
-/
def ofNatIso {X : C} (h : coyonedacoyoneda.obj (op X) ⋙ uliftFunctor.{u₁}coyoneda.obj (op X) ⋙ uliftFunctor.{u₁} ≅ F.cocones) :
    IsColimit (colimitCocone h) where
  desc s := homOfCocone h s
  fac s j := by
    have h := cocone_fac h s
    cases s
    injection h with h₁ h₂
    simp only [heq_iff_eq] at h₂
    conv_rhs => rw [← h₂]
    rfl
  uniq s m w := by
    rw [← homOfCocone_cooneOfHom h m]
    congr
    rw [coconeOfHom_fac]
    dsimp [Cocone.extend]; cases s; congr with j; exact w j

Colimit cocone from corepresenting natural isomorphism

Informal description

Given a natural isomorphism $ h $ between the functor $ \text{coyoneda.obj} (\text{op} X) \circ \text{uliftFunctor} $ and the cocone functor $ F.\text{cocones} $, the cocone corresponding to the identity morphism on $ X $ via $ h $ is a colimit cocone for $ F $. This means that for any cocone $ s $ over $ F $, there exists a unique morphism $ X \to s.\text{pt} $ (the apex of $ s $) that commutes with the cocone structure.

Mathlib.CategoryTheory.Limits.IsLimit

Implementation

References