Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

CategoryTheory.Functor.lan definition

: (C ⥤ H) ⥤ (D ⥤ H)

Full source

/-- The left Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`. -/
noncomputable def lan : (C ⥤ H) ⥤ (D ⥤ H) where
  obj F := leftKanExtension L F
  map {F₁ F₂} φ := descOfIsLeftKanExtension _ (leftKanExtensionUnit L F₁) _
    (φ ≫ leftKanExtensionUnit L F₂)

Left Kan extension functor

Informal description

The left Kan extension functor along a functor $L \colon C \to D$ is a functor from the functor category $(C \to H)$ to the functor category $(D \to H)$. For any functor $F \colon C \to H$, it maps $F$ to its left Kan extension along $L$, denoted $\text{lan}_L F$. The action on morphisms is given by the universal property of the left Kan extension.

CategoryTheory.Functor.lanUnit definition

: (𝟭 (C ⥤ H)) ⟶ L.lan ⋙ (whiskeringLeft C D H).obj L

Full source

/-- The natural transformation `F ⟶ L ⋙ (L.lan).obj G`. -/
noncomputable def lanUnit : (𝟭 (C ⥤ H)) ⟶ L.lan ⋙ (whiskeringLeft C D H).obj L where
  app F := leftKanExtensionUnit L F
  naturality {F₁ F₂} φ := by ext; simp [lan]

Left Kan extension unit natural transformation

Informal description

The natural transformation $\text{lanUnit}$ from the identity functor on the functor category $(C \to H)$ to the composition of the left Kan extension functor $\text{lan}_L$ with the left whiskering functor along $L$. For any functor $F \colon C \to H$, the component $\text{lanUnit}_F$ is given by the left Kan extension unit of $F$ along $L$.

CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit instance

(F : C ⥤ H) : (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F)

Full source

instance (F : C ⥤ H) : (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F) := by
  dsimp [lan, lanUnit]
  infer_instance

Left Kan Extension Property of $\text{lan}_L F$

Informal description

For any functor $F \colon C \to H$, the left Kan extension $\text{lan}_L F$ of $F$ along $L \colon C \to D$ is indeed a left Kan extension, with the unit natural transformation $\text{lanUnit}_F$ providing the universal property.

CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit definition

 (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] :
  (LeftExtension.mk _ (L.leftKanExtensionUnit F)).IsPointwiseLeftKanExtension

Full source

/-- If there exists a pointwise left Kan extension of `F` along `L`,
then `L.lan.obj G` is a pointwise left Kan extension of `F`. -/
noncomputable def isPointwiseLeftKanExtensionLeftKanExtensionUnit
    (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] :
    (LeftExtension.mk _ (L.leftKanExtensionUnit F)).IsPointwiseLeftKanExtension :=
  isPointwiseLeftKanExtensionOfIsLeftKanExtension (F := F) _ (leftKanExtensionUnit L F)

Pointwise left Kan extension property of the left Kan extension unit

Informal description

For a functor $F \colon C \to H$ that has a pointwise left Kan extension along $L \colon C \to D$, the left extension $\text{LeftExtension.mk}\, (L.\text{leftKanExtension}\, F)\, (L.\text{leftKanExtensionUnit}\, F)$ is a pointwise left Kan extension of $F$ along $L$.

CategoryTheory.Functor.leftKanExtensionObjIsoColimit definition

[HasLeftKanExtension L F] (X : D) : (L.leftKanExtension F).obj X ≅ colimit (proj L X ⋙ F)

Full source

/-- If a left Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a colimit. -/
noncomputable def leftKanExtensionObjIsoColimit [HasLeftKanExtension L F] (X : D) :
    (L.leftKanExtension F).obj X ≅ colimit (proj L X ⋙ F) :=
  LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit (F := F)
   (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X)

Isomorphism between left Kan extension and colimit of costructured arrows

Informal description

For a functor $ F \colon C \to H $ that has a left Kan extension along $ L \colon C \to D $, and for any object $ X \in D $, the value of the left Kan extension $ \text{lan}_L F $ at $ X $ is isomorphic to the colimit of the functor $ \text{proj}_L X \circ F $, where $ \text{proj}_L X $ is the projection functor from the category of $ L $-costructured arrows over $ X $.

CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv theorem

 [HasLeftKanExtension L F] (X : D) (f : CostructuredArrow L X) :
  colimit.ι _ f ≫ (L.leftKanExtensionObjIsoColimit F X).inv =
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom

Full source

@[reassoc (attr := simp)]
lemma ι_leftKanExtensionObjIsoColimit_inv [HasLeftKanExtension L F] (X : D)
    (f : CostructuredArrow L X) :
    colimit.ιcolimit.ι _ f ≫ (L.leftKanExtensionObjIsoColimit F X).inv =
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom := by
  simp [leftKanExtensionObjIsoColimit, lanUnit]

Compatibility of colimit coprojection with left Kan extension isomorphism

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors such that $F$ has a left Kan extension along $L$. For any object $X \in D$ and any morphism $f \colon L(Y) \to X$ in the category of $L$-costructured arrows over $X$, the composition of the colimit coprojection $\iota_f \colon F(Y) \to \mathrm{colimit}\, (\mathrm{proj}_L X \circ F)$ with the inverse of the isomorphism $(L.\mathrm{leftKanExtension}\, F)(X) \cong \mathrm{colimit}\, (\mathrm{proj}_L X \circ F)$ equals the composition of the left Kan extension unit $(\eta_F)_Y \colon F(Y) \to (L.\mathrm{leftKanExtension}\, F)(L(Y))$ with $(L.\mathrm{leftKanExtension}\, F)(f) \colon (L.\mathrm{leftKanExtension}\, F)(L(Y)) \to (L.\mathrm{leftKanExtension}\, F)(X)$. In symbols: \[ \iota_f \circ (L.\mathrm{leftKanExtensionObjIsoColimit}\, F\, X)^{-1} = (\eta_F)_Y \circ (L.\mathrm{leftKanExtension}\, F)(f) \]

CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom theorem

 (X : D) (f : CostructuredArrow L X) :
  (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom ≫ (L.leftKanExtensionObjIsoColimit F X).hom =
    colimit.ι (proj L X ⋙ F) f

Full source

@[reassoc (attr := simp)]
lemma ι_leftKanExtensionObjIsoColimit_hom (X : D) (f : CostructuredArrow L X) :
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom ≫
      (L.leftKanExtensionObjIsoColimit F X).hom =
    colimit.ι (projproj L X ⋙ F) f :=
  LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom (F := F)
    (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X) f

Compatibility of Left Kan Extension with Colimit Coprojections

Informal description

For any object $X$ in category $D$ and any morphism $f$ in the category of $L$-costructured arrows over $X$, the composition of: 1. the component of the left Kan extension unit $\eta_F$ at $f.\text{left}$, 2. the image of $f.\text{hom}$ under the left Kan extension functor $\text{lan}_L F$, and 3. the isomorphism $\text{lan}_L F(X) \cong \text{colimit}(\text{proj}_L X \circ F)$, equals the coprojection $\iota_f$ from $F(f.\text{left})$ to the colimit of $\text{proj}_L X \circ F$.

CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom theorem

 (X : D) (f : CostructuredArrow L X) :
  (leftKanExtensionUnit L F).app f.left ≫ (leftKanExtension L F).map f.hom ≫ (L.leftKanExtensionObjIsoColimit F X).hom =
    colimit.ι (proj L X ⋙ F) f

Full source

lemma leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom (X : D)
    (f : CostructuredArrow L X) :
    (leftKanExtensionUnit L F).app f.left ≫ (leftKanExtension L F).map f.hom ≫
       (L.leftKanExtensionObjIsoColimit F X).hom =
    colimit.ι (projproj L X ⋙ F) f :=
  LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom (F := F)
    (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X) f

Compatibility of Left Kan Extension Unit with Colimit Coprojection

Informal description

For any object $X$ in category $D$ and any morphism $f$ in the category of $L$-costructured arrows over $X$, the composition of the following three morphisms: 1. The component of the left Kan extension unit $(L.\text{leftKanExtensionUnit}\, F)$ at the source of $f$, 2. The image of $f$ under the left Kan extension functor $(L.\text{leftKanExtension}\, F)$, 3. The isomorphism $(L.\text{leftKanExtensionObjIsoColimit}\, F\, X).\text{hom}$ between the left Kan extension and the colimit, equals the coprojection morphism $\text{colimit.ι}\, (\text{proj}\, L\, X \circ F)\, f$ from the value of the functor at $f$ to the colimit.

CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom theorem

 (X : C) :
  (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 _))

Full source

@[reassoc (attr := simp)]
lemma leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom (X : C) :
    (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (projproj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 _)) := by
  simpa using leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom L F
    (L.obj X) (CostructuredArrow.mk (𝟙 _))

Compatibility of Left Kan Extension Unit with Colimit Coprojection at Identity

Informal description

For any object $X$ in category $C$, the composition of: 1. the component of the left Kan extension unit $\eta_F$ at $X$, and 2. the isomorphism $\text{lan}_L F(L(X)) \cong \text{colimit}(\text{proj}_L (L(X)) \circ F)$, equals the coprojection $\iota_{(\text{id}_{L(X)})}$ from $F(X)$ to the colimit of $\text{proj}_L (L(X)) \circ F$, where $\text{id}_{L(X)}$ is the identity morphism on $L(X)$.

CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grotendieckProj theorem

{X Y : D} (f : X ⟶ Y) : HasColimit ((functor L).map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ⋙ F)

Full source

@[instance]
theorem hasColimit_map_comp_ι_comp_grotendieckProj {X Y : D} (f : X ⟶ Y) :
    HasColimit ((functor L).map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ⋙ F) :=
  hasColimit_of_iso (isoWhiskerRight (mapCompιCompGrothendieckProj L f) F)

Existence of colimit for composed functor involving Grothendieck construction and costructured arrows

Informal description

For any morphism $f \colon X \to Y$ in category $D$, the functor composition $(L.\text{functor}).\text{map}\, f \circ \text{Grothendieck.ι}\, (L.\text{functor})\, Y \circ \text{grothendieckProj}\, L \circ F$ has a colimit in category $H$. Here: - $L \colon C \to D$ is a functor between categories $C$ and $D$ - $F \colon C \to H$ is a functor from $C$ to $H$ - $\text{functor}\, L \colon D \to \text{Cat}$ is the functor sending objects in $D$ to categories of $L$-costructured arrows - $\text{Grothendieck.ι}$ is the inclusion functor into the Grothendieck construction - $\text{grothendieckProj}\, L$ is the projection functor from the Grothendieck construction back to $C$

CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit definition

[HasLeftKanExtension L F] : leftKanExtension L F ≅ fiberwiseColimit (grothendieckProj L ⋙ F)

Full source

/-- The left Kan extension of `F : C ⥤ H` along a functor `L : C ⥤ D` is isomorphic to the
fiberwise colimit of the projection functor on the Grothendieck construction of the costructured
arrow category composed with `F`. -/
@[simps!]
noncomputable def leftKanExtensionIsoFiberwiseColimit [HasLeftKanExtension L F] :
    leftKanExtensionleftKanExtension L F ≅ fiberwiseColimit (grothendieckProj L ⋙ F) :=
  letI : ∀ X, HasColimit (Grothendieck.ιGrothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) :=
      fun X => hasColimit_of_iso <| Iso.symm <|
        isoWhiskerRightisoWhiskerRight (eqToIso ((functor L).map_id X)) _ ≪≫
        Functor.leftUnitor (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F)
  Iso.symm <| NatIso.ofComponents
    (fun X => HasColimit.isoOfNatIsoHasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X) F) ≪≫
      (leftKanExtensionObjIsoColimit L F X).symm)
    fun f => colimit.hom_ext (by simp)

Isomorphism between left Kan extension and fiberwise colimit via Grothendieck construction

Informal description

For a functor $ F \colon C \to H $ that has a left Kan extension along $ L \colon C \to D $, the left Kan extension $ \text{lan}_L F $ is isomorphic to the fiberwise colimit of the composition of the projection functor $ \text{grothendieckProj}\, L $ from the Grothendieck construction of $ L $-costructured arrows, followed by $ F $. Here: - $ \text{grothendieckProj}\, L \colon \int (L.\text{functor}) \to C $ is the projection functor from the Grothendieck construction of $ L $-costructured arrows back to $ C $. - The fiberwise colimit is taken over the composition $ \text{grothendieckProj}\, L \circ F $.

CategoryTheory.Functor.lanAdjunction definition

: L.lan ⊣ (whiskeringLeft C D H).obj L

Full source

/-- The left Kan extension functor `L.Lan` is left adjoint to the precomposition by `L`. -/
noncomputable def lanAdjunction : L.lan ⊣ (whiskeringLeft C D H).obj L :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun F G => homEquivOfIsLeftKanExtension _ (L.lanUnit.app F) G
      homEquiv_naturality_left_symm := fun {F₁ F₂ G} f α =>
        hom_ext_of_isLeftKanExtension _ (L.lanUnit.app F₁) _ _ (by
          ext X
          dsimp [homEquivOfIsLeftKanExtension]
          rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
          have h := congr_app (L.lanUnit.naturality f) X
          dsimp at h ⊢
          rw [← h, assoc, descOfIsLeftKanExtension_fac_app] )
      homEquiv_naturality_right := fun {F G₁ G₂} β f => by
        dsimp [homEquivOfIsLeftKanExtension]
        rw [assoc] }

Adjunction between left Kan extension and precomposition

Informal description

The adjunction between the left Kan extension functor $\text{lan}_L \colon (C \to H) \to (D \to H)$ and the precomposition functor $(- \circ L) \colon (D \to H) \to (C \to H)$. For any functors $F \colon C \to H$ and $G \colon D \to H$, there is a natural bijection between natural transformations $\text{lan}_L F \Rightarrow G$ and $F \Rightarrow G \circ L$, given by the universal property of the left Kan extension. The unit of this adjunction is the natural transformation $\text{lanUnit}$ that embeds $F$ into its left Kan extension along $L$.

CategoryTheory.Functor.lanAdjunction_unit theorem

: (L.lanAdjunction H).unit = L.lanUnit

Full source

@[simp]
lemma lanAdjunction_unit : (L.lanAdjunction H).unit = L.lanUnit := by
  ext F : 2
  dsimp [lanAdjunction, homEquivOfIsLeftKanExtension]
  simp

Unit of Left Kan Extension Adjunction Equals LanUnit

Informal description

The unit of the adjunction between the left Kan extension functor $\text{lan}_L$ and the precomposition functor $(- \circ L)$ is equal to the natural transformation $\text{lanUnit}$.

CategoryTheory.Functor.lanAdjunction_counit_app theorem

 (G : D ⥤ H) :
  (L.lanAdjunction H).counit.app G = descOfIsLeftKanExtension (L.lan.obj (L ⋙ G)) (L.lanUnit.app (L ⋙ G)) G (𝟙 (L ⋙ G))

Full source

lemma lanAdjunction_counit_app (G : D ⥤ H) :
    (L.lanAdjunction H).counit.app G =
      descOfIsLeftKanExtension (L.lan.obj (L ⋙ G)) (L.lanUnit.app (L ⋙ G)) G (𝟙 (L ⋙ G)) :=
  rfl

Counit of Left Kan Extension Adjunction via Universal Property

Informal description

For any functor $G \colon D \to H$, the counit of the adjunction between the left Kan extension functor $\text{lan}_L$ and the precomposition functor $- \circ L$ at $G$ is given by the universal property of the left Kan extension. Specifically, the counit $(L.\text{lanAdjunction}\, H).\text{counit}.\text{app}\, G$ is equal to the morphism obtained from the left Kan extension property of $\text{lan}_L (L \circ G)$ applied to the identity natural transformation on $L \circ G$.

CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app theorem

(G : D ⥤ H) : L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Full source

@[reassoc (attr := simp)]
lemma lanUnit_app_whiskerLeft_lanAdjunction_counit_app (G : D ⥤ H) :
    L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G) := by
  simp [lanAdjunction_counit_app]

Compatibility of Left Kan Extension Unit and Counit via Whiskering

Informal description

For any functor $G \colon D \to H$, the composition of the left Kan extension unit $\text{lanUnit}_{L \circ G}$ with the left whiskering of the counit of the adjunction $(\text{lan}_L \dashv (- \circ L))$ at $G$ is equal to the identity natural transformation on $L \circ G$. In symbols: \[ \text{lanUnit}_{L \circ G} \circ (L \circ (\text{lan}_L \dashv (- \circ L)).\text{counit}_G) = \text{id}_{L \circ G} \]

CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app theorem

(G : D ⥤ H) (X : C) : (L.lanUnit.app (L ⋙ G)).app X ≫ ((L.lanAdjunction H).counit.app G).app (L.obj X) = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma lanUnit_app_app_lanAdjunction_counit_app_app (G : D ⥤ H) (X : C) :
    (L.lanUnit.app (L ⋙ G)).app X ≫ ((L.lanAdjunction H).counit.app G).app (L.obj X) = 𝟙 _ :=
  congr_app (L.lanUnit_app_whiskerLeft_lanAdjunction_counit_app G) X

Identity Relation for Left Kan Extension Unit and Counit Components

Informal description

For any functor $G \colon D \to H$ and any object $X$ in $C$, the composition of the component of the left Kan extension unit $\text{lanUnit}_{L \circ G}$ at $X$ with the component of the counit of the adjunction $(\text{lan}_L \dashv (- \circ L))$ at $G$ evaluated at $L(X)$ is equal to the identity morphism on $(L \circ G)(X)$. In symbols: \[ (\text{lanUnit}_{L \circ G})_X \circ ((\text{lan}_L \dashv (- \circ L)).\text{counit}_G)_{L(X)} = \text{id}_{(L \circ G)(X)} \]

CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff theorem

(G : D ⥤ H) : IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G))

Full source

lemma isIso_lanAdjunction_counit_app_iff (G : D ⥤ H) :
    IsIsoIsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G)) :=
  (isLeftKanExtension_iff_isIso _ (L.lanUnit.app (L ⋙ G)) _ (by simp)).symm

Isomorphism Criterion for Left Kan Extension via Adjunction Counit

Informal description

For any functor $G \colon D \to H$, the counit of the adjunction between the left Kan extension functor $\text{lan}_L$ and precomposition with $L$ is an isomorphism if and only if $G$ is a left Kan extension of $L \circ G$ along $L$ with the identity natural transformation $\text{id}_{L \circ G}$.

CategoryTheory.Functor.lanCompColimIso definition

[HasColimitsOfShape C H] [HasColimitsOfShape D H] : L.lan ⋙ colim ≅ colim (C := H)

Full source

/-- Composing the left Kan extension of `L : C ⥤ D` with `colim` on shapes `D` is isomorphic
to `colim` on shapes `C`. -/
@[simps!]
noncomputable def lanCompColimIso [HasColimitsOfShape C H] [HasColimitsOfShape D H] :
    L.lan ⋙ colimL.lan ⋙ colim ≅ colim (C := H) :=
  Iso.symm <| NatIso.ofComponents
    (fun G ↦ (colimitIsoOfIsLeftKanExtension _ (L.lanUnit.app G)).symm)
    (fun f ↦ colimit.hom_ext (fun i ↦ by
      dsimp
      rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc]
      congr 1
      exact congr_app (L.lanUnit.naturality f) i))

Isomorphism between $\text{lan}_L \circ \text{colim}$ and $\text{colim}$

Informal description

Given categories $C$, $D$, and $H$ where $H$ has all colimits of shapes $C$ and $D$, the composition of the left Kan extension functor $\text{lan}_L \colon (C \to H) \to (D \to H)$ with the colimit functor $\text{colim} \colon (D \to H) \to H$ is naturally isomorphic to the colimit functor $\text{colim} \colon (C \to H) \to H$. In other words, for any functor $G \colon C \to H$, the colimit of the left Kan extension $\text{lan}_L G$ is isomorphic to the colimit of $G$ itself. This isomorphism is natural in $G$.

CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj instance

: HasColimit (CostructuredArrow.grothendieckProj L ⋙ G)

Full source

instance : HasColimit (CostructuredArrow.grothendieckProjCostructuredArrow.grothendieckProj L ⋙ G) :=
  hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit _

Existence of Colimit for Composition with Grothendieck Projection

Informal description

For any functor $G \colon C \to H$, the composition of the projection functor $\mathrm{grothendieckProj}\, L$ from the Grothendieck construction of $L$-costructured arrows with $G$ has a colimit in $H$. Here: - $L \colon C \to D$ is a functor between categories - $\mathrm{grothendieckProj}\, L$ is the projection from $\int (\mathrm{functor}\, L)$ to $C$ - The Grothendieck construction $\int (\mathrm{functor}\, L)$ has objects $(d, (c, f))$ where $f \colon Lc \to d$ is a morphism in $D$

CategoryTheory.Functor.colimitIsoColimitGrothendieck definition

: colimit G ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G)

Full source

/-- If `G : C ⥤ H` admits a left Kan extension along a functor `L : C ⥤ D` and `H` has colimits of
shape `C` and `D`, then the colimit of `G` is isomorphic to the colimit of a canonical functor
`Grothendieck (CostructuredArrow.functor L) ⥤ H` induced by `L` and `G`. -/
noncomputable def colimitIsoColimitGrothendieck :
    colimitcolimit G ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G) := calc
  colimit G
    ≅ colimit (leftKanExtension L G) :=
        (colimitIsoOfIsLeftKanExtension _ (L.leftKanExtensionUnit G)).symm
  _ ≅ colimit (fiberwiseColimit (CostructuredArrow.grothendieckProj L ⋙ G))calc
  colimit G
    ≅ colimit (leftKanExtension L G) :=
        (colimitIsoOfIsLeftKanExtension _ (L.leftKanExtensionUnit G)).symm
  _ ≅ colimit (fiberwiseColimit (CostructuredArrow.grothendieckProj L ⋙ G)) :=
        HasColimit.isoOfNatIso (leftKanExtensionIsoFiberwiseColimit L G)
  _ ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G) :=
        colimitFiberwiseColimitIso _

Isomorphism between colimit of a functor and colimit via Grothendieck construction

Informal description

For a functor $ G \colon C \to H $ that has a colimit, the colimit of $ G $ is isomorphic to the colimit of the composition of the projection functor $ \text{grothendieckProj}\, L $ from the Grothendieck construction of $ L $-costructured arrows, followed by $ G $. Here: - $ L \colon C \to D $ is a functor between categories. - $ \text{grothendieckProj}\, L \colon \int (L.\text{functor}) \to C $ is the projection functor from the Grothendieck construction of $ L $-costructured arrows back to $ C $. - The Grothendieck construction $ \int (L.\text{functor}) $ has objects $ (d, (c, f)) $ where $ f \colon Lc \to d $ is a morphism in $ D $.

CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv theorem

 (X : Grothendieck (CostructuredArrow.functor L)) :
  colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (colimitIsoColimitGrothendieck L G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Full source

@[reassoc (attr := simp)]
lemma ι_colimitIsoColimitGrothendieck_inv (X : Grothendieck (CostructuredArrow.functor L)) :
    colimit.ιcolimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫
      (colimitIsoColimitGrothendieck L G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber) := by
  simp [colimitIsoColimitGrothendieck]

Compatibility of colimit coprojections with Grothendieck construction isomorphism

Informal description

For any object $X$ in the Grothendieck construction $\int \mathrm{CostructuredArrow}(L)$ (where $X$ consists of a pair $(d, (c, f))$ with $f : L(c) \to d$), the composition of the colimit coprojection $\iota_X$ for the functor $\mathrm{grothendieckProj}\, L \circ G$ with the inverse of the isomorphism $\mathrm{colimitIsoColimitGrothendieck}\, L\, G$ equals the colimit coprojection $\iota_{Y}$ for $G$ at the object $Y = \mathrm{proj}_L(d)(c,f) = c$.

CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom theorem

 (X : C) :
  colimit.ι G X ≫ (colimitIsoColimitGrothendieck L G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) ⟨L.obj X, .mk (𝟙 _)⟩

Full source

@[reassoc (attr := simp)]
lemma ι_colimitIsoColimitGrothendieck_hom (X : C) :
    colimit.ιcolimit.ι G X ≫ (colimitIsoColimitGrothendieck L G).hom =
    colimit.ι (CostructuredArrow.grothendieckProjCostructuredArrow.grothendieckProj L ⋙ G) ⟨L.obj X, .mk (𝟙 _)⟩ := by
  rw [← Iso.eq_comp_inv]
  exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

Compatibility of colimit coprojections with forward Grothendieck isomorphism

Informal description

For any object $X$ in category $C$, the composition of the colimit coprojection $\iota_X \colon G(X) \to \text{colimit } G$ with the forward isomorphism $\text{colimitIsoColimitGrothendieck}\, L\, G$ equals the colimit coprojection $\iota_Y$ for the functor $\text{grothendieckProj}\, L \circ G$ evaluated at the object $Y = (L(X), \text{mk}(1_{L(X)}))$ in the Grothendieck construction $\int \text{CostructuredArrow}(L)$. Here: - $L \colon C \to D$ is a functor between categories - $G \colon C \to H$ is a functor with a colimit - $\text{grothendieckProj}\, L$ is the projection from $\int (\text{functor}\, L)$ to $C$ - $\text{mk}(1_{L(X)})$ constructs a costructured arrow using the identity morphism on $L(X)$ - $\iota_X$ and $\iota_Y$ are the canonical coprojections to the respective colimits

CategoryTheory.Functor.instIsIsoAppLanUnit instance

 (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F] [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
  IsIso ((L.lanUnit.app F).app X)

Full source

instance (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F]
    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
    IsIso ((L.lanUnit.app F).app X) :=
  (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F (L.obj X)).isIso_hom_app

Isomorphism Property of Left Kan Extension Unit Components

Informal description

For any functor $F \colon C \to H$ and object $X \in C$, where $F$ has a pointwise left Kan extension along $L \colon C \to D$ and all functors from $C$ to $H$ have left Kan extensions along $L$, the component of the left Kan extension unit natural transformation at $F$ and $X$ is an isomorphism.

CategoryTheory.Functor.instIsIsoAppLanUnit_1 instance

(F : C ⥤ H) [HasPointwiseLeftKanExtension L F] [∀ (F : C ⥤ H), HasLeftKanExtension L F] : IsIso (L.lanUnit.app F)

Full source

instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F]
    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
    IsIso (L.lanUnit.app F) :=
  NatIso.isIso_of_isIso_app _

Isomorphism Property of the Left Kan Extension Unit Natural Transformation

Informal description

For any functor $F \colon C \to H$ that has a pointwise left Kan extension along $L \colon C \to D$, and assuming all functors from $C$ to $H$ have left Kan extensions along $L$, the natural transformation component $(L.\text{lanUnit}).F$ is an isomorphism.

CategoryTheory.Functor.coreflective instance

[∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] : IsIso (L.lanUnit (H := H))

Full source

instance coreflective [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] :
    IsIso (L.lanUnit (H := H)) := by
  apply NatIso.isIso_of_isIso_app _

Isomorphism of Left Kan Extension Unit under Pointwise Existence

Informal description

For any functor $L \colon C \to D$ and category $H$, if every functor $F \colon C \to H$ has a pointwise left Kan extension along $L$, then the left Kan extension unit natural transformation $L.\text{lanUnit}$ is an isomorphism.

CategoryTheory.Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension instance

 (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
  IsIso ((L.lanAdjunction H).unit.app F)

Full source

instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F]
    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
    IsIso ((L.lanAdjunction H).unit.app F) := by
  rw [lanAdjunction_unit]
  infer_instance

Isomorphism Property of the Left Kan Extension Adjunction Unit

Informal description

For any functor $F \colon C \to H$ that has a pointwise left Kan extension along $L \colon C \to D$, and assuming all functors from $C$ to $H$ have left Kan extensions along $L$, the component of the unit natural transformation of the adjunction $(L.\text{lan} \dashv (- \circ L))$ at $F$ is an isomorphism.

CategoryTheory.Functor.coreflective' instance

[∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] : IsIso (L.lanAdjunction H).unit

Full source

instance coreflective' [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] :
    IsIso (L.lanAdjunction H).unit := by
  apply NatIso.isIso_of_isIso_app _

Isomorphism of the Left Kan Extension Adjunction Unit under Pointwise Existence

Informal description

For any functor $L \colon C \to D$ and category $H$, if every functor $F \colon C \to H$ has a pointwise left Kan extension along $L$, then the unit natural transformation of the adjunction $(L.\text{lan} \dashv (- \circ L))$ is an isomorphism.

CategoryTheory.Functor.ran definition

: (C ⥤ H) ⥤ (D ⥤ H)

Full source

/-- The right Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`. -/
noncomputable def ran : (C ⥤ H) ⥤ (D ⥤ H) where
  obj F := rightKanExtension L F
  map {F₁ F₂} φ := liftOfIsRightKanExtension _ (rightKanExtensionCounit L F₂) _
    (rightKanExtensionCounit L F₁ ≫ φ)

Right Kan extension functor

Informal description

The right Kan extension functor along a functor $L \colon C \to D$ is a functor from the category of functors $C \to H$ to the category of functors $D \to H$. For a given functor $F \colon C \to H$, it sends $F$ to its right Kan extension along $L$.

CategoryTheory.Functor.ranCounit definition

: L.ran ⋙ (whiskeringLeft C D H).obj L ⟶ (𝟭 (C ⥤ H))

Full source

/-- The natural transformation `L ⋙ (L.lan).obj G ⟶ L`. -/
noncomputable def ranCounit : L.ran ⋙ (whiskeringLeft C D H).obj LL.ran ⋙ (whiskeringLeft C D H).obj L ⟶ (𝟭 (C ⥤ H)) where
  app F := rightKanExtensionCounit L F
  naturality {F₁ F₂} φ := by ext; simp [ran]

Counit of the right Kan extension functor

Informal description

The natural transformation from the composition of the right Kan extension functor along $L$ followed by precomposition with $L$ to the identity functor on the category of functors $C \to H$. For each functor $F \colon C \to H$, the component at $F$ is the counit of the right Kan extension of $F$ along $L$.

CategoryTheory.Functor.instIsRightKanExtensionObjRanAppRanCounit instance

(F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Full source

instance (F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F) := by
  dsimp [ran, ranCounit]
  infer_instance

Right Kan Extension Property of $L.\text{ran}(F)$

Informal description

For any functor $F \colon C \to H$, the right Kan extension of $F$ along $L$, denoted by $L.\text{ran}(F)$, is indeed a right Kan extension of $F$ along $L$, with the counit natural transformation $L.\text{ranCounit}(F)$ providing the universal property.

CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit definition

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] :
  (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension

Full source

/-- If there exists a pointwise right Kan extension of `F` along `L`,
then `L.ran.obj G` is a pointwise right Kan extension of `F`. -/
noncomputable def isPointwiseRightKanExtensionRanCounit
    (F : C ⥤ H) [HasPointwiseRightKanExtension L F] :
    (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension :=
  isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (L.ranCounit.app F)

Pointwise right Kan extension property of $L.\text{ran}(F)$

Informal description

Given a functor $F \colon C \to H$ and assuming that $F$ has a pointwise right Kan extension along $L \colon C \to D$, the right Kan extension of $F$ along $L$ equipped with the counit natural transformation $L.\text{ranCounit}(F)$ satisfies the universal property of a pointwise right Kan extension.

CategoryTheory.Functor.ranObjObjIsoLimit definition

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) : (L.ran.obj F).obj X ≅ limit (StructuredArrow.proj X L ⋙ F)

Full source

/-- If a right Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a limit. -/
noncomputable def ranObjObjIsoLimit (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) :
    (L.ran.obj F).obj X ≅ limit (StructuredArrow.proj X L ⋙ F) :=
  RightExtension.IsPointwiseRightKanExtensionAt.isoLimit (F := F)
    (isPointwiseRightKanExtensionRanCounit L F X)

Isomorphism between right Kan extension and limit of structured arrows

Informal description

For a functor $ F \colon C \to H $ that has a pointwise right Kan extension along $ L \colon C \to D $, and for any object $ X \colon D $, the object $ (L.\text{ran}(F))(X) $ is isomorphic to the limit of the composition $ \text{StructuredArrow.proj}\, X\, L \circ F $. Here, $ \text{StructuredArrow.proj}\, X\, L $ is the projection functor from the category of $ L $-structured arrows with domain $ X $ to $ C $.

CategoryTheory.Functor.ranObjObjIsoLimit_hom_π theorem

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
  (L.ranObjObjIsoLimit F X).hom ≫ limit.π _ f = (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right

Full source

@[reassoc (attr := simp)]
lemma ranObjObjIsoLimit_hom_π
    (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
    (L.ranObjObjIsoLimit F X).hom ≫ limit.π _ f =
    (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right := by
  simp [ranObjObjIsoLimit, ran, ranCounit]

Compatibility of right Kan extension isomorphism with limit projections via homomorphism

Informal description

For a functor $F \colon C \to H$ that has a pointwise right Kan extension along $L \colon C \to D$, and for any object $X \colon D$ and structured arrow $f \colon X \to L(Y)$ (where $Y \colon C$), the composition of the isomorphism $(L.\mathrm{ran}(F))(X) \cong \mathrm{limit}(F \circ \mathrm{StructuredArrow.proj}\, X\, L)$ with the limit projection $\pi_f \colon \mathrm{limit}(F \circ \mathrm{StructuredArrow.proj}\, X\, L) \to F(Y)$ equals the composition of the map $(L.\mathrm{ran}(F))(f) \colon (L.\mathrm{ran}(F))(X) \to (L.\mathrm{ran}(F))(Y)$ with the counit component $(L.\mathrm{ranCounit}(F))_Y \colon (L.\mathrm{ran}(F))(Y) \to F(Y)$.

CategoryTheory.Functor.ranObjObjIsoLimit_inv_π theorem

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
  (L.ranObjObjIsoLimit F X).inv ≫ (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right = limit.π _ f

Full source

@[reassoc (attr := simp)]
lemma ranObjObjIsoLimit_inv_π
    (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) (f : StructuredArrow X L) :
    (L.ranObjObjIsoLimit F X).inv ≫ (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right =
    limit.π _ f :=
  RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π (F := F)
    (isPointwiseRightKanExtensionRanCounit L F X) f

Compatibility of right Kan extension isomorphism with limit projections

Informal description

For a functor $F \colon C \to H$ that has a pointwise right Kan extension along $L \colon C \to D$, and for any object $X \colon D$ and structured arrow $f \colon X \to L(Y)$ (where $Y \colon C$), the composition of the inverse of the isomorphism $(L.\mathrm{ran}(F))(X) \cong \mathrm{limit}(F \circ \mathrm{StructuredArrow.proj}\, X\, L)$ with the map $(L.\mathrm{ran}(F))(f) \colon (L.\mathrm{ran}(F))(X) \to (L.\mathrm{ran}(F))(Y)$ followed by the counit component $(L.\mathrm{ranCounit}(F))_Y \colon (L.\mathrm{ran}(F))(Y) \to F(Y)$ equals the limit projection $\pi_f \colon \mathrm{limit}(F \circ \mathrm{StructuredArrow.proj}\, X\, L) \to F(Y)$.

CategoryTheory.Functor.ranAdjunction definition

: (whiskeringLeft C D H).obj L ⊣ L.ran

Full source

/-- The right Kan extension functor `L.ran` is right adjoint to the
precomposition by `L`. -/
noncomputable def ranAdjunction : (whiskeringLeft C D H).obj L ⊣ L.ran :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun F G =>
        (homEquivOfIsRightKanExtension (α := L.ranCounit.app G) _ F).symm
      homEquiv_naturality_right := fun {F G₁ G₂} β f ↦
        hom_ext_of_isRightKanExtension _ (L.ranCounit.app G₂) _ _ (by
        ext X
        dsimp [homEquivOfIsRightKanExtension]
        rw [liftOfIsRightKanExtension_fac_app, NatTrans.comp_app, assoc]
        have h := congr_app (L.ranCounit.naturality f) X
        dsimp at h ⊢
        rw [h, liftOfIsRightKanExtension_fac_app_assoc])
      homEquiv_naturality_left_symm := fun {F₁ F₂ G} β f ↦ by
        dsimp [homEquivOfIsRightKanExtension]
        rw [assoc] }

Adjunction between precomposition and right Kan extension

Informal description

The adjunction between the precomposition functor $(L \circ -) \colon (D \to H) \to (C \to H)$ and the right Kan extension functor $\text{ran}_L \colon (C \to H) \to (D \to H)$. This means that for any functors $F \colon C \to H$ and $G \colon D \to H$, there is a natural bijection $\text{Hom}(L \circ G, F) \cong \text{Hom}(G, \text{ran}_L(F))$.

CategoryTheory.Functor.ranAdjunction_counit theorem

: (L.ranAdjunction H).counit = L.ranCounit

Full source

@[simp]
lemma ranAdjunction_counit : (L.ranAdjunction H).counit = L.ranCounit := by
  ext F : 2
  dsimp [ranAdjunction, homEquivOfIsRightKanExtension]
  simp

Counit of the Right Kan Extension Adjunction Equals RanCounit

Informal description

The counit of the adjunction between the precomposition functor $(L \circ -) \colon (D \to H) \to (C \to H)$ and the right Kan extension functor $\text{ran}_L \colon (C \to H) \to (D \to H)$ is equal to the counit natural transformation of the right Kan extension functor.

CategoryTheory.Functor.ranAdjunction_unit_app theorem

 (G : D ⥤ H) :
  (L.ranAdjunction H).unit.app G = liftOfIsRightKanExtension (L.ran.obj (L ⋙ G)) (L.ranCounit.app (L ⋙ G)) G (𝟙 (L ⋙ G))

Full source

lemma ranAdjunction_unit_app (G : D ⥤ H) :
    (L.ranAdjunction H).unit.app G =
      liftOfIsRightKanExtension (L.ran.obj (L ⋙ G)) (L.ranCounit.app (L ⋙ G)) G (𝟙 (L ⋙ G)) :=
  rfl

Unit Component of Right Kan Extension Adjunction via Lift of Identity

Informal description

For any functor $G \colon D \to H$, the component of the unit of the adjunction $(L \circ -) \dashv \text{ran}_L$ at $G$ is equal to the lift of the identity natural transformation on $L \circ G$ through the right Kan extension property of $\text{ran}_L(L \circ G)$ with counit $\text{ran}_L.\text{counit}(L \circ G)$.

CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app theorem

(G : D ⥤ H) : whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Full source

@[reassoc (attr := simp)]
lemma ranCounit_app_whiskerLeft_ranAdjunction_unit_app (G : D ⥤ H) :
    whiskerLeftwhiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G) := by
  simp [ranAdjunction_unit_app]

Compatibility of Right Kan Extension Unit and Counit via Whiskering

Informal description

For any functor $G \colon D \to H$, the composition of the left whiskering of $L$ with the unit of the adjunction $(L.\text{ranAdjunction}\, H).\text{unit}$ applied to $G$, followed by the counit $L.\text{ranCounit}$ applied to $L \circ G$, equals the identity natural transformation on $L \circ G$. In symbols: \[ \text{whiskerLeft}\, L\, \left((L.\text{ranAdjunction}\, H).\text{unit}(G)\right) \circ L.\text{ranCounit}(L \circ G) = \text{id}_{L \circ G} \]

CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app theorem

(G : D ⥤ H) (X : C) : ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma ranCounit_app_app_ranAdjunction_unit_app_app (G : D ⥤ H) (X : C) :
    ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 𝟙 _ :=
  congr_app (L.ranCounit_app_whiskerLeft_ranAdjunction_unit_app G) X

Identity Relation between Right Kan Extension Unit and Counit Components

Informal description

For any functor $G \colon D \to H$ and any object $X$ in $C$, the composition of the component at $L(X)$ of the unit of the adjunction $(L.\text{ranAdjunction}\, H).\text{unit}(G)$ with the component at $X$ of the counit $L.\text{ranCounit}(L \circ G)$ equals the identity morphism on $(L \circ G)(X)$. In symbols: \[ \left((L.\text{ranAdjunction}\, H).\text{unit}(G)\right)_{L(X)} \circ \left(L.\text{ranCounit}(L \circ G)\right)_X = \text{id}_{(L \circ G)(X)} \]

CategoryTheory.Functor.isIso_ranAdjunction_unit_app_iff theorem

(G : D ⥤ H) : IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G))

Full source

lemma isIso_ranAdjunction_unit_app_iff (G : D ⥤ H) :
    IsIsoIsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G)) :=
  (isRightKanExtension_iff_isIso _ (L.ranCounit.app (L ⋙ G)) _ (by simp)).symm

Isomorphism Condition for Right Kan Extension Unit via Kan Extension Property

Informal description

For any functor $G \colon D \to H$, the unit natural transformation $(L.\text{ranAdjunction}\, H).\text{unit}(G)$ of the adjunction between precomposition with $L$ and the right Kan extension functor is an isomorphism if and only if $G$ is a right Kan extension of $L \circ G$ along $L$ with the identity natural transformation $\text{id}_{L \circ G}$. In symbols: \[ \text{IsIso}\left((L.\text{ranAdjunction}\, H).\text{unit}(G)\right) \leftrightarrow G \text{ is a right Kan extension of } L \circ G \text{ along } L \text{ via } \text{id}_{L \circ G} \]

CategoryTheory.Functor.ranCompLimIso definition

 (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasRightKanExtension G] [HasLimitsOfShape C H] [HasLimitsOfShape D H] :
  L.ran ⋙ lim ≅ lim (C := H)

Full source

/-- Composing the right Kan extension of `L : C ⥤ D` with `lim` on shapes `D` is isomorphic
to `lim` on shapes `C`. -/
@[simps!]
noncomputable def ranCompLimIso (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasRightKanExtension G]
    [HasLimitsOfShape C H] [HasLimitsOfShape D H] : L.ran ⋙ limL.ran ⋙ lim ≅ lim (C := H) :=
  NatIso.ofComponents
    (fun G ↦ limitIsoOfIsRightKanExtension _ (L.ranCounit.app G))
    (fun f ↦ limit.hom_ext (fun i ↦ by
      dsimp
      rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc,
        limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc]
      congr 1
      exact congr_app (L.ranCounit.naturality f) i))

Isomorphism between composition of right Kan extension and limit functors

Informal description

Given functors $L \colon C \to D$ and $G \colon C \to H$, where $H$ has limits of shapes $C$ and $D$, the composition of the right Kan extension functor $L.\text{ran}$ with the limit functor $\text{lim}$ is naturally isomorphic to the limit functor $\text{lim}$ applied directly to $G$. In other words, there is a natural isomorphism: \[ L.\text{ran} \circ \text{lim} \cong \text{lim} \] This isomorphism arises from the universal property of right Kan extensions and the compatibility of limits with Kan extensions.

CategoryTheory.Functor.instIsIsoAppRanCounit instance

 (F : C ⥤ H) (X : C) [HasPointwiseRightKanExtension L F] [∀ (F : C ⥤ H), HasRightKanExtension L F] :
  IsIso ((L.ranCounit.app F).app X)

Full source

instance (F : C ⥤ H) (X : C) [HasPointwiseRightKanExtension L F]
    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
    IsIso ((L.ranCounit.app F).app X) :=
  (isPointwiseRightKanExtensionRanCounit L F (L.obj X)).isIso_hom_app

Isomorphism Property of Right Kan Extension Counit Components

Informal description

For any functor $F \colon C \to H$ and object $X \in C$, if $F$ has a pointwise right Kan extension along $L \colon C \to D$ and every functor from $C$ to $H$ has a right Kan extension along $L$, then the component of the counit natural transformation of the right Kan extension at $X$ is an isomorphism.

CategoryTheory.Functor.instIsIsoAppRanCounit_1 instance

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] [∀ (F : C ⥤ H), HasRightKanExtension L F] : IsIso (L.ranCounit.app F)

Full source

instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F]
    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
    IsIso (L.ranCounit.app F) :=
  NatIso.isIso_of_isIso_app _

Isomorphism Property of the Right Kan Extension Counit

Informal description

For any functor $F \colon C \to H$, if $F$ has a pointwise right Kan extension along $L \colon C \to D$ and every functor from $C$ to $H$ has a right Kan extension along $L$, then the counit natural transformation of the right Kan extension at $F$ is an isomorphism.

CategoryTheory.Functor.reflective instance

[∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] : IsIso (L.ranCounit (H := H))

Full source

instance reflective [∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] :
    IsIso (L.ranCounit (H := H)) := by
  apply NatIso.isIso_of_isIso_app _

Isomorphism Property of the Right Kan Extension Counit for Pointwise Extensions

Informal description

For any functor $L \colon C \to D$ and category $H$, if every functor $F \colon C \to H$ has a pointwise right Kan extension along $L$, then the counit natural transformation of the right Kan extension functor is an isomorphism.

CategoryTheory.Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension instance

 (F : C ⥤ H) [HasPointwiseRightKanExtension L F] [∀ (F : C ⥤ H), HasRightKanExtension L F] :
  IsIso ((L.ranAdjunction H).counit.app F)

Full source

instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F]
    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
    IsIso ((L.ranAdjunction H).counit.app F) := by
  rw [ranAdjunction_counit]
  infer_instance

Isomorphism Property of the Right Kan Extension Adjunction Counit

Informal description

For any functor $F \colon C \to H$, if $F$ has a pointwise right Kan extension along $L \colon C \to D$ and every functor from $C$ to $H$ has a right Kan extension along $L$, then the counit of the adjunction between precomposition with $L$ and the right Kan extension functor at $F$ is an isomorphism.

CategoryTheory.Functor.reflective' instance

[∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] : IsIso (L.ranAdjunction H).counit

Full source

instance reflective' [∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] :
    IsIso (L.ranAdjunction H).counit := by
  apply NatIso.isIso_of_isIso_app _

Isomorphism of the Right Kan Extension Adjunction Counit for Pointwise Extensions

Informal description

For any functor $L \colon C \to D$ and category $H$, if every functor $F \colon C \to H$ has a pointwise right Kan extension along $L$, then the counit of the adjunction between precomposition with $L$ and the right Kan extension functor is an isomorphism.