Mathlib.CategoryTheory.Functor.KanExtension.Basic

CategoryTheory.Functor.RightExtension abbrev

(L : C ⥤ D) (F : C ⥤ H)

Full source

/-- Given two functors `L : C ⥤ D` and `F : C ⥤ H`, this is the category of functors
`F' : H ⥤ D` equipped with a natural transformation `L ⋙ F' ⟶ F`. -/
abbrev RightExtension (L : C ⥤ D) (F : C ⥤ H) :=
  CostructuredArrow ((whiskeringLeft C D H).obj L) F

Category of Right Extensions of $F$ along $L$

Informal description

Given two functors $L \colon C \to D$ and $F \colon C \to H$, the category $\text{RightExtension}(L, F)$ consists of pairs $(F', \alpha)$ where $F' \colon D \to H$ is a functor and $\alpha \colon L \circ F' \to F$ is a natural transformation.

CategoryTheory.Functor.LeftExtension abbrev

(L : C ⥤ D) (F : C ⥤ H)

Full source

/-- Given two functors `L : C ⥤ D` and `F : C ⥤ H`, this is the category of functors
`F' : H ⥤ D` equipped with a natural transformation `F ⟶ L ⋙ F'`. -/
abbrev LeftExtension (L : C ⥤ D) (F : C ⥤ H) :=
  StructuredArrow F ((whiskeringLeft C D H).obj L)

Category of Left Extensions for Functors $L$ and $F$

Informal description

Given two functors $L \colon C \to D$ and $F \colon C \to H$, the category of left extensions consists of functors $F' \colon D \to H$ equipped with a natural transformation $\alpha \colon F \to L \circ F'$.

CategoryTheory.Functor.RightExtension.mk definition

(F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) : RightExtension L F

Full source

/-- Constructor for objects of the category `Functor.RightExtension L F`. -/
@[simps!]
def RightExtension.mk (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F'L ⋙ F' ⟶ F) :
    RightExtension L F :=
  CostructuredArrow.mk α

Construction of a right extension

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, and a functor $F' \colon D \to H$ with a natural transformation $\alpha \colon L \circ F' \to F$, this constructs an object in the category of right extensions of $F$ along $L$, consisting of the pair $(F', \alpha)$.

CategoryTheory.Functor.LeftExtension.mk definition

(F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') : LeftExtension L F

Full source

/-- Constructor for objects of the category `Functor.LeftExtension L F`. -/
@[simps!]
def LeftExtension.mk (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') :
    LeftExtension L F :=
  StructuredArrow.mk α

Construction of a left extension for functors $ L $ and $ F $

Informal description

Given functors $ L \colon C \to D $ and $ F \colon C \to H $, and a functor $ F' \colon D \to H $ equipped with a natural transformation $ \alpha \colon F \to L \circ F' $, this constructs an object in the category of left extensions of $ F $ along $ L $, which consists of such pairs $(F', \alpha)$.

CategoryTheory.Functor.IsRightKanExtension structure

Full source

/-- Given `α : L ⋙ F' ⟶ F`, the property `F'.IsRightKanExtension α` asserts that
`(F', α)` is a terminal object in the category `RightExtension L F`, i.e. that `(F', α)`
is a right Kan extension of `F` along `L`. -/
class IsRightKanExtension : Prop where
  nonempty_isUniversal : Nonempty (RightExtension.mk F' α).IsUniversal

Right Kan Extension Property

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, and $ F' \colon D \to H $, along with a natural transformation $ \alpha \colon L \circ F' \to F $, the property `IsRightKanExtension` asserts that the pair $(F', \alpha)$ forms a right Kan extension of $ F $ along $ L $. This means $(F', \alpha)$ is a terminal object in the category of right extensions of $ F $ along $ L $, where a right extension consists of a functor $ G \colon D \to H $ and a natural transformation $ \beta \colon L \circ G \to F $.

CategoryTheory.Functor.isUniversalOfIsRightKanExtension definition

: (RightExtension.mk F' α).IsUniversal

Full source

/-- If `(F', α)` is a right Kan extension of `F` along `L`, then `(F', α)` is a terminal object
in the category `RightExtension L F`. -/
noncomputable def isUniversalOfIsRightKanExtension : (RightExtension.mk F' α).IsUniversal :=
  IsRightKanExtension.nonempty_isUniversal.some

Universal property of right Kan extensions

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, and $ F' \colon D \to H $, along with a natural transformation $ \alpha \colon L \circ F' \to F $, if $(F', \alpha)$ is a right Kan extension of $ F $ along $ L $, then the pair $(F', \alpha)$ is a terminal object in the category of right extensions of $ F $ along $ L $. This means that for any other right extension $(G, \beta)$, there exists a unique natural transformation $ G \to F' $ making the appropriate diagram commute.

CategoryTheory.Functor.liftOfIsRightKanExtension definition

(G : D ⥤ H) (β : L ⋙ G ⟶ F) : G ⟶ F'

Full source

/-- If `(F', α)` is a right Kan extension of `F` along `L` and `β : L ⋙ G ⟶ F` is
a natural transformation, this is the induced morphism `G ⟶ F'`. -/
noncomputable def liftOfIsRightKanExtension (G : D ⥤ H) (β : L ⋙ GL ⋙ G ⟶ F) : G ⟶ F' :=
  (F'.isUniversalOfIsRightKanExtension α).lift (RightExtension.mk G β)

Induced morphism from universal property of right Kan extension

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, and $ F' \colon D \to H $, along with a natural transformation $ \alpha \colon L \circ F' \to F $ such that $(F', \alpha)$ is a right Kan extension of $ F $ along $ L $, and given another functor $ G \colon D \to H $ with a natural transformation $ \beta \colon L \circ G \to F $, this is the induced natural transformation $ G \to F' $ provided by the universal property of the right Kan extension.

CategoryTheory.Functor.liftOfIsRightKanExtension_fac theorem

(G : D ⥤ H) (β : L ⋙ G ⟶ F) : whiskerLeft L (F'.liftOfIsRightKanExtension α G β) ≫ α = β

Full source

@[reassoc (attr := simp)]
lemma liftOfIsRightKanExtension_fac (G : D ⥤ H) (β : L ⋙ GL ⋙ G ⟶ F) :
    whiskerLeftwhiskerLeft L (F'.liftOfIsRightKanExtension α G β) ≫ α = β :=
  (F'.isUniversalOfIsRightKanExtension α).fac (RightExtension.mk G β)

Factorization Property of Right Kan Extension Induced Morphism

Informal description

Given functors $L \colon C \to D$, $F \colon C \to H$, and $F' \colon D \to H$, and a natural transformation $\alpha \colon L \circ F' \to F$ such that $(F', \alpha)$ is a right Kan extension of $F$ along $L$, then for any functor $G \colon D \to H$ and natural transformation $\beta \colon L \circ G \to F$, the composition of the left whiskering of $L$ with the induced morphism $\text{liftOfIsRightKanExtension}\, \alpha\, G\, \beta \colon G \to F'$ and $\alpha$ equals $\beta$, i.e., $\text{whiskerLeft}\, L\, (\text{liftOfIsRightKanExtension}\, \alpha\, G\, \beta) \circ \alpha = \beta$.

CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app theorem

 (G : D ⥤ H) (β : L ⋙ G ⟶ F) (X : C) : (F'.liftOfIsRightKanExtension α G β).app (L.obj X) ≫ α.app X = β.app X

Full source

@[reassoc (attr := simp)]
lemma liftOfIsRightKanExtension_fac_app (G : D ⥤ H) (β : L ⋙ GL ⋙ G ⟶ F) (X : C) :
    (F'.liftOfIsRightKanExtension α G β).app (L.obj X) ≫ α.app X = β.app X :=
  NatTrans.congr_app (F'.liftOfIsRightKanExtension_fac α G β) X

Componentwise Factorization Property of Right Kan Extension Induced Morphism

Informal description

Given functors $L \colon C \to D$, $F \colon C \to H$, and $F' \colon D \to H$, and a natural transformation $\alpha \colon L \circ F' \to F$ such that $(F', \alpha)$ is a right Kan extension of $F$ along $L$, then for any functor $G \colon D \to H$, natural transformation $\beta \colon L \circ G \to F$, and object $X \in C$, the following diagram commutes: $$(F'.\text{liftOfIsRightKanExtension}\, \alpha\, G\, \beta)(L(X)) \circ \alpha_X = \beta_X$$ where $\alpha_X$ and $\beta_X$ are the components of $\alpha$ and $\beta$ at $X$, respectively.

CategoryTheory.Functor.hom_ext_of_isRightKanExtension theorem

{G : D ⥤ H} (γ₁ γ₂ : G ⟶ F') (hγ : whiskerLeft L γ₁ ≫ α = whiskerLeft L γ₂ ≫ α) : γ₁ = γ₂

Full source

lemma hom_ext_of_isRightKanExtension {G : D ⥤ H} (γ₁ γ₂ : G ⟶ F')
    (hγ : whiskerLeftwhiskerLeft L γ₁ ≫ α = whiskerLeftwhiskerLeft L γ₂ ≫ α) : γ₁ = γ₂ :=
  (F'.isUniversalOfIsRightKanExtension α).hom_ext hγ

Uniqueness of Morphisms into Right Kan Extensions

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F' \colon D \to H$ be a functor with a natural transformation $\alpha \colon L \circ F' \to F$ such that $(F', \alpha)$ is a right Kan extension of $F$ along $L$. Then for any functor $G \colon D \to H$ and natural transformations $\gamma_1, \gamma_2 \colon G \to F'$, if the compositions $\text{whiskerLeft}\, L\, \gamma_1 \circ \alpha$ and $\text{whiskerLeft}\, L\, \gamma_2 \circ \alpha$ are equal, it follows that $\gamma_1 = \gamma_2$.

CategoryTheory.Functor.homEquivOfIsRightKanExtension definition

(G : D ⥤ H) : (G ⟶ F') ≃ (L ⋙ G ⟶ F)

Full source

/-- If `(F', α)` is a right Kan extension of `F` along `L`, then this
is the induced bijection `(G ⟶ F') ≃ (L ⋙ G ⟶ F)` for all `G`. -/
noncomputable def homEquivOfIsRightKanExtension (G : D ⥤ H) :
    (G ⟶ F') ≃ (L ⋙ G ⟶ F) where
  toFun β := whiskerLeftwhiskerLeft _ β ≫ α
  invFun β := liftOfIsRightKanExtension _ α _ β
  left_inv β := Functor.hom_ext_of_isRightKanExtension _ α _ _ (by simp)
  right_inv := by aesop_cat

Bijection induced by universal property of right Kan extension

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, and $ F' \colon D \to H $, along with a natural transformation $ \alpha \colon L \circ F' \to F $ such that $(F', \alpha)$ is a right Kan extension of $ F $ along $ L $, the function `homEquivOfIsRightKanExtension` provides a bijection between natural transformations $ G \to F' $ and natural transformations $ L \circ G \to F $ for any functor $ G \colon D \to H $. The bijection is constructed as follows: - The forward direction maps $ \beta \colon G \to F' $ to the composition $ L \circ G \to L \circ F' \to F $ obtained by whiskering $ \beta $ with $ L $ and then composing with $ \alpha $. - The backward direction uses the universal property of the right Kan extension to lift a natural transformation $ L \circ G \to F $ to a natural transformation $ G \to F' $.

CategoryTheory.Functor.isRightKanExtension_of_iso theorem

 {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F)
  (comm : whiskerLeft L e.hom ≫ α' = α) [F'.IsRightKanExtension α] : F''.IsRightKanExtension α'

Full source

lemma isRightKanExtension_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H}
    (α : L ⋙ F'L ⋙ F' ⟶ F) (α' : L ⋙ F''L ⋙ F'' ⟶ F) (comm : whiskerLeftwhiskerLeft L e.hom ≫ α' = α)
    [F'.IsRightKanExtension α] : F''.IsRightKanExtension α' where
  nonempty_isUniversal := ⟨IsTerminal.ofIso (F'.isUniversalOfIsRightKanExtension α)
    (CostructuredArrow.isoMk e comm)⟩

Right Kan Extension Property Preserved Under Isomorphism

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F', F'' \colon D \to H$ be functors with natural isomorphisms $e \colon F' \cong F''$ and natural transformations $\alpha \colon L \circ F' \to F$, $\alpha' \colon L \circ F'' \to F$ such that $\text{whiskerLeft}\, L\, e \circ \alpha' = \alpha$. If $(F', \alpha)$ is a right Kan extension of $F$ along $L$, then $(F'', \alpha')$ is also a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.isRightKanExtension_iff_of_iso theorem

 {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F)
  (comm : whiskerLeft L e.hom ≫ α' = α) : F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'

Full source

lemma isRightKanExtension_iff_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H}
    (α : L ⋙ F'L ⋙ F' ⟶ F) (α' : L ⋙ F''L ⋙ F'' ⟶ F) (comm : whiskerLeftwhiskerLeft L e.hom ≫ α' = α) :
    F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α' := by
  constructor
  · intro
    exact isRightKanExtension_of_iso e α α' comm
  · intro
    refine isRightKanExtension_of_iso e.symm α' α ?_
    rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]

Right Kan Extension Property is Equivalent Under Isomorphism of Functors

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F', F'' \colon D \to H$ be functors with a natural isomorphism $e \colon F' \cong F''$. Given natural transformations $\alpha \colon L \circ F' \to F$ and $\alpha' \colon L \circ F'' \to F$ such that $\text{whiskerLeft}\, L\, e \circ \alpha' = \alpha$, then $(F', \alpha)$ is a right Kan extension of $F$ along $L$ if and only if $(F'', \alpha')$ is a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.rightKanExtensionUniqueOfIso definition

{G : C ⥤ H} (i : F ≅ G) (G' : D ⥤ H) (β : L ⋙ G' ⟶ G) [G'.IsRightKanExtension β] : F' ≅ G'

Full source

/-- Right Kan extensions of isomorphic functors are isomorphic. -/
@[simps]
noncomputable def rightKanExtensionUniqueOfIso {G : C ⥤ H} (i : F ≅ G) (G' : D ⥤ H)
    (β : L ⋙ G'L ⋙ G' ⟶ G) [G'.IsRightKanExtension β] : F' ≅ G' where
  hom := liftOfIsRightKanExtension _ β F' (α ≫ i.hom)
  inv := liftOfIsRightKanExtension _ α G' (β ≫ i.inv)
  hom_inv_id := F'.hom_ext_of_isRightKanExtension α _ _ (by simp)
  inv_hom_id := G'.hom_ext_of_isRightKanExtension β _ _ (by simp)

Uniqueness of right Kan extensions up to isomorphism

Informal description

Given functors $ L \colon C \to D $, $ F, G \colon C \to H $, and $ F', G' \colon D \to H $, along with an isomorphism $ i \colon F \cong G $ and natural transformations $ \alpha \colon L \circ F' \to F $, $ \beta \colon L \circ G' \to G $ such that $ (F', \alpha) $ and $ (G', \beta) $ are right Kan extensions, there exists a unique isomorphism $ F' \cong G' $ induced by the universal property of the right Kan extensions.

CategoryTheory.Functor.rightKanExtensionUnique definition

(F'' : D ⥤ H) (α' : L ⋙ F'' ⟶ F) [F''.IsRightKanExtension α'] : F' ≅ F''

Full source

/-- Two right Kan extensions are (canonically) isomorphic. -/
@[simps!]
noncomputable def rightKanExtensionUnique
    (F'' : D ⥤ H) (α' : L ⋙ F''L ⋙ F'' ⟶ F) [F''.IsRightKanExtension α'] : F' ≅ F'' :=
  rightKanExtensionUniqueOfIso F' α (Iso.refl _) F'' α'

Uniqueness of right Kan extensions up to isomorphism

Informal description

Given two right Kan extensions $(F', \alpha)$ and $(F'', \alpha')$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, there exists a unique isomorphism $F' \cong F''$ between the extensions, induced by the universal property of right Kan extensions.

CategoryTheory.Functor.isRightKanExtension_iff_isIso theorem

 {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F'' ⟶ F') {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F)
  (comm : whiskerLeft L φ ≫ α = α') [F'.IsRightKanExtension α] : F''.IsRightKanExtension α' ↔ IsIso φ

Full source

lemma isRightKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F'' ⟶ F')
    {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F'L ⋙ F' ⟶ F) (α' : L ⋙ F''L ⋙ F'' ⟶ F)
    (comm : whiskerLeftwhiskerLeft L φ ≫ α = α') [F'.IsRightKanExtension α] :
    F''.IsRightKanExtension α' ↔ IsIso φ := by
  constructor
  · intro
    rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
      (by simp [comm])]
    infer_instance
  · intro
    rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]
    infer_instance

Characterization of Right Kan Extensions via Isomorphisms

Informal description

Let $ L \colon C \to D $ and $ F \colon C \to H $ be functors, and let $ F', F'' \colon D \to H $ be functors with a natural transformation $ \varphi \colon F'' \to F' $. Given natural transformations $ \alpha \colon L \circ F' \to F $ and $ \alpha' \colon L \circ F'' \to F $ such that $ \text{whiskerLeft}\, L\, \varphi \circ \alpha = \alpha' $, and assuming that $ (F', \alpha) $ is a right Kan extension of $ F $ along $ L $, then $ (F'', \alpha') $ is a right Kan extension of $ F $ along $ L $ if and only if $ \varphi $ is an isomorphism.

CategoryTheory.Functor.IsLeftKanExtension structure

Full source

/-- Given `α : F ⟶ L ⋙ F'`, the property `F'.IsLeftKanExtension α` asserts that
`(F', α)` is an initial object in the category `LeftExtension L F`, i.e. that `(F', α)`
is a left Kan extension of `F` along `L`. -/
class IsLeftKanExtension : Prop where
  nonempty_isUniversal : Nonempty (LeftExtension.mk F' α).IsUniversal

Left Kan Extension Property

Informal description

Given a natural transformation $\alpha : F \to L \circ F'$, the property `IsLeftKanExtension` asserts that the pair $(F', \alpha)$ is an initial object in the category of left extensions of $F$ along $L$, meaning it is a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.isUniversalOfIsLeftKanExtension definition

: (LeftExtension.mk F' α).IsUniversal

Full source

/-- If `(F', α)` is a left Kan extension of `F` along `L`, then `(F', α)` is an initial object
in the category `LeftExtension L F`. -/
noncomputable def isUniversalOfIsLeftKanExtension : (LeftExtension.mk F' α).IsUniversal :=
  IsLeftKanExtension.nonempty_isUniversal.some

Universal property of left Kan extensions

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $F \colon C \to H$ and $L \colon C \to D$ are functors, if $(F', \alpha)$ is a left Kan extension of $F$ along $L$, then the pair $(F', \alpha)$ forms an initial object in the category of left extensions of $F$ along $L$. This means that for any other extension $(G, \beta)$ where $G \colon D \to H$ and $\beta \colon F \to L \circ G$, there exists a unique natural transformation $F' \to G$ making the appropriate diagram commute.

CategoryTheory.Functor.descOfIsLeftKanExtension definition

(G : D ⥤ H) (β : F ⟶ L ⋙ G) : F' ⟶ G

Full source

/-- If `(F', α)` is a left Kan extension of `F` along `L` and `β : F ⟶ L ⋙ G` is
a natural transformation, this is the induced morphism `F' ⟶ G`. -/
noncomputable def descOfIsLeftKanExtension (G : D ⥤ H) (β : F ⟶ L ⋙ G) : F' ⟶ G :=
  (F'.isUniversalOfIsLeftKanExtension α).desc (LeftExtension.mk G β)

Induced morphism from a left Kan extension

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L$, and another natural transformation $\beta \colon F \to L \circ G$, this is the unique induced natural transformation $F' \to G$ making the diagram commute.

CategoryTheory.Functor.descOfIsLeftKanExtension_fac theorem

(G : D ⥤ H) (β : F ⟶ L ⋙ G) : α ≫ whiskerLeft L (F'.descOfIsLeftKanExtension α G β) = β

Full source

@[reassoc (attr := simp)]
lemma descOfIsLeftKanExtension_fac (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
    α ≫ whiskerLeft L (F'.descOfIsLeftKanExtension α G β) = β :=
  (F'.isUniversalOfIsLeftKanExtension α).fac (LeftExtension.mk G β)

Factorization Property of Left Kan Extensions

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, and a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L$, then for any other functor $G \colon D \to H$ with a natural transformation $\beta \colon F \to L \circ G$, the composition of $\alpha$ with the left whiskering of $L$ applied to the induced morphism $F' \to G$ equals $\beta$. In other words, the following diagram commutes: $$\alpha \circ (L \circ \text{desc}) = \beta$$ where $\text{desc} \colon F' \to G$ is the unique morphism induced by the universal property of the left Kan extension.

CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app theorem

 (G : D ⥤ H) (β : F ⟶ L ⋙ G) (X : C) : α.app X ≫ (F'.descOfIsLeftKanExtension α G β).app (L.obj X) = β.app X

Full source

@[reassoc (attr := simp)]
lemma descOfIsLeftKanExtension_fac_app (G : D ⥤ H) (β : F ⟶ L ⋙ G) (X : C) :
    α.app X ≫ (F'.descOfIsLeftKanExtension α G β).app (L.obj X) = β.app X :=
  NatTrans.congr_app (F'.descOfIsLeftKanExtension_fac α G β) X

Component-wise Factorization Property of Left Kan Extensions

Informal description

Given functors $L \colon C \to D$, $F \colon C \to H$, and $F' \colon D \to H$ with a natural transformation $\alpha \colon F \to L \circ F'$ making $(F', \alpha)$ a left Kan extension of $F$ along $L$, then for any functor $G \colon D \to H$ and natural transformation $\beta \colon F \to L \circ G$, the following diagram commutes at each object $X$ in $C$: $$ \alpha_X \circ \text{desc}_{L(X)} = \beta_X $$ where $\text{desc} \colon F' \to G$ is the unique morphism induced by the universal property of the left Kan extension.

CategoryTheory.Functor.hom_ext_of_isLeftKanExtension theorem

{G : D ⥤ H} (γ₁ γ₂ : F' ⟶ G) (hγ : α ≫ whiskerLeft L γ₁ = α ≫ whiskerLeft L γ₂) : γ₁ = γ₂

Full source

lemma hom_ext_of_isLeftKanExtension {G : D ⥤ H} (γ₁ γ₂ : F' ⟶ G)
    (hγ : α ≫ whiskerLeft L γ₁ = α ≫ whiskerLeft L γ₂) : γ₁ = γ₂ :=
  (F'.isUniversalOfIsLeftKanExtension α).hom_ext hγ

Uniqueness of Natural Transformations from Left Kan Extensions

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F' \colon D \to H$ be a functor equipped with a natural transformation $\alpha \colon F \to L \circ F'$ that makes $(F', \alpha)$ a left Kan extension of $F$ along $L$. Then for any functor $G \colon D \to H$ and any pair of natural transformations $\gamma_1, \gamma_2 \colon F' \to G$, if the compositions $\alpha \circ (L \circ \gamma_1)$ and $\alpha \circ (L \circ \gamma_2)$ are equal, then $\gamma_1 = \gamma_2$.

CategoryTheory.Functor.homEquivOfIsLeftKanExtension definition

(G : D ⥤ H) : (F' ⟶ G) ≃ (F ⟶ L ⋙ G)

Full source

/-- If `(F', α)` is a left Kan extension of `F` along `L`, then this
is the induced bijection `(F' ⟶ G) ≃ (F ⟶ L ⋙ G)` for all `G`. -/
noncomputable def homEquivOfIsLeftKanExtension (G : D ⥤ H) :
    (F' ⟶ G) ≃ (F ⟶ L ⋙ G) where
  toFun β := α ≫ whiskerLeft _ β
  invFun β := descOfIsLeftKanExtension _ α _ β
  left_inv β := Functor.hom_ext_of_isLeftKanExtension _ α _ _ (by simp)
  right_inv := by aesop_cat

Bijection induced by left Kan extension property

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L$, and a functor $G \colon D \to H$, the bijection $\text{homEquivOfIsLeftKanExtension}\, G$ maps between natural transformations $F' \to G$ and natural transformations $F \to L \circ G$. The forward direction is given by post-composing with $\alpha$ and left whiskering, while the inverse direction is given by the universal property of the left Kan extension.

CategoryTheory.Functor.isLeftKanExtension_of_iso theorem

 {F' : D ⥤ H} {F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
  (comm : α ≫ whiskerLeft L e.hom = α') [F'.IsLeftKanExtension α] : F''.IsLeftKanExtension α'

Full source

lemma isLeftKanExtension_of_iso {F' : D ⥤ H} {F'' : D ⥤ H} (e : F' ≅ F'')
    {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
    (comm : α ≫ whiskerLeft L e.hom = α') [F'.IsLeftKanExtension α] :
    F''.IsLeftKanExtension α' where
  nonempty_isUniversal := ⟨IsInitial.ofIso (F'.isUniversalOfIsLeftKanExtension α)
    (StructuredArrow.isoMk e comm)⟩

Preservation of Left Kan Extension Property under Isomorphism of Functors

Informal description

Let $F', F'' \colon D \to H$ be functors with an isomorphism $e \colon F' \cong F''$, and let $L \colon C \to D$ and $F \colon C \to H$ be functors. Given natural transformations $\alpha \colon F \to L \circ F'$ and $\alpha' \colon F \to L \circ F''$ such that $\alpha \circ (\text{whiskerLeft}\, L\, e) = \alpha'$, if $(F', \alpha)$ is a left Kan extension of $F$ along $L$, then $(F'', \alpha')$ is also a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.isLeftKanExtension_iff_of_iso theorem

 {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
  (comm : α ≫ whiskerLeft L e.hom = α') : F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'

Full source

lemma isLeftKanExtension_iff_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'')
    {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
    (comm : α ≫ whiskerLeft L e.hom = α') :
    F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α' := by
  constructor
  · intro
    exact isLeftKanExtension_of_iso e α α' comm
  · intro
    refine isLeftKanExtension_of_iso e.symm α' α ?_
    rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]

Characterization of Left Kan Extension Property under Isomorphism of Functors

Informal description

Let $F', F'' \colon D \to H$ be functors with an isomorphism $e \colon F' \cong F''$, and let $L \colon C \to D$ and $F \colon C \to H$ be functors. Given natural transformations $\alpha \colon F \to L \circ F'$ and $\alpha' \colon F \to L \circ F''$ such that $\alpha \circ (\text{whiskerLeft}\, L\, e) = \alpha'$, then $(F', \alpha)$ is a left Kan extension of $F$ along $L$ if and only if $(F'', \alpha')$ is a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.leftKanExtensionUniqueOfIso definition

{G : C ⥤ H} (i : F ≅ G) (G' : D ⥤ H) (β : G ⟶ L ⋙ G') [G'.IsLeftKanExtension β] : F' ≅ G'

Full source

/-- Left Kan extensions of isomorphic functors are isomorphic. -/
@[simps]
noncomputable def leftKanExtensionUniqueOfIso {G : C ⥤ H} (i : F ≅ G) (G' : D ⥤ H)
    (β : G ⟶ L ⋙ G') [G'.IsLeftKanExtension β] : F' ≅ G' where
  hom := descOfIsLeftKanExtension _ α G' (i.hom ≫ β)
  inv := descOfIsLeftKanExtension _ β F' (i.inv ≫ α)
  hom_inv_id := F'.hom_ext_of_isLeftKanExtension α _ _ (by simp)
  inv_hom_id := G'.hom_ext_of_isLeftKanExtension β _ _ (by simp)

Isomorphism between left Kan extensions of isomorphic functors

Informal description

Given an isomorphism $i \colon F \cong G$ between functors $F, G \colon C \to H$, and a left Kan extension $(G', \beta)$ of $G$ along $L \colon C \to D$, there exists a unique isomorphism $F' \cong G'$ between the left Kan extensions of $F$ and $G$ along $L$. This isomorphism is constructed using the universal properties of the Kan extensions, ensuring that the diagram commutes appropriately.

CategoryTheory.Functor.leftKanExtensionUnique definition

(F'' : D ⥤ H) (α' : F ⟶ L ⋙ F'') [F''.IsLeftKanExtension α'] : F' ≅ F''

Full source

/-- Two left Kan extensions are (canonically) isomorphic. -/
@[simps!]
noncomputable def leftKanExtensionUnique
    (F'' : D ⥤ H) (α' : F ⟶ L ⋙ F'') [F''.IsLeftKanExtension α'] : F' ≅ F'' :=
  leftKanExtensionUniqueOfIso F' α (Iso.refl _) F'' α'

Uniqueness of left Kan extensions up to isomorphism

Informal description

Given two left Kan extensions $(F', \alpha)$ and $(F'', \alpha')$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, there exists a unique isomorphism $F' \cong F''$ between the extensions. This isomorphism is canonical and arises from the universal property of left Kan extensions.

CategoryTheory.Functor.isLeftKanExtension_iff_isIso theorem

 {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F' ⟶ F'') {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
  (comm : α ≫ whiskerLeft L φ = α') [F'.IsLeftKanExtension α] : F''.IsLeftKanExtension α' ↔ IsIso φ

Full source

lemma isLeftKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F' ⟶ F'')
    {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
    (comm : α ≫ whiskerLeft L φ = α') [F'.IsLeftKanExtension α] :
    F''.IsLeftKanExtension α' ↔ IsIso φ := by
  constructor
  · intro
    rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]
    infer_instance
  · intro
    exact isLeftKanExtension_of_iso (asIso φ) α α' comm

Characterization of Left Kan Extensions via Isomorphism of Natural Transformations

Informal description

Let $F', F'' \colon D \to H$ be functors with a natural transformation $\varphi \colon F' \to F''$, and let $L \colon C \to D$ and $F \colon C \to H$ be functors. Given natural transformations $\alpha \colon F \to L \circ F'$ and $\alpha' \colon F \to L \circ F''$ such that $\alpha \circ (L \circ \varphi) = \alpha'$, and assuming that $(F', \alpha)$ is a left Kan extension of $F$ along $L$, then $(F'', \alpha')$ is a left Kan extension of $F$ along $L$ if and only if $\varphi$ is an isomorphism.

CategoryTheory.Functor.HasRightKanExtension abbrev

(L : C ⥤ D) (F : C ⥤ H)

Full source

/-- This property `HasRightKanExtension L F` holds when the functor `F` has a right
Kan extension along `L`. -/
abbrev HasRightKanExtension (L : C ⥤ D) (F : C ⥤ H) := HasTerminal (RightExtension L F)

Existence of Right Kan Extension of $F$ along $L$

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, the property $\text{HasRightKanExtension}\, L\, F$ holds when there exists a right Kan extension of $F$ along $L$. This means there exists a functor $F' \colon D \to H$ and a natural transformation $\alpha \colon L \circ F' \to F$ such that $(F', \alpha)$ is terminal in the category of right extensions of $F$ along $L$.

CategoryTheory.Functor.HasRightKanExtension.mk theorem

(F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) [F'.IsRightKanExtension α] : HasRightKanExtension L F

Full source

lemma HasRightKanExtension.mk (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F'L ⋙ F' ⟶ F)
    [F'.IsRightKanExtension α] : HasRightKanExtension L F :=
  (F'.isUniversalOfIsRightKanExtension α).hasTerminal

Existence of Right Kan Extension via Terminal Pair

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, a functor $F' \colon D \to H$, and a natural transformation $\alpha \colon L \circ F' \to F$, if $(F', \alpha)$ forms a right Kan extension of $F$ along $L$, then there exists a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.HasLeftKanExtension abbrev

(L : C ⥤ D) (F : C ⥤ H)

Full source

/-- This property `HasLeftKanExtension L F` holds when the functor `F` has a left
Kan extension along `L`. -/
abbrev HasLeftKanExtension (L : C ⥤ D) (F : C ⥤ H) := HasInitial (LeftExtension L F)

Existence of Left Kan Extension for Functors $L$ and $F$

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, the property $\text{HasLeftKanExtension}\, L\, F$ holds when there exists a left Kan extension of $F$ along $L$. This means there exists a functor $F' \colon D \to H$ and a natural transformation $\alpha \colon F \to L \circ F'$ that is universal among all such pairs $(F', \alpha)$.

CategoryTheory.Functor.HasLeftKanExtension.mk theorem

(F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') [F'.IsLeftKanExtension α] : HasLeftKanExtension L F

Full source

lemma HasLeftKanExtension.mk (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F')
    [F'.IsLeftKanExtension α] : HasLeftKanExtension L F :=
  (F'.isUniversalOfIsLeftKanExtension α).hasInitial

Existence of Left Kan Extension via Universal Property

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, and a functor $F' \colon D \to H$ equipped with a natural transformation $\alpha \colon F \to L \circ F'$ that is a left Kan extension, then there exists a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.rightKanExtension definition

: D ⥤ H

Full source

/-- A chosen right Kan extension when `[HasRightKanExtension L F]` holds. -/
noncomputable def rightKanExtension : D ⥤ H := (⊤_ _ : RightExtension L F).left

Right Kan extension of $ F $ along $ L $

Informal description

Given functors $ L \colon C \to D $ and $ F \colon C \to H $, the right Kan extension of $ F $ along $ L $ is a functor $ \mathrm{rightKanExtension}\, L\, F \colon D \to H $ equipped with a natural transformation $ \alpha \colon L \circ \mathrm{rightKanExtension}\, L\, F \to F $ that is terminal in the category of right extensions of $ F $ along $ L $. This means that for any other functor $ F' \colon D \to H $ with a natural transformation $ \beta \colon L \circ F' \to F $, there exists a unique natural transformation $ \gamma \colon F' \to \mathrm{rightKanExtension}\, L\, F $ such that $ \alpha \circ (L \circ \gamma) = \beta $.

CategoryTheory.Functor.rightKanExtensionCounit definition

: L ⋙ rightKanExtension L F ⟶ F

Full source

/-- The counit of the chosen right Kan extension `rightKanExtension L F`. -/
noncomputable def rightKanExtensionCounit : L ⋙ rightKanExtension L FL ⋙ rightKanExtension L F ⟶ F :=
  (⊤_ _ : RightExtension L F).hom

Counit of the right Kan extension

Informal description

The natural transformation $\alpha \colon L \circ \mathrm{rightKanExtension}\, L\, F \to F$ is the counit of the right Kan extension of $F$ along $L$, which is terminal in the category of right extensions of $F$ along $L$.

CategoryTheory.Functor.instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit instance

: (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

Full source

instance : (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F) where
  nonempty_isUniversal := ⟨terminalIsTerminal⟩

The Right Kan Extension Property for $\mathrm{rightKanExtension}\, L\, F$

Informal description

The functor $\mathrm{rightKanExtension}\, L\, F$ equipped with the natural transformation $\mathrm{rightKanExtensionCounit}\, L\, F \colon L \circ \mathrm{rightKanExtension}\, L\, F \to F$ forms a right Kan extension of $F$ along $L$. This means that for any other functor $G \colon D \to H$ with a natural transformation $\beta \colon L \circ G \to F$, there exists a unique natural transformation $\gamma \colon G \to \mathrm{rightKanExtension}\, L\, F$ such that $\mathrm{rightKanExtensionCounit}\, L\, F \circ (L \circ \gamma) = \beta$.

CategoryTheory.Functor.rightKanExtension_hom_ext theorem

 {G : D ⥤ H} (γ₁ γ₂ : G ⟶ rightKanExtension L F)
  (hγ : whiskerLeft L γ₁ ≫ rightKanExtensionCounit L F = whiskerLeft L γ₂ ≫ rightKanExtensionCounit L F) : γ₁ = γ₂

Full source

@[ext]
lemma rightKanExtension_hom_ext {G : D ⥤ H} (γ₁ γ₂ : G ⟶ rightKanExtension L F)
    (hγ : whiskerLeftwhiskerLeft L γ₁ ≫ rightKanExtensionCounit L F =
      whiskerLeftwhiskerLeft L γ₂ ≫ rightKanExtensionCounit L F) :
    γ₁ = γ₂ :=
  hom_ext_of_isRightKanExtension _ _ _ _ hγ

Uniqueness of Morphisms into Right Kan Extensions via Counit Condition

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $\mathrm{rightKanExtension}\, L\, F \colon D \to H$ be the right Kan extension of $F$ along $L$ with counit $\alpha \colon L \circ \mathrm{rightKanExtension}\, L\, F \to F$. For any functor $G \colon D \to H$ and natural transformations $\gamma_1, \gamma_2 \colon G \to \mathrm{rightKanExtension}\, L\, F$, if the compositions $L \circ \gamma_1 \circ \alpha$ and $L \circ \gamma_2 \circ \alpha$ are equal, then $\gamma_1 = \gamma_2$.

CategoryTheory.Functor.leftKanExtension definition

: D ⥤ H

Full source

/-- A chosen left Kan extension when `[HasLeftKanExtension L F]` holds. -/
noncomputable def leftKanExtension : D ⥤ H := (⊥_ _ : LeftExtension L F).right

Left Kan extension of $ F $ along $ L $

Informal description

Given functors $ L \colon C \to D $ and $ F \colon C \to H $, the functor $ \text{leftKanExtension}\, L\, F \colon D \to H $ is a chosen left Kan extension of $ F $ along $ L $. This means it comes equipped with a natural transformation $ \alpha \colon F \to L \circ \text{leftKanExtension}\, L\, F $ that is universal among all such pairs $(F', \alpha)$.

CategoryTheory.Functor.leftKanExtensionUnit definition

: F ⟶ L ⋙ leftKanExtension L F

Full source

/-- The unit of the chosen left Kan extension `leftKanExtension L F`. -/
noncomputable def leftKanExtensionUnit : F ⟶ L ⋙ leftKanExtension L F :=
  (⊥_ _ : LeftExtension L F).hom

Unit of the left Kan extension of $F$ along $L$

Informal description

The natural transformation $\eta \colon F \to L \circ \text{leftKanExtension}\, L\, F$ is the unit of the left Kan extension of $F$ along $L$, where $L \colon C \to D$ and $F \colon C \to H$ are functors. This unit is obtained as the morphism part of the initial object in the category of left extensions of $F$ along $L$.

CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit instance

: (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)

Full source

instance : (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F) where
  nonempty_isUniversal := ⟨initialIsInitial⟩

Universal Property of the Chosen Left Kan Extension

Informal description

The chosen left Kan extension $\text{leftKanExtension}\, L\, F$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, equipped with its unit natural transformation $\eta \colon F \to L \circ \text{leftKanExtension}\, L\, F$, satisfies the universal property of being a left Kan extension. This means that $(\text{leftKanExtension}\, L\, F, \eta)$ is an initial object in the category of left extensions of $F$ along $L$.

CategoryTheory.Functor.leftKanExtension_hom_ext theorem

 {G : D ⥤ H} (γ₁ γ₂ : leftKanExtension L F ⟶ G)
  (hγ : leftKanExtensionUnit L F ≫ whiskerLeft L γ₁ = leftKanExtensionUnit L F ≫ whiskerLeft L γ₂) : γ₁ = γ₂

Full source

@[ext]
lemma leftKanExtension_hom_ext {G : D ⥤ H} (γ₁ γ₂ : leftKanExtensionleftKanExtension L F ⟶ G)
    (hγ : leftKanExtensionUnitleftKanExtensionUnit L F ≫ whiskerLeft L γ₁ =
      leftKanExtensionUnitleftKanExtensionUnit L F ≫ whiskerLeft L γ₂) : γ₁ = γ₂ :=
  hom_ext_of_isLeftKanExtension _ _ _ _ hγ

Uniqueness of Natural Transformations from Left Kan Extension

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $G \colon D \to H$ be another functor. Given two natural transformations $\gamma_1, \gamma_2 \colon \text{leftKanExtension}\, L\, F \to G$ such that the compositions $\eta \circ (L \circ \gamma_1)$ and $\eta \circ (L \circ \gamma_2)$ are equal (where $\eta \colon F \to L \circ \text{leftKanExtension}\, L\, F$ is the unit of the left Kan extension), then $\gamma_1 = \gamma_2$.

CategoryTheory.Functor.LeftExtension.postcomp₁ definition

(f : L' ⟶ L ⋙ G) (F : C ⥤ H) : LeftExtension L' F ⥤ LeftExtension L F

Full source

/-- The functor `LeftExtension L' F ⥤ LeftExtension L F`
induced by a natural transformation `L' ⟶ L ⋙ G'`. -/
@[simps!]
def LeftExtension.postcomp₁ (f : L' ⟶ L ⋙ G) (F : C ⥤ H) :
    LeftExtensionLeftExtension L' F ⥤ LeftExtension L F :=
  StructuredArrow.map₂ (F := (whiskeringLeft D D' H).obj G) (G := 𝟭 _) (𝟙 _)
    ((whiskeringLeft C D' H).map f)

Functor between left extension categories induced by a natural transformation

Informal description

Given a natural transformation $f \colon L' \to L \circ G$ between functors $L' \colon C \to D'$ and $L \circ G \colon C \to D'$, and a functor $F \colon C \to H$, the functor `LeftExtension.postcomp₁` maps an object $(F', \alpha)$ in the category of left extensions of $F$ along $L'$ to an object in the category of left extensions of $F$ along $L$, where $F' \colon D' \to H$ is equipped with a natural transformation $\alpha \colon F \to L' \circ F'$. This is constructed using the structured arrow functor applied to the identity natural transformation and the whiskering of $f$.

CategoryTheory.Functor.RightExtension.postcomp₁ definition

(f : L ⋙ G ⟶ L') (F : C ⥤ H) : RightExtension L' F ⥤ RightExtension L F

Full source

/-- The functor `RightExtension L' F ⥤ RightExtension L F`
induced by a natural transformation `L ⋙ G ⟶ L'`. -/
@[simps!]
def RightExtension.postcomp₁ (f : L ⋙ GL ⋙ G ⟶ L') (F : C ⥤ H) :
    RightExtensionRightExtension L' F ⥤ RightExtension L F :=
  CostructuredArrow.map₂ (F := (whiskeringLeft D D' H).obj G) (G := 𝟭 _)
    ((whiskeringLeft C D' H).map f) (𝟙 _)

Functor induced by natural transformation on right extensions

Informal description

Given a natural transformation $f \colon L \circ G \Rightarrow L'$ and a functor $F \colon C \to H$, the functor $\text{postcomp}_1$ maps objects and morphisms from the category of right extensions of $F$ along $L'$ to the category of right extensions of $F$ along $L$. Specifically, it sends a pair $(F', \alpha \colon L' \circ F' \Rightarrow F)$ to $(F', \alpha \circ (f \circ F'))$, where $f \circ F'$ denotes the whiskering of $f$ by $F'$.

CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso instance

(f : L' ⟶ L ⋙ G) [IsIso f] (F : C ⥤ H) : IsEquivalence (LeftExtension.postcomp₁ G f F)

Full source

noncomputable instance (f : L' ⟶ L ⋙ G) [IsIso f] (F : C ⥤ H) :
    IsEquivalence (LeftExtension.postcomp₁ G f F) := by
  apply StructuredArrow.isEquivalenceMap₂

Equivalence of Left Extension Categories under Isomorphic Natural Transformations

Informal description

For any natural transformation $f \colon L' \to L \circ G$ that is an isomorphism, and any functor $F \colon C \to H$, the functor $\text{postcomp}_1(G, f, F) \colon \text{LeftExtension}(L', F) \to \text{LeftExtension}(L, F)$ is an equivalence of categories.

CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso instance

(f : L ⋙ G ⟶ L') [IsIso f] (F : C ⥤ H) : IsEquivalence (RightExtension.postcomp₁ G f F)

Full source

noncomputable instance (f : L ⋙ GL ⋙ G ⟶ L') [IsIso f] (F : C ⥤ H) :
    IsEquivalence (RightExtension.postcomp₁ G f F) := by
  apply CostructuredArrow.isEquivalenceMap₂

Equivalence of Right Extension Categories Induced by Natural Isomorphism

Informal description

Given functors $L \colon C \to D$, $G \colon D \to E$, and $F \colon C \to H$, and a natural isomorphism $f \colon L \circ G \Rightarrow L'$, the functor $\text{postcomp}_1 \colon \text{RightExtension}(L', F) \to \text{RightExtension}(L, F)$ induced by $f$ is an equivalence of categories.

CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁ theorem

(e : L ⋙ G ≅ L') (F : C ⥤ H) : HasLeftKanExtension L' F ↔ HasLeftKanExtension L F

Full source

lemma hasLeftExtension_iff_postcomp₁ (e : L ⋙ GL ⋙ G ≅ L') (F : C ⥤ H) :
    HasLeftKanExtensionHasLeftKanExtension L' F ↔ HasLeftKanExtension L F :=
  (LeftExtension.postcomp₁ G e.inv F).asEquivalence.hasInitial_iff

Equivalence of Left Kan Extension Existence under Natural Isomorphism

Informal description

Given functors $L \colon C \to D$, $G \colon D \to E$, and $F \colon C \to H$, and a natural isomorphism $e \colon L \circ G \cong L'$, the existence of a left Kan extension of $F$ along $L'$ is equivalent to the existence of a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.hasRightExtension_iff_postcomp₁ theorem

(e : L ⋙ G ≅ L') (F : C ⥤ H) : HasRightKanExtension L' F ↔ HasRightKanExtension L F

Full source

lemma hasRightExtension_iff_postcomp₁ (e : L ⋙ GL ⋙ G ≅ L') (F : C ⥤ H) :
    HasRightKanExtensionHasRightKanExtension L' F ↔ HasRightKanExtension L F :=
  (RightExtension.postcomp₁ G e.hom F).asEquivalence.hasTerminal_iff

Existence of Right Kan Extensions Under Natural Isomorphism

Informal description

Given functors $L \colon C \to D$, $G \colon D \to E$, and $F \colon C \to H$, and a natural isomorphism $e \colon L \circ G \cong L'$, the right Kan extension of $F$ along $L'$ exists if and only if the right Kan extension of $F$ along $L$ exists.

CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv definition

(ex : LeftExtension L' F) : ex.IsUniversal ≃ ((LeftExtension.postcomp₁ G e.inv F).obj ex).IsUniversal

Full source

/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a left extension of `F` along `L'` is universal
iff the corresponding left extension of `L` along `L` is. -/
noncomputable def LeftExtension.isUniversalPostcomp₁Equiv (ex : LeftExtension L' F) :
    ex.IsUniversal ≃ ((LeftExtension.postcomp₁ G e.inv F).obj ex).IsUniversal := by
  apply IsInitial.isInitialIffObj (LeftExtension.postcomp₁ G e.inv F)

Equivalence of universal properties for left extensions under isomorphism of functors

Informal description

Given an isomorphism $e \colon L \circ G \cong L'$ of functors, a left extension $(F', \alpha)$ of $F$ along $L'$ is universal if and only if the corresponding left extension of $F$ along $L$ obtained via postcomposition with $G$ and $e^{-1}$ is universal.

CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv definition

(ex : RightExtension L' F) : ex.IsUniversal ≃ ((RightExtension.postcomp₁ G e.hom F).obj ex).IsUniversal

Full source

/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a right extension of `F` along `L'` is universal
iff the corresponding right extension of `L` along `L` is. -/
noncomputable def RightExtension.isUniversalPostcomp₁Equiv (ex : RightExtension L' F) :
    ex.IsUniversal ≃ ((RightExtension.postcomp₁ G e.hom F).obj ex).IsUniversal := by
  apply IsTerminal.isTerminalIffObj (RightExtension.postcomp₁ G e.hom F)

Equivalence of universality under post-composition with natural isomorphism

Informal description

Given a natural isomorphism $e : L \circ G \cong L'$ and a right extension $ex$ of $F$ along $L'$, the extension $ex$ is universal if and only if the corresponding right extension obtained by post-composition with $e$ is universal. In other words, universality is preserved under the equivalence induced by $e$.

CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁ theorem

 (α : F ⟶ L' ⋙ F') :
  F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv _ ≫ (Functor.associator _ _ _).hom)

Full source

lemma isLeftKanExtension_iff_postcomp₁ (α : F ⟶ L' ⋙ F') :
    F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension
      (α ≫ whiskerRight e.inv _ ≫ (Functor.associator _ _ _).hom) := by
  let eq : (LeftExtension.mk _ α).IsUniversal ≃
      (LeftExtension.mk _
        (α ≫ whiskerRight e.inv _ ≫ (Functor.associator _ _ _).hom)).IsUniversal :=
    (LeftExtension.isUniversalPostcomp₁Equiv G e F _).trans
    (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Characterization of Left Kan Extensions via Postcomposition with Isomorphism

Informal description

Given functors $F \colon C \to H$, $L' \colon C \to D'$, and $F' \colon D' \to H$, and a natural transformation $\alpha \colon F \to L' \circ F'$, the pair $(F', \alpha)$ is a left Kan extension of $F$ along $L'$ if and only if the composition $(G \circ F', \alpha \circ \text{whiskerRight}\, e^{-1}\, F' \circ \text{associator}\, L\, G\, F')$ is a left Kan extension of $F$ along $L$, where $e \colon L \circ G \cong L'$ is a natural isomorphism of functors.

CategoryTheory.Functor.isRightKanExtension_iff_postcomp₁ theorem

 (α : L' ⋙ F' ⟶ F) :
  F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)

Full source

lemma isRightKanExtension_iff_postcomp₁ (α : L' ⋙ F'L' ⋙ F' ⟶ F) :
    F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension
      ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α) := by
  let eq : (RightExtension.mk _ α).IsUniversal ≃
    (RightExtension.mk _
      ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

Equivalence of Right Kan Extension Conditions under Postcomposition with Natural Isomorphism

Informal description

Given functors $L' \colon C \to D$, $F \colon C \to H$, and $F' \colon D \to H$, along with a natural transformation $\alpha \colon L' \circ F' \to F$, the pair $(F', \alpha)$ is a right Kan extension of $F$ along $L'$ if and only if the pair $(G \circ F', \beta)$ is a right Kan extension of $F$ along $L$, where $\beta$ is the natural transformation obtained by composing the associator isomorphism with the whiskering of $e$ by $F'$ and then with $\alpha$. Here, $G \colon C' \to C$ is another functor and $e \colon L \circ G \cong L'$ is a natural isomorphism.

CategoryTheory.Functor.LeftExtension.precomp definition

: LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F)

Full source

/-- The functor `LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F)`
obtained by precomposition. -/
@[simps!]
def LeftExtension.precomp : LeftExtensionLeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F) :=
  StructuredArrow.map₂ (F := 𝟭 _) (G := (whiskeringLeft C' C H).obj G) (𝟙 _) (𝟙 _)

Precomposition functor for left Kan extensions

Informal description

The functor `LeftExtension.precomp` maps a left extension of functors $L \colon C \to D$ and $F \colon C \to H$ to a left extension of the composed functors $G \circ L \colon C' \to D$ and $G \circ F \colon C' \to H$, where $G \colon C' \to C$ is another functor. This is constructed using the identity natural transformation and the identity morphism in the context of structured arrows.

CategoryTheory.Functor.RightExtension.precomp definition

: RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F)

Full source

/-- The functor `RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F)`
obtained by precomposition. -/
@[simps!]
def RightExtension.precomp : RightExtensionRightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F) :=
  CostructuredArrow.map₂ (F := 𝟭 _) (G := (whiskeringLeft C' C H).obj G) (𝟙 _) (𝟙 _)

Precomposition functor for right Kan extensions

Informal description

The functor `RightExtension.precomp` maps a right extension $(F', \alpha)$ of $F$ along $L$ to the right extension $(G \circ F', \beta)$ of $G \circ F$ along $G \circ L$, where $\beta$ is the natural transformation obtained by precomposing $\alpha$ with $G$. This functor is defined using the costructured arrow construction with identity natural transformations.

CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp instance

: IsEquivalence (LeftExtension.precomp L F G)

Full source

noncomputable instance : IsEquivalence (LeftExtension.precomp L F G) := by
  apply StructuredArrow.isEquivalenceMap₂

Precomposition Functor for Left Kan Extensions is an Equivalence

Informal description

The precomposition functor for left Kan extensions, which maps a left extension of functors $L \colon C \to D$ and $F \colon C \to H$ to a left extension of the composed functors $G \circ L \colon C' \to D$ and $G \circ F \colon C' \to H$ (where $G \colon C' \to C$ is another functor), is an equivalence of categories.

CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp instance

: IsEquivalence (RightExtension.precomp L F G)

Full source

noncomputable instance : IsEquivalence (RightExtension.precomp L F G) := by
  apply CostructuredArrow.isEquivalenceMap₂

Precomposition Functor for Right Kan Extensions is an Equivalence

Informal description

The precomposition functor for right Kan extensions, which maps a right extension $(F', \alpha)$ of $F$ along $L$ to the right extension $(G \circ F', \beta)$ of $G \circ F$ along $G \circ L$, is an equivalence of categories.

CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv definition

(e : LeftExtension L F) : e.IsUniversal ≃ ((LeftExtension.precomp L F G).obj e).IsUniversal

Full source

/-- If `G` is an equivalence, then a left extension of `F` along `L` is universal iff
the corresponding left extension of `G ⋙ F` along `G ⋙ L` is. -/
noncomputable def LeftExtension.isUniversalPrecompEquiv (e : LeftExtension L F) :
    e.IsUniversal ≃ ((LeftExtension.precomp L F G).obj e).IsUniversal := by
  apply IsInitial.isInitialIffObj (LeftExtension.precomp L F G)

Equivalence of universality under precomposition for left Kan extensions

Informal description

Given a left extension $e$ of functors $L \colon C \to D$ and $F \colon C \to H$, the property that $e$ is universal is equivalent to the property that its precomposition with a functor $G \colon C' \to C$ is universal. In other words, $e$ is a universal left extension if and only if the corresponding left extension of $G \circ F$ along $G \circ L$ is universal.

CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv definition

(e : RightExtension L F) : e.IsUniversal ≃ ((RightExtension.precomp L F G).obj e).IsUniversal

Full source

/-- If `G` is an equivalence, then a right extension of `F` along `L` is universal iff
the corresponding left extension of `G ⋙ F` along `G ⋙ L` is. -/
noncomputable def RightExtension.isUniversalPrecompEquiv (e : RightExtension L F) :
    e.IsUniversal ≃ ((RightExtension.precomp L F G).obj e).IsUniversal := by
  apply IsTerminal.isTerminalIffObj (RightExtension.precomp L F G)

Equivalence of universality under precomposition for right Kan extensions

Informal description

Given a right extension $(F', \alpha)$ of $F$ along $L$, the property of $(F', \alpha)$ being a universal right Kan extension is equivalent to the property of its precomposition $(G \circ F', \beta)$ being a universal right Kan extension of $G \circ F$ along $G \circ L$, where $\beta$ is the natural transformation obtained by precomposing $\alpha$ with $G$.

CategoryTheory.Functor.isLeftKanExtension_iff_precomp theorem

 (α : F ⟶ L ⋙ F') : F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (whiskerLeft G α ≫ (Functor.associator _ _ _).inv)

Full source

lemma isLeftKanExtension_iff_precomp (α : F ⟶ L ⋙ F') :
    F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension
      (whiskerLeft G α ≫ (Functor.associator _ _ _).inv) := by
  let eq : (LeftExtension.mk _ α).IsUniversal ≃ (LeftExtension.mk _
      (whiskerLeft G α ≫ (Functor.associator _ _ _).inv)).IsUniversal :=
    (LeftExtension.isUniversalPrecompEquiv L F G _).trans
    (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Characterization of Left Kan Extensions via Precomposition

Informal description

Given functors $F \colon C \to H$, $L \colon C \to D$, and $F' \colon D \to H$, and a natural transformation $\alpha \colon F \to L \circ F'$, the pair $(F', \alpha)$ is a left Kan extension of $F$ along $L$ if and only if for any functor $G \colon C' \to C$, the pair $(F', \beta)$ is a left Kan extension of $G \circ F$ along $G \circ L$, where $\beta$ is the natural transformation obtained by whiskering $\alpha$ with $G$ and composing with the associator isomorphism.

CategoryTheory.Functor.isRightKanExtension_iff_precomp theorem

 (α : L ⋙ F' ⟶ F) : F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((Functor.associator _ _ _).hom ≫ whiskerLeft G α)

Full source

lemma isRightKanExtension_iff_precomp (α : L ⋙ F'L ⋙ F' ⟶ F) :
    F'.IsRightKanExtension α ↔
      F'.IsRightKanExtension ((Functor.associator _ _ _).hom ≫ whiskerLeft G α) := by
  let eq : (RightExtension.mk _ α).IsUniversal ≃ (RightExtension.mk _
      ((Functor.associator _ _ _).hom ≫ whiskerLeft G α)).IsUniversal :=
    (RightExtension.isUniversalPrecompEquiv L F G _).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

Right Kan Extension Property is Preserved under Precomposition with Functor $G$

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, $ F' \colon D \to H $, and $ G \colon H \to E $, along with a natural transformation $ \alpha \colon L \circ F' \to F $, the pair $(F', \alpha)$ is a right Kan extension of $ F $ along $ L $ if and only if the pair $(F', \beta)$ is a right Kan extension of $ G \circ F $ along $ G \circ L $, where $\beta$ is the natural transformation obtained by composing the associator isomorphism with the left whiskering of $\alpha$ by $G$.

CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁ definition

: RightExtension L F ≌ RightExtension L' F

Full source

/-- The equivalence `RightExtension L F ≌ RightExtension L' F` induced by
a natural isomorphism `L ≅ L'`. -/
def rightExtensionEquivalenceOfIso₁ : RightExtensionRightExtension L F ≌ RightExtension L' F :=
  CostructuredArrow.mapNatIso ((whiskeringLeft C D H).mapIso iso₁)

Equivalence of right extension categories induced by natural isomorphism of functors

Informal description

Given functors $ L, L' \colon C \to D $ and $ F \colon C \to H $, a natural isomorphism $ \text{iso}_1 \colon L \cong L' $ induces an equivalence of categories between the category of right extensions of $ F $ along $ L $ and the category of right extensions of $ F $ along $ L' $. Here, a right extension of $ F $ along $ L $ consists of a functor $ F' \colon D \to H $ and a natural transformation $ \alpha \colon L \circ F' \to F $.

CategoryTheory.Functor.hasRightExtension_iff_of_iso₁ theorem

: HasRightKanExtension L F ↔ HasRightKanExtension L' F

Full source

lemma hasRightExtension_iff_of_iso₁ : HasRightKanExtensionHasRightKanExtension L F ↔ HasRightKanExtension L' F :=
  (rightExtensionEquivalenceOfIso₁ iso₁ F).hasTerminal_iff

Equivalence of Right Kan Extension Existence under Natural Isomorphism of Functors

Informal description

Given functors $L, L' \colon C \to D$ and $F \colon C \to H$, and a natural isomorphism $\text{iso}_1 \colon L \cong L'$, the following are equivalent: 1. There exists a right Kan extension of $F$ along $L$. 2. There exists a right Kan extension of $F$ along $L'$.

CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ definition

: LeftExtension L F ≌ LeftExtension L' F

Full source

/-- The equivalence `LeftExtension L F ≌ LeftExtension L' F` induced by
a natural isomorphism `L ≅ L'`. -/
def leftExtensionEquivalenceOfIso₁ : LeftExtensionLeftExtension L F ≌ LeftExtension L' F :=
  StructuredArrow.mapNatIso ((whiskeringLeft C D H).mapIso iso₁)

Equivalence of left extension categories induced by natural isomorphism of functors

Informal description

Given functors $ L, L' \colon C \to D $ and $ F \colon C \to H $, and a natural isomorphism $ \text{iso}_1 \colon L \cong L' $, there is an equivalence of categories between the category of left extensions of $ F $ along $ L $ and the category of left extensions of $ F $ along $ L' $. This equivalence is induced by post-composing with the natural isomorphism $ \text{iso}_1 $.

CategoryTheory.Functor.hasLeftExtension_iff_of_iso₁ theorem

: HasLeftKanExtension L F ↔ HasLeftKanExtension L' F

Full source

lemma hasLeftExtension_iff_of_iso₁ : HasLeftKanExtensionHasLeftKanExtension L F ↔ HasLeftKanExtension L' F :=
  (leftExtensionEquivalenceOfIso₁ iso₁ F).hasInitial_iff

Existence of Left Kan Extensions is Preserved under Natural Isomorphism of Functors

Informal description

Given functors $L, L' \colon C \to D$ and $F \colon C \to H$, and a natural isomorphism $\text{iso}_1 \colon L \cong L'$, the left Kan extension of $F$ along $L$ exists if and only if the left Kan extension of $F$ along $L'$ exists.

CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂ definition

: RightExtension L F ≌ RightExtension L F'

Full source

/-- The equivalence `RightExtension L F ≌ RightExtension L F'` induced by
a natural isomorphism `F ≅ F'`. -/
def rightExtensionEquivalenceOfIso₂ : RightExtensionRightExtension L F ≌ RightExtension L F' :=
  CostructuredArrow.mapIso iso₂

Equivalence of right extension categories induced by isomorphism of target functors

Informal description

Given a natural isomorphism $\alpha \colon F \cong F'$ between functors $F, F' \colon C \to H$, there is an equivalence of categories between the category of right extensions of $F$ along $L$ and the category of right extensions of $F'$ along $L$. Here, a right extension of $F$ along $L$ consists of a functor $G \colon D \to H$ and a natural transformation $\beta \colon L \circ G \to F$.

CategoryTheory.Functor.hasRightExtension_iff_of_iso₂ theorem

: HasRightKanExtension L F ↔ HasRightKanExtension L F'

Full source

lemma hasRightExtension_iff_of_iso₂ : HasRightKanExtensionHasRightKanExtension L F ↔ HasRightKanExtension L F' :=
  (rightExtensionEquivalenceOfIso₂ L iso₂).hasTerminal_iff

Existence of Right Kan Extensions is Preserved under Natural Isomorphism of Functors

Informal description

Given a natural isomorphism $\alpha \colon F \cong F'$ between functors $F, F' \colon C \to H$, the functor $F$ has a right Kan extension along $L \colon C \to D$ if and only if $F'$ has a right Kan extension along $L$.

CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂ definition

: LeftExtension L F ≌ LeftExtension L F'

Full source

/-- The equivalence `LeftExtension L F ≌ LeftExtension L F'` induced by
a natural isomorphism `F ≅ F'`. -/
def leftExtensionEquivalenceOfIso₂ : LeftExtensionLeftExtension L F ≌ LeftExtension L F' :=
  StructuredArrow.mapIso iso₂

Equivalence of left extension categories induced by natural isomorphism of functors

Informal description

Given a natural isomorphism $F \cong F'$ between functors $F, F' \colon C \to H$, there is an equivalence of categories between the category of left extensions of $F$ along $L$ and the category of left extensions of $F'$ along $L$. Here, a left extension of $F$ along $L$ consists of a functor $F' \colon D \to H$ equipped with a natural transformation $\alpha \colon F \to L \circ F'$.

CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂ theorem

: HasLeftKanExtension L F ↔ HasLeftKanExtension L F'

Full source

lemma hasLeftExtension_iff_of_iso₂ : HasLeftKanExtensionHasLeftKanExtension L F ↔ HasLeftKanExtension L F' :=
  (leftExtensionEquivalenceOfIso₂ L iso₂).hasInitial_iff

Existence of Left Kan Extensions is Preserved Under Natural Isomorphism of Functors

Informal description

Given functors $L \colon C \to D$ and natural isomorphic functors $F, F' \colon C \to H$, there exists a left Kan extension of $F$ along $L$ if and only if there exists a left Kan extension of $F'$ along $L$.

CategoryTheory.Functor.LeftExtension.isUniversalEquivOfIso₂ definition

 (α₁ : LeftExtension L F₁) (α₂ : LeftExtension L F₂) (e : F₁ ≅ F₂) (e' : α₁.right ≅ α₂.right)
  (h : α₁.hom ≫ whiskerLeft L e'.hom = e.hom ≫ α₂.hom) : α₁.IsUniversal ≃ α₂.IsUniversal

Full source

/-- When two left extensions `α₁ : LeftExtension L F₁` and `α₂ : LeftExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is. -/
noncomputable def LeftExtension.isUniversalEquivOfIso₂
    (α₁ : LeftExtension L F₁) (α₂ : LeftExtension L F₂) (e : F₁ ≅ F₂)
    (e' : α₁.right ≅ α₂.right)
    (h : α₁.hom ≫ whiskerLeft L e'.hom = e.hom ≫ α₂.hom) :
    α₁.IsUniversal ≃ α₂.IsUniversal :=
  (IsInitial.isInitialIffObj (leftExtensionEquivalenceOfIso₂ L e).functor α₁).trans
    (IsInitial.equivOfIso (StructuredArrow.isoMk e'
      (by simp [leftExtensionEquivalenceOfIso₂, h])))

Equivalence of universality for left extensions under natural isomorphism

Informal description

Given two left extensions $\alpha_1 \colon F_1 \to L \circ F_1'$ and $\alpha_2 \colon F_2 \to L \circ F_2'$ along a functor $L \colon C \to D$, and given natural isomorphisms $e \colon F_1 \cong F_2$ and $e' \colon F_1' \cong F_2'$ such that the diagram \[ \alpha_1 \circ (L \circ e') = e \circ \alpha_2 \] commutes, there is an equivalence between the properties that $\alpha_1$ is universal and $\alpha_2$ is universal. Here, universality means that the extension is initial in the category of left extensions.

CategoryTheory.Functor.isLeftKanExtension_iff_of_iso₂ theorem

 {F₁' F₂' : D ⥤ H} (α₁ : F₁ ⟶ L ⋙ F₁') (α₂ : F₂ ⟶ L ⋙ F₂') (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂')
  (h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂) : F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂

Full source

lemma isLeftKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : F₁ ⟶ L ⋙ F₁') (α₂ : F₂ ⟶ L ⋙ F₂')
    (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂) :
    F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂ := by
  let eq := LeftExtension.isUniversalEquivOfIso₂ (LeftExtension.mk _ α₁)
    (LeftExtension.mk _ α₂) e e' h
  constructor
  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩
  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩

Left Kan Extension Property is Preserved Under Natural Isomorphism

Informal description

Let $L \colon C \to D$ and $F_1, F_2 \colon C \to H$ be functors, and let $F_1', F_2' \colon D \to H$ be functors equipped with natural transformations $\alpha_1 \colon F_1 \to L \circ F_1'$ and $\alpha_2 \colon F_2 \to L \circ F_2'$. Given natural isomorphisms $e \colon F_1 \cong F_2$ and $e' \colon F_1' \cong F_2'$ such that the diagram \[ \alpha_1 \circ (L \circ e') = e \circ \alpha_2 \] commutes, then $(F_1', \alpha_1)$ is a left Kan extension of $F_1$ along $L$ if and only if $(F_2', \alpha_2)$ is a left Kan extension of $F_2$ along $L$.

CategoryTheory.Functor.RightExtension.isUniversalEquivOfIso₂ definition

 (α₁ : RightExtension L F₁) (α₂ : RightExtension L F₂) (e : F₁ ≅ F₂) (e' : α₁.left ≅ α₂.left)
  (h : whiskerLeft L e'.hom ≫ α₂.hom = α₁.hom ≫ e.hom) : α₁.IsUniversal ≃ α₂.IsUniversal

Full source

/-- When two right extensions `α₁ : RightExtension L F₁` and `α₂ : RightExtension L F₂`
are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
then `α₁` is universal iff `α₂` is. -/
noncomputable def RightExtension.isUniversalEquivOfIso₂
    (α₁ : RightExtension L F₁) (α₂ : RightExtension L F₂) (e : F₁ ≅ F₂)
    (e' : α₁.left ≅ α₂.left)
    (h : whiskerLeftwhiskerLeft L e'.hom ≫ α₂.hom = α₁.hom ≫ e.hom) :
    α₁.IsUniversal ≃ α₂.IsUniversal :=
  (IsTerminal.isTerminalIffObj (rightExtensionEquivalenceOfIso₂ L e).functor α₁).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk e'
      (by simp [rightExtensionEquivalenceOfIso₂, h])))

Equivalence of universality for right extensions under isomorphism of target functors

Informal description

Given two right extensions $\alpha_1 \colon L \circ F_1' \to F_1$ and $\alpha_2 \colon L \circ F_2' \to F_2$ along a functor $L \colon C \to D$, and given isomorphisms $e \colon F_1 \cong F_2$ and $e' \colon F_1' \cong F_2'$ such that the diagram \[ \begin{CD} L \circ F_1' @>{L \circ e'}>> L \circ F_2' \\ @V{\alpha_1}VV @VV{\alpha_2}V \\ F_1 @>>{e}> F_2 \end{CD} \] commutes, there is an equivalence between the properties that $\alpha_1$ is universal and that $\alpha_2$ is universal. Here, universality means that the corresponding object in the category of right extensions is terminal.

CategoryTheory.Functor.isRightKanExtension_iff_of_iso₂ theorem

 {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F₁' ⟶ F₁) (α₂ : L ⋙ F₂' ⟶ F₂) (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂')
  (h : whiskerLeft L e'.hom ≫ α₂ = α₁ ≫ e.hom) : F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂

Full source

lemma isRightKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F₁'L ⋙ F₁' ⟶ F₁) (α₂ : L ⋙ F₂'L ⋙ F₂' ⟶ F₂)
    (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : whiskerLeftwhiskerLeft L e'.hom ≫ α₂ = α₁ ≫ e.hom) :
    F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂ := by
  let eq := RightExtension.isUniversalEquivOfIso₂ (RightExtension.mk _ α₁)
    (RightExtension.mk _ α₂) e e' h
  constructor
  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩
  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩

Equivalence of Right Kan Extension Property under Isomorphism of Target Functors

Informal description

Let $L \colon C \to D$ be a functor, and let $F_1, F_2 \colon C \to H$ and $F_1', F_2' \colon D \to H$ be functors. Given natural transformations $\alpha_1 \colon L \circ F_1' \to F_1$ and $\alpha_2 \colon L \circ F_2' \to F_2$, and isomorphisms $e \colon F_1 \cong F_2$ and $e' \colon F_1' \cong F_2'$ such that the diagram \[ \begin{CD} L \circ F_1' @>{L \circ e'}>> L \circ F_2' \\ @V{\alpha_1}VV @VV{\alpha_2}V \\ F_1 @>>{e}> F_2 \end{CD} \] commutes, then $F_1'$ is a right Kan extension of $F_1$ along $L$ via $\alpha_1$ if and only if $F_2'$ is a right Kan extension of $F_2$ along $L$ via $\alpha_2$.

CategoryTheory.Functor.coconeOfIsLeftKanExtension definition

(c : Cocone F) : Cocone F'

Full source

/-- Construct a cocone for a left Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
`L : C ⥤ D` given a cocone for `F`. -/
@[simps]
noncomputable def coconeOfIsLeftKanExtension (c : Cocone F) : Cocone F' where
  pt := c.pt
  ι := F'.descOfIsLeftKanExtension α _ c.ι

Cocone induced by a left Kan extension

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L$, and a cocone $c$ over $F$, this constructs a cocone over $F'$ with the same cocone point as $c$ and with the cocone legs induced by the universal property of the left Kan extension.

CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension definition

{c : Cocone F} (hc : IsColimit c) : IsColimit (F'.coconeOfIsLeftKanExtension α c)

Full source

/-- If `c` is a colimit cocone for a functor `F : C ⥤ H` and `α : F ⟶ L ⋙ F'` is the unit of any
left Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coconeOfIsLeftKanExtension α c` is
a colimit cocone, too. -/
@[simps]
def isColimitCoconeOfIsLeftKanExtension {c : Cocone F} (hc : IsColimit c) :
    IsColimit (F'.coconeOfIsLeftKanExtension α c) where
  desc s := hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))
  fac s := by
    have : F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
        (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) = s.ι :=
      F'.hom_ext_of_isLeftKanExtension α _ _ (by aesop_cat)
    exact congr_app this
  uniq s m hm := hc.hom_ext (fun j ↦ by
    have := hm (L.obj j)
    nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)]
    dsimp at this ⊢
    rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app])

Preservation of colimits by left Kan extensions

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L \colon C \to D$, and a colimit cocone $c$ over $F$, the cocone $F'.\text{coconeOfIsLeftKanExtension}\, \alpha\, c$ is also a colimit cocone. This means that the left Kan extension preserves the colimit property of the original cocone.

CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension definition

: colimit F' ≅ colimit F

Full source

/-- If `F' : D ⥤ H` is a left Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the colimit over `F'`
is isomorphic to the colimit over `F`. -/
noncomputable def colimitIsoOfIsLeftKanExtension : colimitcolimit F' ≅ colimit F :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit F')
    (F'.isColimitCoconeOfIsLeftKanExtension α (colimit.isColimit F))

Isomorphism between colimits induced by a left Kan extension

Informal description

Given a natural transformation $\alpha \colon F \to L \circ F'$ where $(F', \alpha)$ is a left Kan extension of $F$ along $L \colon C \to D$, there exists a canonical isomorphism between the colimit of $F'$ and the colimit of $F$. This isomorphism is constructed using the universal property of colimits and the fact that left Kan extensions preserve colimits.

CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom theorem

(i : C) : α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom = colimit.ι F i

Full source

@[reassoc (attr := simp)]
lemma ι_colimitIsoOfIsLeftKanExtension_hom (i : C) :
    α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom =
      colimit.ι F i := by
  simp [colimitIsoOfIsLeftKanExtension]

Compatibility of colimit coprojections with left Kan extension isomorphism

Informal description

For any object $i$ in category $C$, the composition of the natural transformation component $\alpha_i \colon F(i) \to F'(L(i))$, the colimit coprojection $\iota_{L(i)} \colon F'(L(i)) \to \text{colimit } F'$, and the isomorphism $\text{colimit } F' \cong \text{colimit } F$ equals the colimit coprojection $\iota_i \colon F(i) \to \text{colimit } F$. In symbols: $$ \alpha_i \circ \iota_{L(i)} \circ (\text{colimit } F' \cong \text{colimit } F).\text{hom} = \iota_i. $$

CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv theorem

(i : C) : colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = α.app i ≫ colimit.ι F' (L.obj i)

Full source

@[reassoc (attr := simp)]
lemma ι_colimitIsoOfIsLeftKanExtension_inv (i : C) :
    colimit.ιcolimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv =
    α.app i ≫ colimit.ι F' (L.obj i) := by
  rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]

Compatibility of colimit coprojections with inverse of left Kan extension isomorphism

Informal description

For any object $i$ in category $C$, the composition of the colimit coprojection $\iota_i \colon F(i) \to \text{colimit } F$ with the inverse of the isomorphism $\text{colimit } F' \cong \text{colimit } F$ equals the composition of the natural transformation component $\alpha_i \colon F(i) \to F'(L(i))$ with the colimit coprojection $\iota_{L(i)} \colon F'(L(i)) \to \text{colimit } F'$. In symbols: $$ \iota_i \circ (\text{colimit } F' \cong \text{colimit } F)^{-1} = \alpha_i \circ \iota_{L(i)}. $$

CategoryTheory.Functor.coneOfIsRightKanExtension definition

(c : Cone F) : Cone F'

Full source

/-- Construct a cone for a right Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
`L : C ⥤ D` given a cone for `F`. -/
@[simps]
noncomputable def coneOfIsRightKanExtension (c : Cone F) : Cone F' where
  pt := c.pt
  π := F'.liftOfIsRightKanExtension α _ c.π

Cone construction from right Kan extension property

Informal description

Given a functor $ F' \colon D \to H $ that is a right Kan extension of $ F \colon C \to H $ along a functor $ L \colon C \to D $, and given a cone $ c $ over $ F $, this constructs a cone over $ F' $ with the same apex $ c.\mathrm{pt} $. The natural transformation of the new cone is obtained by lifting the natural transformation $ c.\pi $ of the original cone through the universal property of the right Kan extension.

CategoryTheory.Functor.isLimitConeOfIsRightKanExtension definition

{c : Cone F} (hc : IsLimit c) : IsLimit (F'.coneOfIsRightKanExtension α c)

Full source

/-- If `c` is a limit cone for a functor `F : C ⥤ H` and `α : L ⋙ F' ⟶ F` is the counit of any
right Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coneOfIsRightKanExtension α c` is
a limit cone, too. -/
@[simps]
def isLimitConeOfIsRightKanExtension {c : Cone F} (hc : IsLimit c) :
    IsLimit (F'.coneOfIsRightKanExtension α c) where
  lift s := hc.lift (Cone.mk _ (whiskerLeftwhiskerLeft L s.π ≫ α))
  fac s := by
    have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
      F'.hom_ext_of_isRightKanExtension α _ _ (by aesop_cat)
    exact congr_app this
  uniq s m hm := hc.hom_ext (fun j ↦ by
    have := hm (L.obj j)
    nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)]
    dsimp at this ⊢
    rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app])

Limit cone preservation under right Kan extension

Informal description

Given a functor $ F' \colon D \to H $ that is a right Kan extension of $ F \colon C \to H $ along a functor $ L \colon C \to D $, and given a limit cone $ c $ over $ F $, the cone $ F'.\text{coneOfIsRightKanExtension}\, \alpha\, c $ is also a limit cone. Here, $ \alpha \colon L \circ F' \to F $ is the counit of the right Kan extension.

CategoryTheory.Functor.limitIsoOfIsRightKanExtension definition

: limit F' ≅ limit F

Full source

/-- If `F' : D ⥤ H` is a right Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the limit over `F'`
is isomorphic to the limit over `F`. -/
noncomputable def limitIsoOfIsRightKanExtension : limitlimit F' ≅ limit F :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit F')
    (F'.isLimitConeOfIsRightKanExtension α (limit.isLimit F))

Isomorphism between limits under right Kan extension

Informal description

Given functors $ L \colon C \to D $, $ F \colon C \to H $, and $ F' \colon D \to H $, where $ F' $ is a right Kan extension of $ F $ along $ L $ with counit $ \alpha \colon L \circ F' \to F $, the limit of $ F' $ is isomorphic to the limit of $ F $. This isomorphism is constructed using the universal property of the right Kan extension and the uniqueness of limit objects up to isomorphism.

CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π theorem

(i : C) : (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i

Full source

@[reassoc (attr := simp)]
lemma limitIsoOfIsRightKanExtension_inv_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i := by
  simp [limitIsoOfIsRightKanExtension]

Componentwise Compatibility of Right Kan Extension Limit Isomorphism with Projections

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F' \colon D \to H$ be a right Kan extension of $F$ along $L$ with counit $\alpha \colon L \circ F' \to F$. For any object $i \in C$, the composition of the inverse of the isomorphism $\text{limit } F' \cong \text{limit } F$ with the projection $\pi_{L(i)} \colon \text{limit } F' \to F'(L(i))$ and the component $\alpha_i \colon F'(L(i)) \to F(i)$ equals the projection $\pi_i \colon \text{limit } F \to F(i)$. In symbols: $$(\text{limitIsoOfIsRightKanExtension}\, \alpha)^{-1} \circ \pi_{L(i)} \circ \alpha_i = \pi_i$$

CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π theorem

(i : C) : (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i

Full source

@[reassoc (attr := simp)]
lemma limitIsoOfIsRightKanExtension_hom_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.πlimit.π F' (L.obj i) ≫ α.app i := by
  rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]

Compatibility of Right Kan Extension Limit Isomorphism with Projections

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $F' \colon D \to H$ be a right Kan extension of $F$ along $L$ with counit $\alpha \colon L \circ F' \to F$. For any object $i \in C$, the composition of the isomorphism $\text{limit } F' \cong \text{limit } F$ with the projection $\pi_i \colon \text{limit } F \to F(i)$ equals the composition of the projection $\pi_{L(i)} \colon \text{limit } F' \to F'(L(i))$ with the component $\alpha_i \colon F'(L(i)) \to F(i)$. In symbols: $$(\text{limitIsoOfIsRightKanExtension}\, \alpha) \circ \pi_i = \pi_{L(i)} \circ \alpha_i$$

References