Mathlib.CategoryTheory.Limits.Cones

CategoryTheory.Functor.cones definition

: Cᵒᵖ ⥤ Type max u₁ v₃

Full source

/-- If `F : J ⥤ C` then `F.cones` is the functor assigning to an object `X : C` the
type of natural transformations from the constant functor with value `X` to `F`.
An object representing this functor is a limit of `F`.
-/
@[simps!]
def cones : CᵒᵖCᵒᵖ ⥤ Type max u₁ v₃ :=
  (const J).op ⋙ yoneda.obj F

Functor of Cones over $F$

Informal description

Given a functor $F \colon J \to C$, the functor $F.\mathrm{cones} \colon C^{\mathrm{op}} \to \mathrm{Type}$ assigns to each object $X \in C$ the type of natural transformations from the constant functor with value $X$ to $F$. An object representing this functor is a limit of $F$.

CategoryTheory.Functor.cocones definition

: C ⥤ Type max u₁ v₃

Full source

/-- If `F : J ⥤ C` then `F.cocones` is the functor assigning to an object `(X : C)`
the type of natural transformations from `F` to the constant functor with value `X`.
An object corepresenting this functor is a colimit of `F`.
-/
@[simps!]
def cocones : C ⥤ Type max u₁ v₃ :=
  constconst J ⋙ coyoneda.obj (op F)

Functor of Cocones over $F$

Informal description

Given a functor $F \colon J \to C$, the functor $F.\mathrm{cocones} \colon C \to \mathrm{Type}$ assigns to each object $X \in C$ the type of natural transformations from $F$ to the constant functor with value $X$. An object corepresenting this functor is a colimit of $F$.

CategoryTheory.cones definition

: (J ⥤ C) ⥤ Cᵒᵖ ⥤ Type max u₁ v₃

Full source

/-- Functorially associated to each functor `J ⥤ C`, we have the `C`-presheaf consisting of
cones with a given cone point.
-/
@[simps!]
def cones : (J ⥤ C) ⥤ Cᵒᵖ ⥤ Type max u₁ v₃ where
  obj := Functor.cones
  map f := whiskerLeft (const J).op (yoneda.map f)

Functor of Cones over a Diagram

Informal description

The functor $\mathrm{cones} \colon (J \to C) \to (C^{\mathrm{op}} \to \mathrm{Type})$ assigns to each functor $F \colon J \to C$ the presheaf $F.\mathrm{cones} \colon C^{\mathrm{op}} \to \mathrm{Type}$, which sends an object $X \in C$ to the set of natural transformations from the constant functor with value $X$ to $F$. For a natural transformation $f \colon F \to F'$, the functor $\mathrm{cones}$ maps $f$ to the natural transformation obtained by left whiskering with the constant functor and the Yoneda embedding.

CategoryTheory.cocones definition

: (J ⥤ C)ᵒᵖ ⥤ C ⥤ Type max u₁ v₃

Full source

/-- Contravariantly associated to each functor `J ⥤ C`, we have the `C`-copresheaf consisting of
cocones with a given cocone point.
-/
@[simps!]
def cocones : (J ⥤ C)ᵒᵖ(J ⥤ C)ᵒᵖ ⥤ C ⥤ Type max u₁ v₃ where
  obj F := Functor.cocones (unop F)
  map f := whiskerLeft (const J) (coyoneda.map f)

Functor of Cocones over a Diagram

Informal description

The functor that associates to each functor $F \colon J \to C$ (viewed as an object in the opposite category $(J \to C)^{\mathrm{op}}$) the copresheaf of cocones over $F$. Specifically, for a functor $F$, it returns the functor $C \to \mathrm{Type}$ that sends an object $X$ in $C$ to the set of natural transformations from $F$ to the constant functor with value $X$. For a morphism $f \colon F \to F'$ in $(J \to C)^{\mathrm{op}}$, it maps to the natural transformation between the corresponding copresheaves of cocones via left whiskering with the constant functor and the co-Yoneda embedding.

CategoryTheory.Limits.Cone structure

(F : J ⥤ C)

Full source

/-- A `c : Cone F` is:
* an object `c.pt` and
* a natural transformation `c.π : c.pt ⟶ F` from the constant `c.pt` functor to `F`.

Example: if `J` is a category coming from a poset then the data required to make
a term of type `Cone F` is morphisms `πⱼ : c.pt ⟶ F j` for all `j : J` and,
for all `i ≤ j` in `J`, morphisms `πᵢⱼ : F i ⟶ F j` such that `πᵢ ≫ πᵢⱼ = πᵢ`.

`Cone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cones.obj X`.
-/
structure Cone (F : J ⥤ C) where
  /-- An object of `C` -/
  pt : C
  /-- A natural transformation from the constant functor at `X` to `F` -/
  π : (const J).obj pt ⟶ F

Cone over a functor

Informal description

A cone over a functor $F \colon J \to C$ consists of: - An object $c.\mathrm{pt}$ in $C$ called the *cone point*. - A natural transformation $c.\pi \colon \Delta(c.\mathrm{pt}) \Rightarrow F$, where $\Delta(c.\mathrm{pt})$ is the constant functor at $c.\mathrm{pt}$. For any morphism $f \colon j \to j'$ in $J$, the components of the natural transformation satisfy the commutativity condition $c.\pi_j \circ F(f) = c.\pi_{j'}$.

CategoryTheory.Limits.inhabitedCone instance

(F : Discrete PUnit ⥤ C) : Inhabited (Cone F)

Full source

instance inhabitedCone (F : DiscreteDiscrete PUnit ⥤ C) : Inhabited (Cone F) :=
  ⟨{  pt := F.obj ⟨⟨⟩⟩
      π := { app := fun ⟨⟨⟩⟩ => 𝟙 _
             naturality := by
              intro X Y f
              match X, Y, f with
              | .mk A, .mk B, .up g =>
                aesop_cat
           }
  }⟩

Existence of Cones over Functors from the Discrete Unit Category

Informal description

For any functor $F \colon \mathrm{Discrete\ PUnit} \to C$ from the discrete category on the unit type to a category $C$, the type of cones over $F$ is inhabited. That is, there exists at least one cone over $F$.

CategoryTheory.Limits.Cone.w theorem

{F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') : c.π.app j ≫ F.map f = c.π.app j'

Full source

@[reassoc (attr := simp)]
theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') :
    c.π.app j ≫ F.map f = c.π.app j' := by
  rw [← c.π.naturality f]
  apply id_comp

Commutativity Condition for Cone Components

Informal description

For any cone $c$ over a functor $F \colon J \to C$ and any morphism $f \colon j \to j'$ in $J$, the diagram \[ c.\pi_j \circ F(f) = c.\pi_{j'} \] commutes, where $c.\pi_j$ is the component of the cone's natural transformation at object $j$.

CategoryTheory.Limits.Cocone structure

(F : J ⥤ C)

Full source

/-- A `c : Cocone F` is
* an object `c.pt` and
* a natural transformation `c.ι : F ⟶ c.pt` from `F` to the constant `c.pt` functor.

For example, if the source `J` of `F` is a partially ordered set, then to give
`c : Cocone F` is to give a collection of morphisms `ιⱼ : F j ⟶ c.pt` and, for
all `j ≤ k` in `J`, morphisms `ιⱼₖ : F j ⟶ F k` such that `Fⱼₖ ≫ Fₖ = Fⱼ` for all `j ≤ k`.

`Cocone F` is equivalent, via `Cone.equiv` below, to `Σ X, F.cocones.obj X`.
-/
structure Cocone (F : J ⥤ C) where
  /-- An object of `C` -/
  pt : C
  /-- A natural transformation from `F` to the constant functor at `pt` -/
  ι : F ⟶ (const J).obj pt

Cocone over a functor

Informal description

A cocone `c` over a functor `F : J ⥤ C` consists of: - An object `c.pt` in `C` called the cocone point - A natural transformation `c.ι : F ⟶ c.pt` from `F` to the constant functor at `c.pt` For a partially ordered set `J`, this means giving: - Morphisms `ιⱼ : F j → c.pt` for each `j ∈ J` - For all `j ≤ k` in `J`, morphisms `F j → F k` making the obvious diagrams commute

CategoryTheory.Limits.inhabitedCocone instance

(F : Discrete PUnit ⥤ C) : Inhabited (Cocone F)

Full source

instance inhabitedCocone (F : DiscreteDiscrete PUnit ⥤ C) : Inhabited (Cocone F) :=
  ⟨{  pt := F.obj ⟨⟨⟩⟩
      ι := { app := fun ⟨⟨⟩⟩ => 𝟙 _
             naturality := by
              intro X Y f
              match X, Y, f with
              | .mk A, .mk B, .up g =>
                simp
           }
  }⟩

Existence of Cocones for Functors from the Discrete Unit Category

Informal description

For any functor $F$ from the discrete category on the unit type to a category $C$, the type of cocones over $F$ is inhabited.

CategoryTheory.Limits.Cocone.w theorem

{F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j ⟶ j') : F.map f ≫ c.ι.app j' = c.ι.app j

Full source

@[reassoc]
theorem Cocone.w {F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j ⟶ j') :
    F.map f ≫ c.ι.app j' = c.ι.app j := by
  rw [c.ι.naturality f]
  apply comp_id

Cocone Naturality Condition

Informal description

For any cocone $c$ over a functor $F \colon J \to C$ and any morphism $f \colon j \to j'$ in $J$, the diagram \[ F(j) \xrightarrow{F(f)} F(j') \xrightarrow{\iota_{j'}} c.\mathrm{pt} \] commutes with the cocone's natural transformation $\iota$, i.e., $F(f) \circ \iota_{j'} = \iota_j$.

CategoryTheory.Limits.Cone.equiv definition

(F : J ⥤ C) : Cone F ≅ Σ X, F.cones.obj X

Full source

/-- The isomorphism between a cone on `F` and an element of the functor `F.cones`. -/
@[simps!]
def equiv (F : J ⥤ C) : ConeCone F ≅ ΣX, F.cones.obj X where
  hom c := ⟨op c.pt, c.π⟩
  inv c :=
    { pt := c.1.unop
      π := c.2 }
  hom_inv_id := by
    funext X
    cases X
    rfl
  inv_hom_id := by
    funext X
    cases X
    rfl

Isomorphism between cones and elements of the cones functor

Informal description

Given a functor $F \colon J \to C$, there is a natural isomorphism between the type of cones over $F$ and the dependent pair type $\Sigma X, F.\mathrm{cones}(X)$, where: - The forward direction maps a cone $c$ to the pair $\langle c.\mathrm{pt}, c.\pi \rangle$. - The backward direction maps a pair $\langle X, \pi \rangle$ to the cone with point $X$ and natural transformation $\pi$. This isomorphism establishes that cones over $F$ are equivalent to elements of the functor $F.\mathrm{cones}$.

CategoryTheory.Limits.Cone.extensions definition

(c : Cone F) : yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cones

Full source

/-- A map to the vertex of a cone naturally induces a cone by composition. -/
@[simps]
def extensions (c : Cone F) : yonedayoneda.obj c.pt ⋙ uliftFunctor.{u₁}yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cones where
  app _ f := (const J).map f.down ≫ c.π

Natural transformation induced by cone extensions

Informal description

Given a cone $c$ over a functor $F \colon J \to C$, the natural transformation $\mathrm{extensions}\, c$ maps an object $X$ in $C$ to the function that takes a morphism $f \colon X \to c.\mathrm{pt}$ and returns the natural transformation obtained by composing the constant natural transformation at $f$ with the cone's natural transformation $c.\pi$. More precisely, for any $X \in C$, the component $(\mathrm{extensions}\, c)_X$ sends a lifted morphism $f \colon \mathrm{ULift}\, (\mathrm{Hom}(X, c.\mathrm{pt}))$ to the natural transformation $\Delta(f.\mathrm{down}) \circ c.\pi$, where $\Delta(f.\mathrm{down})$ is the constant natural transformation induced by $f.\mathrm{down} \colon X \to c.\mathrm{pt}$. This defines a natural transformation from the functor $\mathrm{Hom}(-, c.\mathrm{pt}) \circ \mathrm{ULift}$ to the functor of cones over $F$.

CategoryTheory.Limits.Cone.extend definition

(c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F

Full source

/-- A map to the vertex of a cone induces a cone by composition. -/
@[simps]
def extend (c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F :=
  { pt := X
    π := c.extensions.app (op X) ⟨f⟩ }

Extension of a cone by precomposition

Informal description

Given a cone $c$ over a functor $F \colon J \to C$ and a morphism $f \colon X \to c.\mathrm{pt}$ in $C$, the extended cone $\mathrm{extend}\, c\, f$ is a new cone over $F$ with: - Cone point $X$ - Natural transformation obtained by composing the constant natural transformation at $f$ with $c.\pi$ This construction replaces the original cone point with $X$ and adjusts the natural transformation accordingly via precomposition with $f$.

CategoryTheory.Limits.Cone.whisker definition

(E : K ⥤ J) (c : Cone F) : Cone (E ⋙ F)

Full source

/-- Whisker a cone by precomposition of a functor. -/
@[simps]
def whisker (E : K ⥤ J) (c : Cone F) : Cone (E ⋙ F) where
  pt := c.pt
  π := whiskerLeft E c.π

Whiskering a cone by precomposition of a functor

Informal description

Given a functor $E \colon K \to J$ and a cone $c$ over a functor $F \colon J \to C$, the whiskered cone $\text{Cone.whisker}\, E\, c$ is a cone over the composition $E \circ F \colon K \to C$ with the same cone point as $c$ and whose natural transformation is obtained by left whiskering $c.\pi$ with $E$.

CategoryTheory.Limits.Cocone.equiv definition

(F : J ⥤ C) : Cocone F ≅ Σ X, F.cocones.obj X

Full source

/-- The isomorphism between a cocone on `F` and an element of the functor `F.cocones`. -/
def equiv (F : J ⥤ C) : CoconeCocone F ≅ ΣX, F.cocones.obj X where
  hom c := ⟨c.pt, c.ι⟩
  inv c :=
    { pt := c.1
      ι := c.2 }
  hom_inv_id := by
    funext X
    cases X
    rfl
  inv_hom_id := by
    funext X
    cases X
    rfl

Isomorphism between cocones and their functorial representation

Informal description

The isomorphism between the type of cocones over a functor $F \colon J \to C$ and the dependent pair type $\Sigma X, F.\mathrm{cocones}(X)$, where $X$ ranges over objects of $C$ and $F.\mathrm{cocones}(X)$ is the type of natural transformations from $F$ to the constant functor at $X$. Concretely: - The forward direction maps a cocone $c$ to the pair $(c.\mathrm{pt}, c.\iota)$ - The backward direction maps a pair $(X, \iota)$ to the cocone with point $X$ and natural transformation $\iota$ - These operations are mutually inverse, establishing an isomorphism.

CategoryTheory.Limits.Cocone.extensions definition

(c : Cocone F) : coyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁} ⟶ F.cocones

Full source

/-- A map from the vertex of a cocone naturally induces a cocone by composition. -/
@[simps]
def extensions (c : Cocone F) : coyonedacoyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁}coyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁} ⟶ F.cocones where
  app _ f := c.ι ≫ (const J).map f.down

Cocone extension natural transformation

Informal description

Given a cocone $c$ over a functor $F \colon J \to C$, the natural transformation $\text{extensions}\, c$ maps any morphism $f \colon c.\text{pt} \to Y$ (lifted via $\text{ULift}$) to the cocone obtained by composing the cocone's natural transformation $c.\iota$ with the constant functor applied to $f$. This yields a new cocone with vertex $Y$ where the components are given by $c.\iota_j \circ f$ for each $j \in J$.

CategoryTheory.Limits.Cocone.extend definition

(c : Cocone F) {Y : C} (f : c.pt ⟶ Y) : Cocone F

Full source

/-- A map from the vertex of a cocone induces a cocone by composition. -/
@[simps]
def extend (c : Cocone F) {Y : C} (f : c.pt ⟶ Y) : Cocone F where
  pt := Y
  ι := c.extensions.app Y ⟨f⟩

Extension of a cocone by composition

Informal description

Given a cocone $c$ over a functor $F \colon J \to C$ and a morphism $f \colon c.\mathrm{pt} \to Y$ in $C$, the extended cocone $\mathrm{Cocone.extend}\, c\, f$ has vertex $Y$ and its natural transformation is obtained by composing the components of $c.\iota$ with $f$. Concretely, for each object $j$ in $J$, the component $\iota_j$ of the extended cocone is given by $c.\iota_j \circ f$.

CategoryTheory.Limits.Cocone.whisker definition

(E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F)

Full source

/-- Whisker a cocone by precomposition of a functor. See `whiskering` for a functorial
version.
-/
@[simps]
def whisker (E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F) where
  pt := c.pt
  ι := whiskerLeft E c.ι

Whiskering a cocone by precomposition

Informal description

Given a functor $E \colon K \to J$ and a cocone $c$ over a functor $F \colon J \to C$, the whiskered cocone $\text{Cocone.whisker}\, E\, c$ is a cocone over the composition $E \circ F \colon K \to C$ with the same cocone point as $c$. The natural transformation for this cocone is obtained by left whiskering $c.\iota$ with $E$.

CategoryTheory.Limits.ConeMorphism structure

(A B : Cone F)

Full source

/-- A cone morphism between two cones for the same diagram is a morphism of the cone points which
commutes with the cone legs. -/
structure ConeMorphism (A B : Cone F) where
  /-- A morphism between the two vertex objects of the cones -/
  hom : A.pt ⟶ B.pt
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  w : ∀ j : J, hom ≫ B.π.app j = A.π.app j := by aesop_cat

Cone Morphism

Informal description

A morphism between two cones $A$ and $B$ over the same functor $F \colon J \to C$ consists of a morphism $h \colon A.\mathrm{pt} \to B.\mathrm{pt}$ between their cone points, such that for every object $j$ in $J$, the diagram \[ A.\mathrm{pt} \xrightarrow{h} B.\mathrm{pt} \] \[ A.\pi_j \downarrow \qquad \downarrow B.\pi_j \] \[ F(j) \quad = \quad F(j) \] commutes, i.e., $A.\pi_j = h \circ B.\pi_j$ for all $j$.

CategoryTheory.Limits.inhabitedConeMorphism instance

(A : Cone F) : Inhabited (ConeMorphism A A)

Full source

instance inhabitedConeMorphism (A : Cone F) : Inhabited (ConeMorphism A A) :=
  ⟨{ hom := 𝟙 _ }⟩

Identity Cone Morphism Exists for Every Cone

Informal description

For any cone $A$ over a functor $F \colon J \to C$, there exists a canonical morphism from $A$ to itself, namely the identity morphism on the cone point $A.\mathrm{pt}$.

CategoryTheory.Limits.Cone.category instance

: Category (Cone F)

Full source

/-- The category of cones on a given diagram. -/
@[simps]
instance Cone.category : Category (Cone F) where
  Hom A B := ConeMorphism A B
  comp f g := { hom := f.hom ≫ g.hom }
  id B := { hom := 𝟙 B.pt }

-- Porting note: if we do not have `simps` automatically generate the lemma for simplifying
-- the hom field of a category, we need to write the `ext` lemma in terms of the categorical
-- morphism, rather than the underlying structure.

The Category of Cones over a Functor

Informal description

For any functor $F \colon J \to C$, the collection of cones over $F$ forms a category, where: - The objects are cones over $F$, each consisting of a cone point and a natural transformation from the constant functor at the cone point to $F$. - The morphisms between cones $A$ and $B$ are given by morphisms $h \colon A.\mathrm{pt} \to B.\mathrm{pt}$ that commute with the cone's natural transformations.

CategoryTheory.Limits.ConeMorphism.ext theorem

{c c' : Cone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Full source

@[ext]
theorem ConeMorphism.ext {c c' : Cone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g := by
  cases f
  cases g
  congr

Extensionality of Cone Morphisms via Underlying Morphism Equality

Informal description

Let $c$ and $c'$ be two cones over a functor $F \colon J \to C$, and let $f, g \colon c \to c'$ be two morphisms of cones. If the underlying morphisms $f.\mathrm{hom}$ and $g.\mathrm{hom}$ between the cone points are equal, then $f = g$.

CategoryTheory.Limits.Cones.eta definition

(c : Cone F) : c ≅ ⟨c.pt, c.π⟩

Full source

/-- Eta rule for cones. -/
@[simps!]
def eta (c : Cone F) : c ≅ ⟨c.pt, c.π⟩ :=
  Cones.ext (Iso.refl _)

Eta isomorphism for cones

Informal description

For any cone $c$ over a functor $F \colon J \to C$, there is an isomorphism between $c$ and the cone constructed from its own cone point $c.\mathrm{pt}$ and natural transformation $c.\pi$. This isomorphism is given by the identity morphism on $c.\mathrm{pt}$.

CategoryTheory.Limits.Cones.cone_iso_of_hom_iso theorem

{K : J ⥤ C} {c d : Cone K} (f : c ⟶ d) [i : IsIso f.hom] : IsIso f

Full source

/-- Given a cone morphism whose object part is an isomorphism, produce an
isomorphism of cones.
-/
theorem cone_iso_of_hom_iso {K : J ⥤ C} {c d : Cone K} (f : c ⟶ d) [i : IsIso f.hom] : IsIso f :=
  ⟨⟨{   hom := inv f.hom
        w := fun j => (asIso f.hom).inv_comp_eq.2 (f.w j).symm }, by aesop_cat⟩⟩

Isomorphism of cones induced by isomorphism of cone points

Informal description

Let $\mathcal{C}$ and $\mathcal{J}$ be categories, and let $K \colon \mathcal{J} \to \mathcal{C}$ be a functor. Given two cones $c$ and $d$ over $K$ and a morphism of cones $f \colon c \to d$, if the underlying morphism $f.\mathrm{hom} \colon c.\mathrm{pt} \to d.\mathrm{pt}$ is an isomorphism in $\mathcal{C}$, then $f$ itself is an isomorphism of cones.

CategoryTheory.Limits.Cones.extend definition

(s : Cone F) {X : C} (f : X ⟶ s.pt) : s.extend f ⟶ s

Full source

/-- There is a morphism from an extended cone to the original cone. -/
@[simps]
def extend (s : Cone F) {X : C} (f : X ⟶ s.pt) : s.extend f ⟶ s where
  hom := f

Morphism from extended cone to original cone

Informal description

Given a cone $s$ over a functor $F \colon J \to C$ and a morphism $f \colon X \to s.\mathrm{pt}$ in $C$, there is a morphism from the extended cone $s.\mathrm{extend}\, f$ to the original cone $s$, where the morphism is given by $f$ itself.

CategoryTheory.Limits.Cones.extendId definition

(s : Cone F) : s.extend (𝟙 s.pt) ≅ s

Full source

/-- Extending a cone by the identity does nothing. -/
@[simps!]
def extendId (s : Cone F) : s.extend (𝟙 s.pt) ≅ s :=
  Cones.ext (Iso.refl _)

Isomorphism between a cone and its extension by the identity

Informal description

For any cone $s$ over a functor $F \colon J \to C$, extending the cone by the identity morphism $\text{id}_{s.\mathrm{pt}}$ yields a cone that is isomorphic to the original cone $s$.

CategoryTheory.Limits.Cones.extendComp definition

(s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : s.extend (f ≫ g) ≅ (s.extend g).extend f

Full source

/-- Extending a cone by a composition is the same as extending the cone twice. -/
@[simps!]
def extendComp (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) :
    s.extend (f ≫ g) ≅ (s.extend g).extend f :=
  Cones.ext (Iso.refl _)

Composition of cone extensions

Informal description

Given a cone $s$ over a functor $F \colon J \to C$ and morphisms $f \colon X \to Y$ and $g \colon Y \to s.\mathrm{pt}$ in $C$, the extension of $s$ by the composition $f \circ g$ is isomorphic to the extension of $s$ by $g$ followed by the extension by $f$. More precisely, there is an isomorphism between the cones: $$ s.\mathrm{extend}(f \circ g) \cong (s.\mathrm{extend}\, g).\mathrm{extend}\, f $$ where both sides have cone point $X$ and appropriately adjusted natural transformations.

CategoryTheory.Limits.Cones.extendIso definition

(s : Cone F) {X : C} (f : X ≅ s.pt) : s.extend f.hom ≅ s

Full source

/-- A cone extended by an isomorphism is isomorphic to the original cone. -/
@[simps]
def extendIso (s : Cone F) {X : C} (f : X ≅ s.pt) : s.extend f.hom ≅ s where
  hom := { hom := f.hom }
  inv := { hom := f.inv }

Isomorphism between extended cone and original cone via an isomorphism of cone points

Informal description

Given a cone $s$ over a functor $F \colon J \to C$ and an isomorphism $f \colon X \cong s.\mathrm{pt}$ in $C$, the extended cone $s.\mathrm{extend}\, f.\mathrm{hom}$ is isomorphic to the original cone $s$. Explicitly, the isomorphism consists of: - A morphism from the extended cone to the original cone given by $f.\mathrm{hom} \colon X \to s.\mathrm{pt}$. - An inverse morphism given by $f.\mathrm{inv} \colon s.\mathrm{pt} \to X$.

CategoryTheory.Limits.Cones.instIsIsoConeExtend instance

{s : Cone F} {X : C} (f : X ⟶ s.pt) [IsIso f] : IsIso (Cones.extend s f)

Full source

instance {s : Cone F} {X : C} (f : X ⟶ s.pt) [IsIso f] : IsIso (Cones.extend s f) :=
  ⟨(extendIso s (asIso f)).inv, by aesop_cat⟩

Isomorphism of Cone Extension via Isomorphism of Cone Points

Informal description

Given a cone $s$ over a functor $F \colon J \to C$ and a morphism $f \colon X \to s.\mathrm{pt}$ in $C$, if $f$ is an isomorphism, then the morphism $\mathrm{extend}\, s\, f$ from the extended cone $s.\mathrm{extend}\, f$ to $s$ is also an isomorphism.

CategoryTheory.Limits.Cones.postcompose definition

{G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G

Full source

/--
Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
-/
@[simps]
def postcompose {G : J ⥤ C} (α : F ⟶ G) : ConeCone F ⥤ Cone G where
  obj c :=
    { pt := c.pt
      π := c.π ≫ α }
  map f := { hom := f.hom }

Postcomposition of cones along a natural transformation

Informal description

Given a natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon J \to C$, the functor `postcompose` maps a cone over $F$ to a cone over $G$ by postcomposing the cone's natural transformation with $\alpha$. Explicitly, for a cone $c$ over $F$: - The cone point remains unchanged: $c.\mathrm{pt}$. - The natural transformation becomes $c.\pi \circ \alpha$. Morphisms between cones are preserved under this construction.

CategoryTheory.Limits.Cones.postcomposeComp definition

{G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) : postcompose (α ≫ β) ≅ postcompose α ⋙ postcompose β

Full source

/-- Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as
postcomposing by `α` and then by `β`. -/
@[simps!]
def postcomposeComp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
    postcomposepostcompose (α ≫ β) ≅ postcompose α ⋙ postcompose β :=
  NatIso.ofComponents fun s => Cones.ext (Iso.refl _)

Postcomposition of cones with composite natural transformation

Informal description

Given functors $ F, G, H \colon J \to C $ and natural transformations $ \alpha \colon F \Rightarrow G $ and $ \beta \colon G \Rightarrow H $, the functor obtained by postcomposing cones over $ F $ with the composite natural transformation $ \alpha \circ \beta $ is naturally isomorphic to the composition of the functors obtained by first postcomposing with $ \alpha $ and then with $ \beta $.

CategoryTheory.Limits.Cones.postcomposeId definition

: postcompose (𝟙 F) ≅ 𝟭 (Cone F)

Full source

/-- Postcomposing by the identity does not change the cone up to isomorphism. -/
@[simps!]
def postcomposeId : postcomposepostcompose (𝟙 F) ≅ 𝟭 (Cone F) :=
  NatIso.ofComponents fun s => Cones.ext (Iso.refl _)

Postcomposition with identity natural transformation preserves cones up to isomorphism

Informal description

The functor that postcomposes a cone over $F$ with the identity natural transformation $\mathrm{id}_F$ is naturally isomorphic to the identity functor on the category of cones over $F$. In other words, for any cone $s$ over $F$, the cone obtained by postcomposing $s$ with $\mathrm{id}_F$ is isomorphic to $s$ itself via the identity isomorphism on the cone point $s.\mathrm{pt}$.

CategoryTheory.Limits.Cones.postcomposeEquivalence definition

{G : J ⥤ C} (α : F ≅ G) : Cone F ≌ Cone G

Full source

/-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cones.
-/
@[simps]
def postcomposeEquivalence {G : J ⥤ C} (α : F ≅ G) : ConeCone F ≌ Cone G where
  functor := postcompose α.hom
  inverse := postcompose α.inv
  unitIso := NatIso.ofComponents fun s => Cones.ext (Iso.refl _)
  counitIso := NatIso.ofComponents fun s => Cones.ext (Iso.refl _)

Equivalence of cone categories induced by a natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$, there is an equivalence of categories between the category of cones over $F$ and the category of cones over $G$. The equivalence is constructed as follows: - The forward functor maps a cone $c$ over $F$ to a cone over $G$ by postcomposing the natural transformation $c.\pi$ with $\alpha$. - The inverse functor similarly postcomposes with $\alpha^{-1}$. - The unit and counit of the equivalence are both given by the identity isomorphism on the cone points.

CategoryTheory.Limits.Cones.whiskering definition

(E : K ⥤ J) : Cone F ⥤ Cone (E ⋙ F)

Full source

/-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cone F` to `Cone (E ⋙ F)`.
-/
@[simps]
def whiskering (E : K ⥤ J) : ConeCone F ⥤ Cone (E ⋙ F) where
  obj c := c.whisker E
  map f := { hom := f.hom }

Whiskering functor for cones

Informal description

Given a functor $E \colon K \to J$, the whiskering functor $\text{Cones.whisker}\, E$ maps a cone over $F \colon J \to C$ to a cone over the composition $E \circ F \colon K \to C$ by precomposing the natural transformation of the cone with $E$. On morphisms, it preserves the underlying morphism between the cone points.

CategoryTheory.Limits.Cones.whiskeringEquivalence definition

(e : K ≌ J) : Cone F ≌ Cone (e.functor ⋙ F)

Full source

/-- Whiskering by an equivalence gives an equivalence between categories of cones.
-/
@[simps]
def whiskeringEquivalence (e : K ≌ J) : ConeCone F ≌ Cone (e.functor ⋙ F) where
  functor := whiskering e.functor
  inverse := whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom
  unitIso := NatIso.ofComponents fun s => Cones.ext (Iso.refl _)
  counitIso :=
    NatIso.ofComponents
      fun s =>
        Cones.ext (Iso.refl _)
          (by
            intro k
            simpa [e.counit_app_functor] using s.w (e.unitInv.app k))

Equivalence of cone categories induced by whiskering with an equivalence

Informal description

Given an equivalence of categories $e \colon K \simeq J$, the whiskering equivalence $\text{Cones.whiskeringEquivalence}\, e$ establishes an equivalence between the category of cones over a functor $F \colon J \to C$ and the category of cones over the composition $e.\text{functor} \circ F \colon K \to C$. The equivalence consists of: - A functor that precomposes the cone's natural transformation with $e.\text{functor}$. - An inverse functor that precomposes with $e.\text{inverse}$ and then postcomposes with the natural isomorphism $(e.\text{invFunIdAssoc}\, F).\text{hom}$. - Natural isomorphisms witnessing the equivalence, constructed using identity isomorphisms on the cone points and coherence conditions involving the unit and counit of $e$.

CategoryTheory.Limits.Cones.equivalenceOfReindexing definition

{G : K ⥤ C} (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : Cone F ≌ Cone G

Full source

/-- The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
-/
@[simps! functor inverse unitIso counitIso]
def equivalenceOfReindexing {G : K ⥤ C} (e : K ≌ J) (α : e.functor ⋙ Fe.functor ⋙ F ≅ G) : ConeCone F ≌ Cone G :=
  (whiskeringEquivalence e).trans (postcomposeEquivalence α)

Equivalence of cone categories under reindexing and natural isomorphism

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a natural isomorphism $\alpha \colon e.\text{functor} \circ F \cong G$ between functors $F \colon J \to C$ and $G \colon K \to C$, there is an equivalence of categories between the category of cones over $F$ and the category of cones over $G$. This equivalence is constructed by first applying the whiskering equivalence induced by $e$, followed by the postcomposition equivalence induced by $\alpha$.

CategoryTheory.Limits.Cones.forget definition

: Cone F ⥤ C

Full source

/-- Forget the cone structure and obtain just the cone point. -/
@[simps]
def forget : ConeCone F ⥤ C where
  obj t := t.pt
  map f := f.hom

Forgetful functor from cones to base category

Informal description

The forgetful functor from the category of cones over a functor $F \colon J \to C$ to the base category $C$, which maps each cone to its cone point and each cone morphism to its underlying morphism in $C$.

CategoryTheory.Limits.Cones.functoriality definition

: Cone F ⥤ Cone (F ⋙ G)

Full source

/-- A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially. -/
@[simps]
def functoriality : ConeCone F ⥤ Cone (F ⋙ G) where
  obj A :=
    { pt := G.obj A.pt
      π :=
        { app := fun j => G.map (A.π.app j)
          naturality := by intros; erw [← G.map_comp]; simp } }
  map f :=
    { hom := G.map f.hom
      w := fun j => by simp [-ConeMorphism.w, ← f.w j] }

Functoriality of cones under composition with a functor

Informal description

Given a functor $G \colon C \to D$, the functoriality construction sends cones over a functor $F \colon J \to C$ to cones over the composition $F \circ G \colon J \to D$. Specifically: - For a cone $A$ over $F$ with cone point $A.\mathrm{pt}$ and natural transformation $A.\pi$, the resulting cone over $F \circ G$ has cone point $G(A.\mathrm{pt})$ and natural transformation with components $G(A.\pi_j)$ for each $j \in J$. - For a morphism $f$ between cones $A$ and $B$ over $F$, the corresponding morphism between the resulting cones over $F \circ G$ is given by $G(f.\mathrm{hom})$. This construction defines a functor from the category of cones over $F$ to the category of cones over $F \circ G$.

CategoryTheory.Limits.Cones.functorialityCompFunctoriality definition

(H : D ⥤ E) : functoriality F G ⋙ functoriality (F ⋙ G) H ≅ functoriality F (G ⋙ H)

Full source

/-- Functoriality is functorial. -/
def functorialityCompFunctoriality (H : D ⥤ E) :
    functorialityfunctoriality F G ⋙ functoriality (F ⋙ G) Hfunctoriality F G ⋙ functoriality (F ⋙ G) H ≅ functoriality F (G ⋙ H) :=
  NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [functoriality])

Natural isomorphism between composed functoriality constructions for cones

Informal description

Given functors $F \colon J \to C$, $G \colon C \to D$, and $H \colon D \to E$, the composition of the functoriality constructions for cones over $F$ and $F \circ G$ is naturally isomorphic to the functoriality construction for cones over $F$ composed with $G \circ H$. More precisely, the functor obtained by first applying the functoriality construction with $G$ and then with $H$ is isomorphic to the functor obtained by applying the functoriality construction with the composition $G \circ H$.

CategoryTheory.Limits.Cones.functoriality_full instance

[G.Full] [G.Faithful] : (functoriality F G).Full

Full source

instance functoriality_full [G.Full] [G.Faithful] : (functoriality F G).Full where
  map_surjective t :=
    ⟨{ hom := G.preimage t.hom
       w := fun j => G.map_injective (by simpa using t.w j) }, by aesop_cat⟩

Fullness of Cone Functoriality under Fully Faithful Functors

Informal description

Given a fully faithful functor $G \colon C \to D$, the functoriality construction that sends cones over a functor $F \colon J \to C$ to cones over the composition $F \circ G \colon J \to D$ is a full functor.

CategoryTheory.Limits.Cones.functoriality_faithful instance

[G.Faithful] : (Cones.functoriality F G).Faithful

Full source

instance functoriality_faithful [G.Faithful] : (Cones.functoriality F G).Faithful where
  map_injective {_X} {_Y} f g h :=
    ConeMorphism.ext f g <| G.map_injective <| congr_arg ConeMorphism.hom h

Faithfulness of Cone Functoriality under Faithful Functors

Informal description

Given a faithful functor $G \colon C \to D$, the functoriality construction that sends cones over a functor $F \colon J \to C$ to cones over the composition $F \circ G \colon J \to D$ is a faithful functor.

CategoryTheory.Limits.Cones.functorialityEquivalence definition

(e : C ≌ D) : Cone F ≌ Cone (F ⋙ e.functor)

Full source

/-- If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cones over `F` and cones over `F ⋙ e.functor`.
-/
@[simps]
def functorialityEquivalence (e : C ≌ D) : ConeCone F ≌ Cone (F ⋙ e.functor) :=
  let f : (F ⋙ e.functor) ⋙ e.inverse(F ⋙ e.functor) ⋙ e.inverse ≅ F :=
    Functor.associatorFunctor.associator _ _ _ ≪≫ isoWhiskerLeft _ e.unitIso.symm ≪≫ Functor.rightUnitor _
  { functor := functoriality F e.functor
    inverse := functorialityfunctoriality (F ⋙ e.functor) e.inverse ⋙ (postcomposeEquivalence f).functor
    unitIso := NatIso.ofComponents fun c => Cones.ext (e.unitIso.app _)
    counitIso := NatIso.ofComponents fun c => Cones.ext (e.counitIso.app _) }

Equivalence of cone categories under composition with an equivalence of categories

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the functoriality construction induces an equivalence between the category of cones over a functor $F \colon J \to C$ and the category of cones over the composition $F \circ e.\text{functor} \colon J \to D$. Specifically: - The forward functor maps a cone $c$ over $F$ to a cone over $F \circ e.\text{functor}$ by applying $e.\text{functor}$ to the cone point and the components of the natural transformation. - The inverse functor is constructed using the inverse equivalence $e.\text{inverse}$ and a postcomposition with a natural isomorphism that arises from the equivalence data. - The unit and counit of the equivalence are given by the unit and counit isomorphisms of $e$, applied to the cone points.

CategoryTheory.Limits.Cones.reflects_cone_isomorphism instance

(F : C ⥤ D) [F.ReflectsIsomorphisms] (K : J ⥤ C) : (Cones.functoriality K F).ReflectsIsomorphisms

Full source

/-- If `F` reflects isomorphisms, then `Cones.functoriality F` reflects isomorphisms
as well.
-/
instance reflects_cone_isomorphism (F : C ⥤ D) [F.ReflectsIsomorphisms] (K : J ⥤ C) :
    (Cones.functoriality K F).ReflectsIsomorphisms := by
  constructor
  intro A B f _
  haveI : IsIso (F.map f.hom) :=
    (Cones.forget (K ⋙ F)).map_isIso ((Cones.functoriality K F).map f)
  haveI := ReflectsIsomorphisms.reflects F f.hom
  apply cone_iso_of_hom_iso

Reflection of Cone Isomorphisms under Functoriality

Informal description

Let $F \colon C \to D$ be a functor that reflects isomorphisms, and let $K \colon J \to C$ be any functor. Then the functoriality construction $\text{Cones.functoriality}\, K\, F$ from the category of cones over $K$ to the category of cones over $K \circ F$ also reflects isomorphisms. That is, if a morphism of cones becomes an isomorphism after applying $\text{Cones.functoriality}\, K\, F$, then it was already an isomorphism in the original category of cones over $K$.

CategoryTheory.Limits.CoconeMorphism structure

(A B : Cocone F)

Full source

/-- A cocone morphism between two cocones for the same diagram is a morphism of the cocone points
which commutes with the cocone legs. -/
structure CoconeMorphism (A B : Cocone F) where
  /-- A morphism between the (co)vertex objects in `C` -/
  hom : A.pt ⟶ B.pt
  /-- The triangle made from the two natural transformations and `hom` commutes -/
  w : ∀ j : J, A.ι.app j ≫ hom = B.ι.app j := by aesop_cat

Cocone morphism

Informal description

A morphism between two cocones $A$ and $B$ over the same diagram $F$ consists of a morphism $h : A.pt \to B.pt$ between their cocone points that commutes with the cocone legs, i.e., for each object $j$ in the diagram's indexing category, the diagram \[ F(j) \xrightarrow{A.ι_j} A.pt \xrightarrow{h} B.pt \] commutes with \[ F(j) \xrightarrow{B.ι_j} B.pt. \]

CategoryTheory.Limits.inhabitedCoconeMorphism instance

(A : Cocone F) : Inhabited (CoconeMorphism A A)

Full source

instance inhabitedCoconeMorphism (A : Cocone F) : Inhabited (CoconeMorphism A A) :=
  ⟨{ hom := 𝟙 _ }⟩

Existence of Identity Cocone Morphism

Informal description

For any cocone $A$ over a functor $F$, there exists an identity morphism from $A$ to itself in the category of cocones over $F$.

CategoryTheory.Limits.Cocone.category instance

: Category (Cocone F)

Full source

@[simps]
instance Cocone.category : Category (Cocone F) where
  Hom A B := CoconeMorphism A B
  comp f g := { hom := f.hom ≫ g.hom }
  id B := { hom := 𝟙 B.pt }

-- Porting note: if we do not have `simps` automatically generate the lemma for simplifying
-- the hom field of a category, we need to write the `ext` lemma in terms of the categorical
-- morphism, rather than the underlying structure.

The Category of Cocones over a Functor

Informal description

For any functor $F : J \to C$, the collection of cocones over $F$ forms a category, where: - Objects are cocones $(c.\text{pt}, c.\iota)$ over $F$ - Morphisms are cocone morphisms $h : c.\text{pt} \to c'.\text{pt}$ that commute with the cocone legs

CategoryTheory.Limits.CoconeMorphism.ext theorem

{c c' : Cocone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Full source

@[ext]
theorem CoconeMorphism.ext {c c' : Cocone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g := by
  cases f
  cases g
  congr

Extensionality of Cocone Morphisms

Informal description

Given two cocones $c$ and $c'$ over the same functor $F$, and two morphisms $f, g \colon c \to c'$ between them, if the underlying morphisms $f.\text{hom}$ and $g.\text{hom}$ between the cocone points are equal, then $f = g$ as cocone morphisms.

CategoryTheory.Limits.Cocones.eta definition

(c : Cocone F) : c ≅ ⟨c.pt, c.ι⟩

Full source

/-- Eta rule for cocones. -/
@[simps!]
def eta (c : Cocone F) : c ≅ ⟨c.pt, c.ι⟩ :=
  Cocones.ext (Iso.refl _)

Eta rule for cocones

Informal description

For any cocone $c$ over a functor $F : J \to C$, there is an isomorphism between $c$ and the cocone constructed from its own cocone point $c.\text{pt}$ and natural transformation $c.\iota$. This isomorphism is given by the identity morphism on $c.\text{pt}$.

CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso theorem

{K : J ⥤ C} {c d : Cocone K} (f : c ⟶ d) [i : IsIso f.hom] : IsIso f

Full source

/-- Given a cocone morphism whose object part is an isomorphism, produce an
isomorphism of cocones.
-/
theorem cocone_iso_of_hom_iso {K : J ⥤ C} {c d : Cocone K} (f : c ⟶ d) [i : IsIso f.hom] :
    IsIso f :=
  ⟨⟨{ hom := inv f.hom
      w := fun j => (asIso f.hom).comp_inv_eq.2 (f.w j).symm }, by aesop_cat⟩⟩

Isomorphism of Cocones from Isomorphism of Cocone Points

Informal description

Let $K \colon J \to C$ be a functor, and let $c$ and $d$ be cocones over $K$. Given a cocone morphism $f \colon c \to d$ such that the underlying morphism $f.\text{hom} \colon c.\text{pt} \to d.\text{pt}$ is an isomorphism, then $f$ itself is an isomorphism of cocones.

CategoryTheory.Limits.Cocones.extend definition

(s : Cocone F) {X : C} (f : s.pt ⟶ X) : s ⟶ s.extend f

Full source

/-- There is a morphism from a cocone to its extension. -/
@[simps]
def extend (s : Cocone F) {X : C} (f : s.pt ⟶ X) : s ⟶ s.extend f where
  hom := f

Cocone extension morphism

Informal description

Given a cocone $s$ over a functor $F \colon J \to C$ and a morphism $f \colon s.\mathrm{pt} \to X$ in $C$, there exists a cocone morphism from $s$ to the extended cocone $s.\mathrm{extend}\, f$, where the morphism is given by $f$ itself. The extended cocone has vertex $X$ and its natural transformation is obtained by composing the components of $s.\iota$ with $f$.

CategoryTheory.Limits.Cocones.extendId definition

(s : Cocone F) : s ≅ s.extend (𝟙 s.pt)

Full source

/-- Extending a cocone by the identity does nothing. -/
@[simps!]
def extendId (s : Cocone F) : s ≅ s.extend (𝟙 s.pt) :=
  Cocones.ext (Iso.refl _)

Isomorphism between a cocone and its extension by the identity

Informal description

Given a cocone $s$ over a functor $F \colon J \to C$, the isomorphism $\text{Cocones.extendId}\, s$ relates $s$ to its extension by the identity morphism $\text{id}_{s.\text{pt}}$. Specifically, this isomorphism has as its forward and backward morphisms the identity morphism on $s.\text{pt}$.

CategoryTheory.Limits.Cocones.extendComp definition

(s : Cocone F) {X Y : C} (f : s.pt ⟶ X) (g : X ⟶ Y) : s.extend (f ≫ g) ≅ (s.extend f).extend g

Full source

/-- Extending a cocone by a composition is the same as extending the cone twice. -/
@[simps!]
def extendComp (s : Cocone F) {X Y : C} (f : s.pt ⟶ X) (g : X ⟶ Y) :
    s.extend (f ≫ g) ≅ (s.extend f).extend g :=
  Cocones.ext (Iso.refl _)

Composition of cocone extensions

Informal description

Given a cocone $s$ over a functor $F \colon J \to C$, and morphisms $f \colon s.\mathrm{pt} \to X$ and $g \colon X \to Y$ in $C$, the cocone obtained by extending $s$ with the composition $f \circ g$ is isomorphic to the cocone obtained by first extending $s$ with $f$ and then extending the result with $g$.

CategoryTheory.Limits.Cocones.extendIso definition

(s : Cocone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.hom

Full source

/-- A cocone extended by an isomorphism is isomorphic to the original cone. -/
@[simps]
def extendIso (s : Cocone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.hom where
  hom := { hom := f.hom }
  inv := { hom := f.inv }

Isomorphism between a cocone and its extension by an isomorphism

Informal description

Given a cocone $s$ over a functor $F \colon J \to C$ and an isomorphism $f \colon s.\mathrm{pt} \cong X$ in $C$, the cocone $s$ is isomorphic to the extended cocone $s.\mathrm{extend}\, f.\mathrm{hom}$ obtained by composing the cocone legs with $f.\mathrm{hom}$.

CategoryTheory.Limits.Cocones.instIsIsoCoconeExtend instance

{s : Cocone F} {X : C} (f : s.pt ⟶ X) [IsIso f] : IsIso (Cocones.extend s f)

Full source

instance {s : Cocone F} {X : C} (f : s.pt ⟶ X) [IsIso f] : IsIso (Cocones.extend s f) :=
  ⟨(extendIso s (asIso f)).inv, by aesop_cat⟩

Extension of a cocone by an isomorphism yields an isomorphism

Informal description

Given a cocone $s$ over a functor $F \colon J \to C$ and a morphism $f \colon s.\mathrm{pt} \to X$ in $C$ that is an isomorphism, the cocone morphism $\mathrm{Cocones.extend}\, s\, f$ from $s$ to its extension $s.\mathrm{extend}\, f$ is also an isomorphism.

CategoryTheory.Limits.Cocones.precompose definition

{G : J ⥤ C} (α : G ⟶ F) : Cocone F ⥤ Cocone G

Full source

/-- Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone
for `G`. -/
@[simps]
def precompose {G : J ⥤ C} (α : G ⟶ F) : CoconeCocone F ⥤ Cocone G where
  obj c :=
    { pt := c.pt
      ι := α ≫ c.ι }
  map f := { hom := f.hom }

Precomposition of cocones by a natural transformation

Informal description

Given a natural transformation $\alpha : G \to F$ between functors $G, F : J \to C$, the functor `precompose` maps a cocone $c$ over $F$ to a cocone over $G$ by composing $\alpha$ with the cocone's natural transformation $c.\iota : F \to c.\text{pt}$, resulting in a new cocone with the same cocone point $c.\text{pt}$ and natural transformation $\alpha \circ c.\iota : G \to c.\text{pt}$.

CategoryTheory.Limits.Cocones.precomposeComp definition

{G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) : precompose (α ≫ β) ≅ precompose β ⋙ precompose α

Full source

/-- Precomposing a cocone by the composite natural transformation `α ≫ β` is the same as
precomposing by `β` and then by `α`. -/
def precomposeComp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) :
    precomposeprecompose (α ≫ β) ≅ precompose β ⋙ precompose α :=
  NatIso.ofComponents fun s => Cocones.ext (Iso.refl _)

Natural isomorphism between precomposition functors for cocones

Informal description

Given functors $ F, G, H : J \to C $ and natural transformations $ \alpha : F \to G $ and $ \beta : G \to H $, the functor obtained by precomposing cocones with the composite natural transformation $ \alpha \circ \beta $ is naturally isomorphic to the composition of the functors obtained by first precomposing with $ \beta $ and then with $ \alpha $.

CategoryTheory.Limits.Cocones.precomposeId definition

: precompose (𝟙 F) ≅ 𝟭 (Cocone F)

Full source

/-- Precomposing by the identity does not change the cocone up to isomorphism. -/
def precomposeId : precomposeprecompose (𝟙 F) ≅ 𝟭 (Cocone F) :=
  NatIso.ofComponents fun s => Cocones.ext (Iso.refl _)

Precomposition with identity preserves cocones up to isomorphism

Informal description

The functor that precomposes cocones over $F$ with the identity natural transformation $\text{id}_F$ is naturally isomorphic to the identity functor on the category of cocones over $F$.

CategoryTheory.Limits.Cocones.precomposeEquivalence definition

{G : J ⥤ C} (α : G ≅ F) : Cocone F ≌ Cocone G

Full source

/-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cocones.
-/
@[simps]
def precomposeEquivalence {G : J ⥤ C} (α : G ≅ F) : CoconeCocone F ≌ Cocone G where
  functor := precompose α.hom
  inverse := precompose α.inv
  unitIso := NatIso.ofComponents fun s => Cocones.ext (Iso.refl _)
  counitIso := NatIso.ofComponents fun s => Cocones.ext (Iso.refl _)

Equivalence of cocone categories under natural isomorphism of functors

Informal description

Given a natural isomorphism $\alpha \colon G \cong F$ between functors $G, F \colon J \to C$, the categories of cocones over $F$ and $G$ are equivalent. The equivalence is constructed by precomposing cocones with $\alpha$ and its inverse, with the unit and counit isomorphisms given by identity isomorphisms on the cocone points.

CategoryTheory.Limits.Cocones.whiskering definition

(E : K ⥤ J) : Cocone F ⥤ Cocone (E ⋙ F)

Full source

/-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cocone F` to `Cocone (E ⋙ F)`.
-/
@[simps]
def whiskering (E : K ⥤ J) : CoconeCocone F ⥤ Cocone (E ⋙ F) where
  obj c := c.whisker E
  map f := { hom := f.hom }

Whiskering functor for cocones by precomposition

Informal description

Given a functor $E \colon K \to J$, the whiskering functor $\text{Cocones.whiskering}\, E$ maps a cocone over $F \colon J \to C$ to a cocone over the composition $E \circ F \colon K \to C$ by precomposing with $E$. The functor acts on morphisms by preserving the underlying morphism between cocone points.

CategoryTheory.Limits.Cocones.whiskeringEquivalence definition

(e : K ≌ J) : Cocone F ≌ Cocone (e.functor ⋙ F)

Full source

/-- Whiskering by an equivalence gives an equivalence between categories of cones.
-/
@[simps]
def whiskeringEquivalence (e : K ≌ J) : CoconeCocone F ≌ Cocone (e.functor ⋙ F) where
  functor := whiskering e.functor
  inverse :=
    whiskering e.inverse ⋙
      precompose
        ((Functor.leftUnitor F).inv ≫
          whiskerRight e.counitIso.inv F ≫ (Functor.associator _ _ _).inv)
  unitIso := NatIso.ofComponents fun s => Cocones.ext (Iso.refl _)
  counitIso := NatIso.ofComponents fun s =>
    Cocones.ext (Iso.refl _) fun k => by simpa [e.counitInv_app_functor k] using s.w (e.unit.app k)

Equivalence of cocone categories under whiskering by an equivalence

Informal description

Given an equivalence of categories $e \colon K \simeq J$, the whiskering equivalence functor establishes an equivalence between the category of cocones over a functor $F \colon J \to C$ and the category of cocones over the composition $e.\text{functor} \circ F \colon K \to C$. The equivalence consists of: - A functor that precomposes a cocone over $F$ with $e.\text{functor}$ to obtain a cocone over $e.\text{functor} \circ F$. - An inverse functor that precomposes a cocone over $e.\text{functor} \circ F$ with $e.\text{inverse}$ and adjusts the natural transformation using the counit isomorphism of $e$. - Natural isomorphisms witnessing the equivalence, constructed using identity isomorphisms on the cocone points.

CategoryTheory.Limits.Cocones.equivalenceOfReindexing definition

{G : K ⥤ C} (e : K ≌ J) (α : e.functor ⋙ F ≅ G) : Cocone F ≌ Cocone G

Full source

/--
The categories of cocones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic
(possibly after changing the indexing category by an equivalence).
-/
@[simps! functor_obj]
def equivalenceOfReindexing {G : K ⥤ C} (e : K ≌ J) (α : e.functor ⋙ Fe.functor ⋙ F ≅ G) : CoconeCocone F ≌ Cocone G :=
  (whiskeringEquivalence e).trans (precomposeEquivalence α.symm)

Equivalence of cocone categories under reindexing and natural isomorphism

Informal description

Given an equivalence of categories $e \colon K \simeq J$ and a natural isomorphism $\alpha \colon e.\text{functor} \circ F \cong G$ between functors $F \colon J \to C$ and $G \colon K \to C$, the categories of cocones over $F$ and $G$ are equivalent. This equivalence is constructed by first whiskering with $e$ and then precomposing with $\alpha^{-1}$.

CategoryTheory.Limits.Cocones.forget definition

: Cocone F ⥤ C

Full source

/-- Forget the cocone structure and obtain just the cocone point. -/
@[simps]
def forget : CoconeCocone F ⥤ C where
  obj t := t.pt
  map f := f.hom

Forgetful functor from cocones to base category

Informal description

The forgetful functor from the category of cocones over a functor $F : J \to C$ to the base category $C$, which maps each cocone to its cocone point and each cocone morphism to its underlying morphism in $C$.

CategoryTheory.Limits.Cocones.functoriality definition

: Cocone F ⥤ Cocone (F ⋙ G)

Full source

/-- A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially. -/
@[simps]
def functoriality : CoconeCocone F ⥤ Cocone (F ⋙ G) where
  obj A :=
    { pt := G.obj A.pt
      ι :=
        { app := fun j => G.map (A.ι.app j)
          naturality := by intros; erw [← G.map_comp]; simp } }
  map f :=
    { hom := G.map f.hom
      w := by intros; rw [← Functor.map_comp, CoconeMorphism.w] }

Functoriality of cocones under composition with $G$

Informal description

Given a functor $G : C \to D$, the functoriality construction sends cocones over $F : J \to C$ to cocones over the composition $F \circ G : J \to D$. Specifically: - For a cocone $A$ over $F$, the cocone point becomes $G(A.\text{pt})$, and the cocone legs are given by $G$ applied to each leg $A.\iota_j$. - For a morphism $f$ between cocones over $F$, the corresponding morphism between the new cocones is $G(f.\text{hom})$. This construction yields a functor from the category of cocones over $F$ to the category of cocones over $F \circ G$.

CategoryTheory.Limits.Cocones.functorialityCompFunctoriality definition

(H : D ⥤ E) : functoriality F G ⋙ functoriality (F ⋙ G) H ≅ functoriality F (G ⋙ H)

Full source

/-- Functoriality is functorial. -/
def functorialityCompFunctoriality (H : D ⥤ E) :
    functorialityfunctoriality F G ⋙ functoriality (F ⋙ G) Hfunctoriality F G ⋙ functoriality (F ⋙ G) H ≅ functoriality F (G ⋙ H) :=
  NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp [functoriality])

Natural isomorphism between composed cocone functorialities

Informal description

Given functors $F : J \to C$, $G : C \to D$, and $H : D \to E$, there is a natural isomorphism between: 1. The composition of the functoriality constructions for $G$ followed by $H$ (applied to cocones over $F$ and then to cocones over $F \circ G$) 2. The functoriality construction for the composition $G \circ H$ (applied directly to cocones over $F$) This isomorphism is given componentwise by the identity isomorphisms on the cocone points, and it satisfies the naturality condition with respect to cocone morphisms.

CategoryTheory.Limits.Cocones.functoriality_full instance

[G.Full] [G.Faithful] : (functoriality F G).Full

Full source

instance functoriality_full [G.Full] [G.Faithful] : (functoriality F G).Full where
  map_surjective t :=
    ⟨{ hom := G.preimage t.hom
       w := fun j => G.map_injective (by simpa using t.w j) }, by aesop_cat⟩

Fullness of Cocone Functoriality for Fully Faithful Functors

Informal description

Given a fully faithful functor $G : C \to D$, the functoriality construction that sends cocones over $F : J \to C$ to cocones over $F \circ G : J \to D$ is a full functor. That is, for any two cocones $c$ and $c'$ over $F$, every morphism between their images under the functoriality construction is induced by a morphism between $c$ and $c'$.

CategoryTheory.Limits.Cocones.functoriality_faithful instance

[G.Faithful] : (functoriality F G).Faithful

Full source

instance functoriality_faithful [G.Faithful] : (functoriality F G).Faithful where
  map_injective {_X} {_Y} f g h :=
    CoconeMorphism.ext f g <| G.map_injective <| congr_arg CoconeMorphism.hom h

Faithfulness of Cocone Functoriality under Faithful Functors

Informal description

Given a faithful functor $G : C \to D$, the functoriality construction that sends cocones over $F : J \to C$ to cocones over $F \circ G : J \to D$ is also faithful. This means that for any two morphisms $f, g$ between cocones over $F$, if their images under the functoriality construction are equal, then $f = g$.

CategoryTheory.Limits.Cocones.functorialityEquivalence definition

(e : C ≌ D) : Cocone F ≌ Cocone (F ⋙ e.functor)

Full source

/-- If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cocones over `F` and cocones over `F ⋙ e.functor`.
-/
@[simps]
def functorialityEquivalence (e : C ≌ D) : CoconeCocone F ≌ Cocone (F ⋙ e.functor) :=
  let f : (F ⋙ e.functor) ⋙ e.inverse(F ⋙ e.functor) ⋙ e.inverse ≅ F :=
    Functor.associatorFunctor.associator _ _ _ ≪≫ isoWhiskerLeft _ e.unitIso.symm ≪≫ Functor.rightUnitor _
  { functor := functoriality F e.functor
    inverse := functorialityfunctoriality (F ⋙ e.functor) e.inverse ⋙ (precomposeEquivalence f.symm).functor
    unitIso := NatIso.ofComponents fun c => Cocones.ext (e.unitIso.app _)
    counitIso := NatIso.ofComponents fun c => Cocones.ext (e.counitIso.app _) }

Equivalence of cocone categories under composition with an equivalence of categories

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the functoriality construction induces an equivalence between the category of cocones over a functor $F \colon J \to C$ and the category of cocones over the composition $F \circ e.\text{functor} \colon J \to D$. Specifically, the equivalence consists of: - A functor sending a cocone $c$ over $F$ to the cocone over $F \circ e.\text{functor}$ with cocone point $e.\text{functor}(c.\text{pt})$ and legs given by applying $e.\text{functor}$ to each $c.\iota_j$. - An inverse functor constructed using the inverse equivalence $e.\text{inverse}$ and a natural isomorphism $F \circ e.\text{functor} \circ e.\text{inverse} \cong F$. - Natural isomorphisms witnessing the equivalence, induced by the unit and counit of $e$.

CategoryTheory.Limits.Cocones.reflects_cocone_isomorphism instance

(F : C ⥤ D) [F.ReflectsIsomorphisms] (K : J ⥤ C) : (Cocones.functoriality K F).ReflectsIsomorphisms

Full source

/-- If `F` reflects isomorphisms, then `Cocones.functoriality F` reflects isomorphisms
as well.
-/
instance reflects_cocone_isomorphism (F : C ⥤ D) [F.ReflectsIsomorphisms] (K : J ⥤ C) :
    (Cocones.functoriality K F).ReflectsIsomorphisms := by
  constructor
  intro A B f _
  haveI : IsIso (F.map f.hom) :=
    (Cocones.forget (K ⋙ F)).map_isIso ((Cocones.functoriality K F).map f)
  haveI := ReflectsIsomorphisms.reflects F f.hom
  apply cocone_iso_of_hom_iso

Reflection of Isomorphisms in Cocone Functoriality

Informal description

For any functor $F \colon C \to D$ that reflects isomorphisms and any functor $K \colon J \to C$, the functoriality construction that sends cocones over $K$ to cocones over $K \circ F$ also reflects isomorphisms. That is, if a morphism of cocones becomes an isomorphism after applying the functoriality construction, then it was already an isomorphism in the original category of cocones.

CategoryTheory.Functor.mapCone definition

(c : Cone F) : Cone (F ⋙ H)

Full source

/-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/
@[simps!]
def mapCone (c : Cone F) : Cone (F ⋙ H) :=
  (Cones.functoriality F H).obj c

Image of a cone under a functor

Informal description

Given a functor $H \colon C \to D$ and a cone $c$ over a functor $F \colon J \to C$, the image of $c$ under $H$ is a cone over the composition $F \circ H \colon J \to D$. This cone has: - Cone point $H(c.\mathrm{pt})$ - Natural transformation with components $H(c.\pi_j)$ for each $j \in J$

CategoryTheory.Functor.mapConeMapCone definition

{F : J ⥤ C} {H : C ⥤ D} {H' : D ⥤ E} (c : Cone F) : H'.mapCone (H.mapCone c) ≅ (H ⋙ H').mapCone c

Full source

/-- The construction `mapCone` respects functor composition. -/
@[simps!]
noncomputable def mapConeMapCone {F : J ⥤ C} {H : C ⥤ D} {H' : D ⥤ E} (c : Cone F) :
    H'.mapCone (H.mapCone c) ≅ (H ⋙ H').mapCone c := Cones.ext (Iso.refl _)

Functoriality of cone mapping under functor composition

Informal description

Given functors $F \colon J \to C$, $H \colon C \to D$, and $H' \colon D \to E$, and a cone $c$ over $F$, the image of $c$ under $H'$ composed with $H$ is naturally isomorphic to the image of $c$ under the composition $H \circ H'$. Specifically, the isomorphism is given by the identity morphism on the cone point.

CategoryTheory.Functor.mapCocone definition

(c : Cocone F) : Cocone (F ⋙ H)

Full source

/-- The image of a cocone in C under a functor G : C ⥤ D is a cocone in D. -/
@[simps!]
def mapCocone (c : Cocone F) : Cocone (F ⋙ H) :=
  (Cocones.functoriality F H).obj c

Image of a cocone under a functor

Informal description

Given a functor $H : C \to D$ and a cocone $c$ over a functor $F : J \to C$, the image of $c$ under $H$ is a cocone over the composition $F \circ H : J \to D$. Specifically: - The cocone point is $H(c.\text{pt})$ - The cocone legs are given by $H$ applied to each leg $c.\iota_j$ of the original cocone. This construction preserves the cocone structure, ensuring that the naturality conditions are maintained.

CategoryTheory.Functor.mapCoconeMapCocone definition

{F : J ⥤ C} {H : C ⥤ D} {H' : D ⥤ E} (c : Cocone F) : H'.mapCocone (H.mapCocone c) ≅ (H ⋙ H').mapCocone c

Full source

/-- The construction `mapCocone` respects functor composition. -/
@[simps!]
noncomputable def mapCoconeMapCocone {F : J ⥤ C} {H : C ⥤ D} {H' : D ⥤ E} (c : Cocone F) :
    H'.mapCocone (H.mapCocone c) ≅ (H ⋙ H').mapCocone c := Cocones.ext (Iso.refl _)

Functoriality of cocone mapping under composition

Informal description

Given functors $H : C \to D$ and $H' : D \to E$, and a cocone $c$ over a functor $F : J \to C$, the image of $c$ under $H' \circ H$ is naturally isomorphic to the image of $H.mapCocone(c)$ under $H'$. Specifically, the cocone point and legs are preserved up to isomorphism by the functor composition.

CategoryTheory.Functor.mapConeMorphism definition

{c c' : Cone F} (f : c ⟶ c') : H.mapCone c ⟶ H.mapCone c'

Full source

/-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially. -/
def mapConeMorphism {c c' : Cone F} (f : c ⟶ c') : H.mapCone c ⟶ H.mapCone c' :=
  (Cones.functoriality F H).map f

Image of a cone morphism under a functor

Informal description

Given a morphism $f \colon c \to c'$ between cones over a functor $F \colon J \to C$, the functor $H \colon C \to D$ induces a morphism $H(f) \colon H(c) \to H(c')$ between the images of these cones under $H$. This morphism is constructed functorially, ensuring that the cone structure is preserved.

CategoryTheory.Functor.mapCoconeMorphism definition

{c c' : Cocone F} (f : c ⟶ c') : H.mapCocone c ⟶ H.mapCocone c'

Full source

/-- Given a cocone morphism `c ⟶ c'`, construct a cocone morphism on the mapped cocones
functorially. -/
def mapCoconeMorphism {c c' : Cocone F} (f : c ⟶ c') : H.mapCocone c ⟶ H.mapCocone c' :=
  (Cocones.functoriality F H).map f

Functorial image of a cocone morphism

Informal description

Given a functor $H : C \to D$ and a morphism $f : c \to c'$ between cocones over a functor $F : J \to C$, this constructs the induced morphism between the images of these cocones under $H$. Specifically, it produces a morphism $H(c) \to H(c')$ in the category of cocones over $F \circ H : J \to D$, where: - The underlying morphism of cocone points is $H(f.\text{hom}) : H(c.\text{pt}) \to H(c'.\text{pt})$ - The naturality condition is preserved by functoriality

CategoryTheory.Functor.mapConeInv definition

[IsEquivalence H] (c : Cone (F ⋙ H)) : Cone F

Full source

/-- If `H` is an equivalence, we invert `H.mapCone` and get a cone for `F` from a cone
for `F ⋙ H`. -/
noncomputable def mapConeInv [IsEquivalence H] (c : Cone (F ⋙ H)) : Cone F :=
  (Limits.Cones.functorialityEquivalence F (asEquivalence H)).inverse.obj c

Inverse image of a cone under an equivalence of categories

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cone $c$ over the composition $F \circ H \colon J \to C$, the construction `mapConeInv` produces a cone over the original functor $F \colon J \to D$. This is achieved by applying the inverse functor of the equivalence to the cone point and the components of the natural transformation, thus inverting the effect of `H.mapCone`.

CategoryTheory.Functor.mapConeMapConeInv definition

{F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cone (F ⋙ H)) : mapCone H (mapConeInv H c) ≅ c

Full source

/-- `mapCone` is the left inverse to `mapConeInv`. -/
noncomputable def mapConeMapConeInv {F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H]
    (c : Cone (F ⋙ H)) :
    mapConemapCone H (mapConeInv H c) ≅ c :=
  (Limits.Cones.functorialityEquivalence F (asEquivalence H)).counitIso.app c

Natural isomorphism between composed cone mappings under equivalence

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cone $c$ over the composition $F \circ H \colon J \to C$, the composition of the functorial mappings `mapCone H` and `mapConeInv H` yields a cone that is naturally isomorphic to the original cone $c$. More precisely, for any cone $c$ over $F \circ H$, there exists a natural isomorphism between the cone obtained by first applying the inverse image construction `mapConeInv H` followed by the direct image construction `mapCone H`, and the original cone $c$.

CategoryTheory.Functor.mapConeInvMapCone definition

{F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cone F) : mapConeInv H (mapCone H c) ≅ c

Full source

/-- `MapCone` is the right inverse to `mapConeInv`. -/
noncomputable def mapConeInvMapCone {F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cone F) :
    mapConeInvmapConeInv H (mapCone H c) ≅ c :=
  (Limits.Cones.functorialityEquivalence F (asEquivalence H)).unitIso.symm.app c

Inverse image of image of a cone under equivalence is isomorphic to original cone

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cone $c$ over a functor $F \colon J \to D$, the composition of applying $H$ to $c$ and then inverting the result via $H^{-1}$ is naturally isomorphic to the original cone $c$. More precisely, the isomorphism is given by the inverse of the unit isomorphism from the equivalence of cone categories induced by $H$.

CategoryTheory.Functor.mapCoconeInv definition

[IsEquivalence H] (c : Cocone (F ⋙ H)) : Cocone F

Full source

/-- If `H` is an equivalence, we invert `H.mapCone` and get a cone for `F` from a cone
for `F ⋙ H`. -/
noncomputable def mapCoconeInv [IsEquivalence H] (c : Cocone (F ⋙ H)) : Cocone F :=
  (Limits.Cocones.functorialityEquivalence F (asEquivalence H)).inverse.obj c

Inverse image of a cocone under an equivalence of categories

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cocone $c$ over the composed functor $F \circ H \colon J \to C$, the construction `mapCoconeInv` produces a cocone over the original functor $F \colon J \to D$. This is achieved by applying the inverse functor of the equivalence between the categories of cocones induced by $H$.

CategoryTheory.Functor.mapCoconeMapCoconeInv definition

{F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cocone (F ⋙ H)) : mapCocone H (mapCoconeInv H c) ≅ c

Full source

/-- `mapCocone` is the left inverse to `mapCoconeInv`. -/
noncomputable def mapCoconeMapCoconeInv {F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H]
    (c : Cocone (F ⋙ H)) :
    mapCoconemapCocone H (mapCoconeInv H c) ≅ c :=
  (Limits.Cocones.functorialityEquivalence F (asEquivalence H)).counitIso.app c

Isomorphism between cocone and its image under equivalence functor composition

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cocone $c$ over the composed functor $F \circ H \colon J \to D$, the image of the inverse image of $c$ under $H$ is isomorphic to $c$ itself. More precisely, the composition of the functors `mapCocone H` and `mapCoconeInv H` applied to $c$ yields a cocone that is naturally isomorphic to $c$.

CategoryTheory.Functor.mapCoconeInvMapCocone definition

{F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cocone F) : mapCoconeInv H (mapCocone H c) ≅ c

Full source

/-- `mapCocone` is the right inverse to `mapCoconeInv`. -/
noncomputable def mapCoconeInvMapCocone {F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H] (c : Cocone F) :
    mapCoconeInvmapCoconeInv H (mapCocone H c) ≅ c :=
  (Limits.Cocones.functorialityEquivalence F (asEquivalence H)).unitIso.symm.app c

Inverse image of mapped cocone is isomorphic to original cocone

Informal description

Given an equivalence of categories $H \colon D \to C$ and a cocone $c$ over a functor $F \colon J \to D$, the composition of the functoriality constructions `mapCocone` followed by `mapCoconeInv` yields a cocone that is naturally isomorphic to the original cocone $c$. More precisely, the isomorphism is given by the inverse of the unit isomorphism from the equivalence between the categories of cocones induced by $H$.

CategoryTheory.Functor.functorialityCompPostcompose definition

 {H H' : C ⥤ D} (α : H ≅ H') :
  Cones.functoriality F H ⋙ Cones.postcompose (whiskerLeft F α.hom) ≅ Cones.functoriality F H'

Full source

/-- `functoriality F _ ⋙ postcompose (whisker_left F _)` simplifies to `functoriality F _`. -/
@[simps!]
def functorialityCompPostcompose {H H' : C ⥤ D} (α : H ≅ H') :
    Cones.functorialityCones.functoriality F H ⋙ Cones.postcompose (whiskerLeft F α.hom)Cones.functoriality F H ⋙ Cones.postcompose (whiskerLeft F α.hom) ≅ Cones.functoriality F H' :=
  NatIso.ofComponents fun c => Cones.ext (α.app _)

Isomorphism between functoriality constructions of cones via natural isomorphism

Informal description

Given an isomorphism $\alpha \colon H \cong H'$ between functors $H, H' \colon C \to D$, the composition of the functoriality of cones under $H$ with the postcomposition by the left whiskering of $\alpha$ is naturally isomorphic to the functoriality of cones under $H'$. More precisely, for any cone $c$ over $F$, the isomorphism $\alpha$ induces an isomorphism between the cones obtained via the two different functorial constructions.

CategoryTheory.Functor.postcomposeWhiskerLeftMapCone definition

 {H H' : C ⥤ D} (α : H ≅ H') (c : Cone F) : (Cones.postcompose (whiskerLeft F α.hom :)).obj (mapCone H c) ≅ mapCone H' c

Full source

/-- For `F : J ⥤ C`, given a cone `c : Cone F`, and a natural isomorphism `α : H ≅ H'` for functors
`H H' : C ⥤ D`, the postcomposition of the cone `H.mapCone` using the isomorphism `α` is
isomorphic to the cone `H'.mapCone`.
-/
@[simps!]
def postcomposeWhiskerLeftMapCone {H H' : C ⥤ D} (α : H ≅ H') (c : Cone F) :
    (Cones.postcompose (whiskerLeft F α.hom :)).obj (mapCone H c) ≅ mapCone H' c :=
  (functorialityCompPostcompose α).app c

Isomorphism between postcomposed and directly mapped cones via natural isomorphism

Informal description

Given a natural isomorphism $\alpha \colon H \cong H'$ between functors $H, H' \colon C \to D$ and a cone $c$ over a functor $F \colon J \to C$, the cone obtained by first applying $H$ to $c$ and then postcomposing with the left whiskering of $\alpha$ is isomorphic to the cone obtained by directly applying $H'$ to $c$. More precisely, the isomorphism is given by the component at $c$ of the natural isomorphism between the functoriality constructions.

CategoryTheory.Functor.mapConePostcompose definition

 {α : F ⟶ G} {c} : mapCone H ((Cones.postcompose α).obj c) ≅ (Cones.postcompose (whiskerRight α H :)).obj (mapCone H c)

Full source

/--
`mapCone` commutes with `postcompose`. In particular, for `F : J ⥤ C`, given a cone `c : Cone F`, a
natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious ways of producing
a cone over `G ⋙ H`, and they are both isomorphic.
-/
@[simps!]
def mapConePostcompose {α : F ⟶ G} {c} :
    mapConemapCone H ((Cones.postcompose α).obj c) ≅
      (Cones.postcompose (whiskerRight α H :)).obj (mapCone H c) :=
  Cones.ext (Iso.refl _)

Isomorphism between postcomposed and whiskered cones under functor application

Informal description

Given a natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon J \to C$, a cone $c$ over $F$, and a functor $H \colon C \to D$, the image of the postcomposed cone $(Cones.postcompose \alpha).obj c$ under $H$ is isomorphic to the cone obtained by postcomposing the image of $c$ under $H$ with the whiskering of $\alpha$ by $H$ on the right. More precisely, there is a natural isomorphism: $$ H(\text{postcompose}(\alpha)(c)) \cong \text{postcompose}(\alpha \circ H)(H(c)) $$ where: - $\text{postcompose}(\alpha)(c)$ is the cone over $G$ obtained by postcomposing $c$'s natural transformation with $\alpha$ - $H(c)$ is the image of the cone $c$ under $H$ - $\alpha \circ H$ is the right whiskering of $\alpha$ by $H$

CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor definition

 {α : F ≅ G} {c} :
  mapCone H ((Cones.postcomposeEquivalence α).functor.obj c) ≅
    (Cones.postcomposeEquivalence (isoWhiskerRight α H :)).functor.obj (mapCone H c)

Full source

/-- `mapCone` commutes with `postcomposeEquivalence`
-/
@[simps!]
def mapConePostcomposeEquivalenceFunctor {α : F ≅ G} {c} :
    mapConemapCone H ((Cones.postcomposeEquivalence α).functor.obj c) ≅
      (Cones.postcomposeEquivalence (isoWhiskerRight α H :)).functor.obj (mapCone H c) :=
  Cones.ext (Iso.refl _)

Naturality of cone equivalence under functor application

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 functor $H \colon C \to D$, the image under $H$ of the cone obtained by applying the equivalence functor from $\text{Cones}(F)$ to $\text{Cones}(G)$ to $c$ is isomorphic to the cone obtained by first applying $H$ to $c$ and then applying the equivalence functor from $\text{Cones}(F \circ H)$ to $\text{Cones}(G \circ H)$. More precisely, there is a natural isomorphism: $$ H(\text{postcomposeEquivalence}(\alpha)(c)) \cong \text{postcomposeEquivalence}(\alpha \circ H)(H(c)) $$ where: - $\text{postcomposeEquivalence}(\alpha)$ is the equivalence between cone categories induced by $\alpha$ - $\alpha \circ H$ is the right whiskering of $\alpha$ by $H$

CategoryTheory.Functor.functorialityCompPrecompose definition

 {H H' : C ⥤ D} (α : H ≅ H') :
  Cocones.functoriality F H ⋙ Cocones.precompose (whiskerLeft F α.inv) ≅ Cocones.functoriality F H'

Full source

/-- `functoriality F _ ⋙ precompose (whiskerLeft F _)` simplifies to `functoriality F _`. -/
@[simps!]
def functorialityCompPrecompose {H H' : C ⥤ D} (α : H ≅ H') :
    Cocones.functorialityCocones.functoriality F H ⋙ Cocones.precompose (whiskerLeft F α.inv)Cocones.functoriality F H ⋙ Cocones.precompose (whiskerLeft F α.inv) ≅
      Cocones.functoriality F H' :=
  NatIso.ofComponents fun c => Cocones.ext (α.app _)

Natural isomorphism between functoriality and precomposition of cocones under functor isomorphism

Informal description

Given an isomorphism $\alpha \colon H \cong H'$ between functors $H, H' \colon C \to D$, there is a natural isomorphism between the composition of the cocone functoriality with respect to $H$ followed by precomposition with the whiskering of $\alpha^{-1}$ on the left by $F$, and the cocone functoriality with respect to $H'$. More precisely, for any cocone $c$ over $F$, the isomorphism is given by $\alpha$ applied to the cocone point of $c$.

CategoryTheory.Functor.precomposeWhiskerLeftMapCocone definition

 {H H' : C ⥤ D} (α : H ≅ H') (c : Cocone F) :
  (Cocones.precompose (whiskerLeft F α.inv :)).obj (mapCocone H c) ≅ mapCocone H' c

Full source

/--
For `F : J ⥤ C`, given a cocone `c : Cocone F`, and a natural isomorphism `α : H ≅ H'` for functors
`H H' : C ⥤ D`, the precomposition of the cocone `H.mapCocone` using the isomorphism `α` is
isomorphic to the cocone `H'.mapCocone`.
-/
@[simps!]
def precomposeWhiskerLeftMapCocone {H H' : C ⥤ D} (α : H ≅ H') (c : Cocone F) :
    (Cocones.precompose (whiskerLeft F α.inv :)).obj (mapCocone H c) ≅ mapCocone H' c :=
  (functorialityCompPrecompose α).app c

Isomorphism between precomposed whiskered cocone and mapped cocone under functor isomorphism

Informal description

Given an isomorphism $\alpha \colon H \cong H'$ between functors $H, H' \colon C \to D$ and a cocone $c$ over a functor $F \colon J \to C$, the cocone obtained by first mapping $c$ through $H$ and then precomposing with the whiskering of $\alpha^{-1}$ on the left by $F$ is isomorphic to the cocone obtained by directly mapping $c$ through $H'$. More precisely, for any cocone $c$ over $F$, the isomorphism is given by $\alpha$ applied to the cocone point of $c$, ensuring that the naturality conditions are preserved.

CategoryTheory.Functor.mapCoconePrecompose definition

 {α : F ⟶ G} {c} :
  mapCocone H ((Cocones.precompose α).obj c) ≅ (Cocones.precompose (whiskerRight α H :)).obj (mapCocone H c)

Full source

/-- `map_cocone` commutes with `precompose`. In particular, for `F : J ⥤ C`, given a cocone
`c : Cocone F`, a natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious
ways of producing a cocone over `G ⋙ H`, and they are both isomorphic.
-/
@[simps!]
def mapCoconePrecompose {α : F ⟶ G} {c} :
    mapCoconemapCocone H ((Cocones.precompose α).obj c) ≅
      (Cocones.precompose (whiskerRight α H :)).obj (mapCocone H c) :=
  Cocones.ext (Iso.refl _)

Compatibility of cocone mapping with precomposition

Informal description

Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon J \to C$, a cocone $c$ over $G$, and a functor $H \colon C \to D$, the image under $H$ of the precomposition of $c$ with $\alpha$ is isomorphic to the precomposition with $\alpha \circ H$ of the image under $H$ of $c$. More precisely, there is a natural isomorphism between: 1. The cocone obtained by first precomposing $c$ with $\alpha$ and then applying $H$ to the resulting cocone over $F$ 2. The cocone obtained by first applying $H$ to $c$ and then precomposing with the whiskering of $\alpha$ by $H$ The isomorphism is given by the identity morphism on the cocone point $H(c.\text{pt})$.

CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor definition

 {α : F ≅ G} {c} :
  mapCocone H ((Cocones.precomposeEquivalence α).functor.obj c) ≅
    (Cocones.precomposeEquivalence (isoWhiskerRight α H :)).functor.obj (mapCocone H c)

Full source

/-- `mapCocone` commutes with `precomposeEquivalence`
-/
@[simps!]
def mapCoconePrecomposeEquivalenceFunctor {α : F ≅ G} {c} :
    mapCoconemapCocone H ((Cocones.precomposeEquivalence α).functor.obj c) ≅
      (Cocones.precomposeEquivalence (isoWhiskerRight α H :)).functor.obj (mapCocone H c) :=
  Cocones.ext (Iso.refl _)

Compatibility of cocone mapping with precomposition equivalence

Informal description

Given a natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon J \to C$, a functor $H \colon C \to D$, and a cocone $c$ over $F$, the image of the cocone $(Cocones.precomposeEquivalence \alpha).functor.obj c$ under $H$ is isomorphic to the cocone obtained by first mapping $c$ under $H$ and then applying the precomposition equivalence induced by the whiskered isomorphism $\alpha \circ H \colon F \circ H \cong G \circ H$.

CategoryTheory.Functor.mapConeWhisker definition

{E : K ⥤ J} {c : Cone F} : mapCone H (c.whisker E) ≅ (mapCone H c).whisker E

Full source

/-- `mapCone` commutes with `whisker`
-/
@[simps!]
def mapConeWhisker {E : K ⥤ J} {c : Cone F} : mapConemapCone H (c.whisker E) ≅ (mapCone H c).whisker E :=
  Cones.ext (Iso.refl _)

Natural isomorphism between whiskered image cones

Informal description

Given functors $F \colon J \to C$, $H \colon C \to D$, and $E \colon K \to J$, and a cone $c$ over $F$, the image of the whiskered cone $c.\text{whisker}\, E$ under $H$ is naturally isomorphic to the whiskering of the image cone $H(c)$ by $E$. More precisely, there is a natural isomorphism: $$ H(c.\text{whisker}\, E) \cong (H(c)).\text{whisker}\, E $$ where: - $c.\text{whisker}\, E$ is the cone over $E \circ F$ obtained by precomposing $c$ with $E$ - $H(c)$ is the image of $c$ under $H$ (a cone over $F \circ H$) - $(H(c)).\text{whisker}\, E$ is the whiskering of $H(c)$ by $E$ (a cone over $E \circ F \circ H$)

CategoryTheory.Functor.mapCoconeWhisker definition

{E : K ⥤ J} {c : Cocone F} : mapCocone H (c.whisker E) ≅ (mapCocone H c).whisker E

Full source

/-- `mapCocone` commutes with `whisker`
-/
@[simps!]
def mapCoconeWhisker {E : K ⥤ J} {c : Cocone F} :
    mapCoconemapCocone H (c.whisker E) ≅ (mapCocone H c).whisker E :=
  Cocones.ext (Iso.refl _)

Natural isomorphism between whiskering and mapping cocones

Informal description

Given a functor $H \colon C \to D$, a functor $E \colon K \to J$, and a cocone $c$ over a functor $F \colon J \to C$, the image of the whiskered cocone $c.\text{whisker}\, E$ under $H$ is naturally isomorphic to the whiskering of the image cocone $H(c)$ by $E$. More precisely, there is a natural isomorphism between: 1. The cocone obtained by first whiskering $c$ with $E$ and then applying $H$ 2. The cocone obtained by first applying $H$ to $c$ and then whiskering with $E$ This isomorphism is witnessed by the identity morphism on the cocone point $H(c.\text{pt})$.

CategoryTheory.Limits.Cocone.op definition

(c : Cocone F) : Cone F.op

Full source

/-- Change a `Cocone F` into a `Cone F.op`. -/
@[simps]
def Cocone.op (c : Cocone F) : Cone F.op where
  pt := Opposite.op c.pt
  π := NatTrans.op c.ι

Opposite cocone as a cone

Informal description

Given a cocone `c` over a functor `F : J ⥤ C`, the operation `Cocone.op` constructs a cone over the opposite functor `F.op : Jᵒᵖ ⥤ Cᵒᵖ` by: - Taking the cocone point `c.pt` and considering it as an object in the opposite category `Cᵒᵖ` via `Opposite.op c.pt` - Transforming the cocone's natural transformation `c.ι : F ⟶ c.pt` into a natural transformation `NatTrans.op c.ι : Δ(c.pt) ⟶ F.op` for the cone

CategoryTheory.Limits.Cone.op definition

(c : Cone F) : Cocone F.op

Full source

/-- Change a `Cone F` into a `Cocone F.op`. -/
@[simps]
def Cone.op (c : Cone F) : Cocone F.op where
  pt := Opposite.op c.pt
  ι := NatTrans.op c.π

Opposite cone as a cocone

Informal description

Given a cone $c$ over a functor $F \colon J \to C$, the operation $\mathrm{Cone.op}$ constructs a cocone over the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$ by: - Taking the cone point $c.\mathrm{pt}$ and considering it as an object in the opposite category $C^{\mathrm{op}}$ via $\mathrm{Opposite.op}\, c.\mathrm{pt}$ - Transforming the cone's natural transformation $c.\pi \colon \Delta(c.\mathrm{pt}) \Rightarrow F$ into a natural transformation $\mathrm{NatTrans.op}\, c.\pi \colon F^{\mathrm{op}} \Rightarrow \Delta(\mathrm{Opposite.op}\, c.\mathrm{pt})$ for the cocone.

CategoryTheory.Limits.Cocone.unop definition

(c : Cocone F.op) : Cone F

Full source

/-- Change a `Cocone F.op` into a `Cone F`. -/
@[simps]
def Cocone.unop (c : Cocone F.op) : Cone F where
  pt := Opposite.unop c.pt
  π := NatTrans.removeOp c.ι

Cone from opposite cocone

Informal description

Given a cocone $c$ over the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$, this constructs a cone over $F \colon J \to C$ by: - Taking the cocone point $c.\mathrm{pt}$ in $C^{\mathrm{op}}$ and applying the unopposite operation to obtain an object in $C$ - Transforming the cocone's natural transformation $c.\iota \colon F^{\mathrm{op}} \Rightarrow \Delta(c.\mathrm{pt})$ into a natural transformation $\Delta(\mathrm{Opposite.unop}\, c.\mathrm{pt}) \Rightarrow F$ for the cone.

CategoryTheory.Limits.Cone.unop definition

(c : Cone F.op) : Cocone F

Full source

/-- Change a `Cone F.op` into a `Cocone F`. -/
@[simps]
def Cone.unop (c : Cone F.op) : Cocone F where
  pt := Opposite.unop c.pt
  ι := NatTrans.removeOp c.π

Cocone from opposite cone

Informal description

Given a cone $c$ over the opposite functor $F^{\mathrm{op}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$, this constructs a cocone over $F \colon J \to C$ by: - Taking the cone point $c.\mathrm{pt}$ in $C^{\mathrm{op}}$ and applying the unopposite operation to obtain an object in $C$ - Transforming the cone's natural transformation $c.\pi \colon \Delta(c.\mathrm{pt}) \Rightarrow F^{\mathrm{op}}$ into a natural transformation $\mathrm{NatTrans.removeOp}\, c.\pi \colon F \Rightarrow \Delta(\mathrm{Opposite.unop}\, c.\mathrm{pt})$ for the cocone.

CategoryTheory.Limits.coconeEquivalenceOpConeOp definition

: Cocone F ≌ (Cone F.op)ᵒᵖ

Full source

/-- The category of cocones on `F`
is equivalent to the opposite category of
the category of cones on the opposite of `F`.
-/
def coconeEquivalenceOpConeOp : CoconeCocone F ≌ (Cone F.op)ᵒᵖ where
  functor :=
    { obj := fun c => op (Cocone.op c)
      map := fun {X} {Y} f =>
        Quiver.Hom.op
          { hom := f.hom.op
            w := fun j => by
              apply Quiver.Hom.unop_inj
              dsimp
              apply CoconeMorphism.w } }
  inverse :=
    { obj := fun c => Cone.unop (unop c)
      map := fun {X} {Y} f =>
        { hom := f.unop.hom.unop
          w := fun j => by
            apply Quiver.Hom.op_inj
            dsimp
            apply ConeMorphism.w } }
  unitIso := NatIso.ofComponents (fun c => Cocones.ext (Iso.refl _))
  counitIso :=
    NatIso.ofComponents
      (fun c => (Cones.ext (Iso.refl c.unop.pt)).op)
      fun {X} {Y} f =>
      Quiver.Hom.unop_inj (ConeMorphism.ext _ _ (by simp))
  functor_unitIso_comp c := by
    apply Quiver.Hom.unop_inj
    apply ConeMorphism.ext
    dsimp
    apply comp_id

Equivalence between cocones and opposite cones

Informal description

The category of cocones over a functor $F$ is equivalent to the opposite category of the category of cones over the opposite functor $F^{\mathrm{op}}$.

CategoryTheory.Limits.coneOfCoconeLeftOp definition

(c : Cocone F.leftOp) : Cone F

Full source

/-- Change a cocone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
@[simps!]
def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F where
  pt := op c.pt
  π := NatTrans.removeLeftOp c.ι

Cone from cocone over left opposite functor

Informal description

Given a cocone $c$ over the left opposite functor $F^{\mathrm{leftOp}} \colon J^{\mathrm{op}} \to C$, this constructs a cone over the original functor $F \colon J \to C^{\mathrm{op}}$ by: - Taking the cocone point $c.\mathrm{pt}$ in $C$ and applying the opposite operation to obtain an object in $C^{\mathrm{op}}$ - Transforming the cocone's natural transformation $c.\iota \colon F^{\mathrm{leftOp}} \Rightarrow \Delta(c.\mathrm{pt})$ into a natural transformation $\mathrm{NatTrans.removeLeftOp}\, c.\iota \colon \Delta(\mathrm{op}\, c.\mathrm{pt}) \Rightarrow F$ for the cone.

CategoryTheory.Limits.coconeLeftOpOfCone definition

(c : Cone F) : Cocone F.leftOp

Full source

/-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.leftOp : Jᵒᵖ ⥤ C`. -/
@[simps!]
def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp where
  pt := unop c.pt
  ι := NatTrans.leftOp c.π

Cocone from cone via left opposite functor

Informal description

Given a cone $c$ over a functor $F \colon J \to C^{\mathrm{op}}$, the construction produces a cocone over the left opposite functor $F^{\mathrm{leftOp}} \colon J^{\mathrm{op}} \to C$. The cocone point is $\mathrm{unop}(c.\mathrm{pt})$, and the natural transformation is obtained by applying the left opposite operation to $c.\pi$.

CategoryTheory.Limits.coconeOfConeLeftOp definition

(c : Cone F.leftOp) : Cocone F

Full source

/-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
@[simps pt]
def coconeOfConeLeftOp (c : Cone F.leftOp) : Cocone F where
  pt := op c.pt
  ι := NatTrans.removeLeftOp c.π

Cocone from cone over left opposite functor

Informal description

Given a cone $c$ over the left opposite functor $F^{\mathrm{leftOp}} \colon J^{\mathrm{op}} \to C$, this constructs a cocone over the original functor $F \colon J \to C^{\mathrm{op}}$ by: - Taking the cone point $c.\mathrm{pt}$ in $C$ and applying the opposite operation to obtain an object in $C^{\mathrm{op}}$ - Transforming the cone's natural transformation $c.\pi \colon \Delta(c.\mathrm{pt}) \Rightarrow F^{\mathrm{leftOp}}$ into a natural transformation $\mathrm{removeLeftOp}(c.\pi) \colon F \Rightarrow \Delta(\mathrm{op}\, c.\mathrm{pt})$ for the cocone.

CategoryTheory.Limits.coconeOfConeLeftOp_ι_app theorem

(c : Cone F.leftOp) (j) : (coconeOfConeLeftOp c).ι.app j = (c.π.app (op j)).op

Full source

@[simp]
theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) :
    (coconeOfConeLeftOp c).ι.app j = (c.π.app (op j)).op := by
  dsimp only [coconeOfConeLeftOp]
  simp

Component equality for cocone from cone over left opposite functor

Informal description

Given a cone $c$ over the left opposite functor $F^{\mathrm{leftOp}} \colon J^{\mathrm{op}} \to C$, the component of the cocone's natural transformation at object $j$ in $J$ is equal to the opposite of the cone's natural transformation component at the opposite object $\mathrm{op}(j)$ in $J^{\mathrm{op}}$. That is, for any $j \in J$, we have: $$(coconeOfConeLeftOp\, c).\iota_j = (c.\pi_{\mathrm{op}(j)})^{\mathrm{op}}$$

CategoryTheory.Limits.coneLeftOpOfCocone definition

(c : Cocone F) : Cone F.leftOp

Full source

/-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.leftOp : Jᵒᵖ ⥤ C`. -/
@[simps!]
def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp where
  pt := unop c.pt
  π := NatTrans.leftOp c.ι

Conversion from cocone to cone via left opposite functor

Informal description

Given a cocone `c` over a functor `F : J ⥤ Cᵒᵖ`, this constructs a cone over the left opposite functor `F.leftOp : Jᵒᵖ ⥤ C`. The cone point is given by the unopposite of the cocone point `c.pt`, and the natural transformation is obtained by applying the left opposite operation to the cocone's natural transformation `c.ι`.

CategoryTheory.Limits.coneOfCoconeRightOp definition

(c : Cocone F.rightOp) : Cone F

Full source

/-- Change a cocone on `F.rightOp : J ⥤ Cᵒᵖ` to a cone on `F : Jᵒᵖ ⥤ C`. -/
@[simps]
def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F where
  pt := unop c.pt
  π := NatTrans.removeRightOp c.ι

Conversion from cocone over right opposite functor to cone over original functor

Informal description

Given a cocone $c$ over the right opposite functor $F^{\mathrm{rightOp}} \colon J \to C^{\mathrm{op}}$, this constructs a cone over the original functor $F \colon J^{\mathrm{op}} \to C$. The cone point is obtained by applying the unopposite operation to the cocone point $c.\mathrm{pt}$, and the natural transformation is constructed by removing the right opposite operation from the cocone's natural transformation $c.\iota$.

CategoryTheory.Limits.coconeRightOpOfCone definition

(c : Cone F) : Cocone F.rightOp

Full source

/-- Change a cone on `F : Jᵒᵖ ⥤ C` to a cocone on `F.rightOp : Jᵒᵖ ⥤ C`. -/
@[simps]
def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp where
  pt := op c.pt
  ι := NatTrans.rightOp c.π

Cocone from cone via right opposite functor

Informal description

Given a cone $c$ over a functor $F \colon J^{\mathrm{op}} \to C$, this constructs a cocone over the right opposite functor $F^{\mathrm{rightOp}} \colon J \to C^{\mathrm{op}}$. The cocone point is the opposite object of the cone point $c.\mathrm{pt}$, and the natural transformation is obtained by applying the right opposite operation to the cone's natural transformation $c.\pi$.

CategoryTheory.Limits.coconeOfConeRightOp definition

(c : Cone F.rightOp) : Cocone F

Full source

/-- Change a cone on `F.rightOp : J ⥤ Cᵒᵖ` to a cocone on `F : Jᵒᵖ ⥤ C`. -/
@[simps]
def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F where
  pt := unop c.pt
  ι := NatTrans.removeRightOp c.π

Cocone from cone over right opposite functor

Informal description

Given a cone $c$ over the right opposite functor $F^{\mathrm{rightOp}} \colon J \to C^{\mathrm{op}}$, this constructs a cocone over the original functor $F \colon J^{\mathrm{op}} \to C$. The cocone point is obtained by applying the unopposite operation to the cone point $c.\mathrm{pt}$, and the natural transformation $\iota$ is constructed by removing the right opposite operation from the cone's natural transformation $\pi$.

CategoryTheory.Limits.coneRightOpOfCocone definition

(c : Cocone F) : Cone F.rightOp

Full source

/-- Change a cocone on `F : Jᵒᵖ ⥤ C` to a cone on `F.rightOp : J ⥤ Cᵒᵖ`. -/
@[simps]
def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp where
  pt := op c.pt
  π := NatTrans.rightOp c.ι

Cone from cocone via right opposite functor

Informal description

Given a cocone $c$ over a functor $F \colon J \to C$, this constructs a cone over the right opposite functor $F^{\mathrm{rightOp}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$. The cone consists of: - The cone point $\mathrm{op}(c.\mathrm{pt})$, which is the opposite object of the cocone point - A natural transformation $\pi$ obtained by applying the right opposite operation to the cocone's natural transformation $\iota \colon F \Rightarrow \Delta(c.\mathrm{pt})$ This transformation converts cocones in the original category to cones in the opposite categories via the right opposite functor construction.

CategoryTheory.Limits.coneOfCoconeUnop definition

(c : Cocone F.unop) : Cone F

Full source

/-- Change a cocone on `F.unop : J ⥤ C` into a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def coneOfCoconeUnop (c : Cocone F.unop) : Cone F where
  pt := op c.pt
  π := NatTrans.removeUnop c.ι

Cone from unopposed cocone

Informal description

Given a cocone $c$ over the unopposite functor $F^{\mathrm{unop}} \colon J \to C$, the construction `coneOfCoconeUnop` produces a cone over the original functor $F \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$. Specifically: - The cone point is $\mathrm{op}(c.\mathrm{pt})$ - The natural transformation $\pi$ is obtained by taking the opposite of the cocone's natural transformation $\iota$ This converts a cocone in the original categories to a cone in the opposite categories.

CategoryTheory.Limits.coconeUnopOfCone definition

(c : Cone F) : Cocone F.unop

Full source

/-- Change a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cocone on `F.unop : J ⥤ C`. -/
@[simps]
def coconeUnopOfCone (c : Cone F) : Cocone F.unop where
  pt := unop c.pt
  ι := NatTrans.unop c.π

Cocone from unopposed cone

Informal description

Given a cone $c$ over a functor $F \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$, the construction `coconeUnopOfCone` produces a cocone over the unopposite functor $F^{\mathrm{unop}} \colon J \to C$. Specifically: - The cocone point is $\mathrm{unop}(c.\mathrm{pt})$ - The natural transformation $\iota$ is obtained by applying $\mathrm{unop}$ to the cone's natural transformation $\pi$ This converts a cone in the opposite categories to a cocone in the original categories.

CategoryTheory.Limits.coconeOfConeUnop definition

(c : Cone F.unop) : Cocone F

Full source

/-- Change a cone on `F.unop : J ⥤ C` into a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def coconeOfConeUnop (c : Cone F.unop) : Cocone F where
  pt := op c.pt
  ι := NatTrans.removeUnop c.π

Cocone from unopposed cone

Informal description

Given a cone $c$ over the unopposite functor $F^{\mathrm{unop}} \colon J \to C$, the construction `coconeOfConeUnop` produces a cocone over the original functor $F \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$. Specifically: - The cocone point is $\mathrm{op}(c.\mathrm{pt})$ - The natural transformation $\iota$ is obtained by taking the opposite of the cone's natural transformation $\pi$ This converts a cone in the original categories to a cocone in the opposite categories.

CategoryTheory.Limits.coneUnopOfCocone definition

(c : Cocone F) : Cone F.unop

Full source

/-- Change a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cone on `F.unop : J ⥤ C`. -/
@[simps]
def coneUnopOfCocone (c : Cocone F) : Cone F.unop where
  pt := unop c.pt
  π := NatTrans.unop c.ι

Cone from unopposed cocone

Informal description

Given a cocone $c$ over a functor $F \colon J \to C$, the construction `coneUnopOfCocone` produces a cone over the unopposite functor $F^{\mathrm{unop}} \colon J^{\mathrm{op}} \to C^{\mathrm{op}}$. Specifically: - The cone point is $\mathrm{unop}(c.\mathrm{pt})$ - The natural transformation $\pi$ is obtained by applying $\mathrm{unop}$ to the cocone's natural transformation $\iota$ This converts a cocone in the original categories to a cone in the opposite categories.

CategoryTheory.Functor.mapConeOp definition

(t : Cone F) : (mapCone G t).op ≅ mapCocone G.op t.op

Full source

/-- The opposite cocone of the image of a cone is the image of the opposite cocone. -/
@[simps!]
def mapConeOp (t : Cone F) : (mapCone G t).op ≅ mapCocone G.op t.op :=
  Cocones.ext (Iso.refl _)

Opposite of a mapped cone is mapped opposite cone

Informal description

Given a cone $t$ over a functor $F \colon J \to C$ and a functor $G \colon C \to D$, the opposite of the image of $t$ under $G$ is isomorphic to the image of the opposite cone $t^{\mathrm{op}}$ under the opposite functor $G^{\mathrm{op}}$. More precisely, there is an isomorphism between: 1. The opposite cocone of $G(t)$, obtained by first mapping the cone $t$ through $G$ and then taking its opposite 2. The cocone obtained by first taking the opposite of $t$ to get $t^{\mathrm{op}}$ and then mapping it through $G^{\mathrm{op}}$ This isomorphism is witnessed by the identity isomorphism on the underlying objects.

CategoryTheory.Functor.mapCoconeOp definition

{t : Cocone F} : (mapCocone G t).op ≅ mapCone G.op t.op

Full source

/-- The opposite cone of the image of a cocone is the image of the opposite cone. -/
@[simps!]
def mapCoconeOp {t : Cocone F} : (mapCocone G t).op ≅ mapCone G.op t.op :=
  Cones.ext (Iso.refl _)

Opposite of a mapped cocone is mapped opposite cocone

Informal description

Given a functor $G \colon C \to D$ and a cocone $t$ over a functor $F \colon J \to C$, the opposite of the image of $t$ under $G$ is isomorphic to the image of the opposite of $t$ under the opposite functor $G^{\mathrm{op}}$. More precisely, there is an isomorphism between: 1. The opposite cone of the cocone obtained by applying $G$ to $t$ (i.e., $(G \circ t)^{\mathrm{op}}$) 2. The cone obtained by applying $G^{\mathrm{op}}$ to the opposite cocone $t^{\mathrm{op}}$ This isomorphism is witnessed by the identity morphism on the underlying objects, ensuring the naturality conditions are preserved.