Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt abbrev

(Y : D)

Full source

/-- The condition that a functor `F` has a pointwise left Kan extension along `L` at `Y`.
It means that the functor `CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H`
has a colimit. -/
abbrev HasPointwiseLeftKanExtensionAt (Y : D) :=
  HasColimit (CostructuredArrow.projCostructuredArrow.proj L Y ⋙ F)

Existence of Pointwise Left Kan Extension at an Object

Informal description

A functor $F \colon C \to H$ is said to have a pointwise left Kan extension along $L \colon C \to D$ at an object $Y \in D$ if the composite functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$ has a colimit. Here, $\text{CostructuredArrow}\, L\, Y$ is the category whose objects are morphisms $L(X) \to Y$ for $X \in C$ and morphisms are commutative triangles.

CategoryTheory.Functor.HasPointwiseLeftKanExtension abbrev

Full source

/-- The condition that a functor `F` has a pointwise left Kan extension along `L`: it means
that it has a pointwise left Kan extension at any object. -/
abbrev HasPointwiseLeftKanExtension := ∀ (Y : D), HasPointwiseLeftKanExtensionAt L F Y

Existence of Pointwise Left Kan Extension Along a Functor

Informal description

A functor $F \colon C \to H$ has a pointwise left Kan extension along a functor $L \colon C \to D$ if, for every object $Y \in D$, the composite functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$ has a colimit. Here, $\text{CostructuredArrow}\, L\, Y$ denotes the category whose objects are morphisms $L(X) \to Y$ for $X \in C$, with morphisms given by commutative triangles.

CategoryTheory.Functor.HasPointwiseRightKanExtensionAt abbrev

(Y : D)

Full source

/-- The condition that a functor `F` has a pointwise right Kan extension along `L` at `Y`.
It means that the functor `StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H`
has a limit. -/
abbrev HasPointwiseRightKanExtensionAt (Y : D) :=
  HasLimit (StructuredArrow.projStructuredArrow.proj Y L ⋙ F)

Existence of Pointwise Right Kan Extension at an Object

Informal description

A functor $F \colon C \to H$ has a pointwise right Kan extension along a functor $L \colon C \to D$ at an object $Y \colon D$ if the functor $\text{StructuredArrow.proj } Y L \circ F \colon \text{StructuredArrow } Y L \to H$ has a limit.

CategoryTheory.Functor.HasPointwiseRightKanExtension abbrev

Full source

/-- The condition that a functor `F` has a pointwise right Kan extension along `L`: it means
that it has a pointwise right Kan extension at any object. -/
abbrev HasPointwiseRightKanExtension := ∀ (Y : D), HasPointwiseRightKanExtensionAt L F Y

Existence of Pointwise Right Kan Extension

Informal description

A functor $F \colon C \to H$ has a pointwise right Kan extension along a functor $L \colon C \to D$ if, for every object $Y$ in $D$, the functor $\text{StructuredArrow.proj } Y L \circ F \colon \text{StructuredArrow } Y L \to H$ has a limit.

CategoryTheory.Functor.LeftExtension.coconeAt definition

(Y : D) : Cocone (CostructuredArrow.proj L Y ⋙ F)

Full source

/-- The cocone for `CostructuredArrow.proj L Y ⋙ F` attached to `E : LeftExtension L F`.
The point of this cocone is `E.right.obj Y` -/
@[simps]
def coconeAt (Y : D) : Cocone (CostructuredArrow.projCostructuredArrow.proj L Y ⋙ F) where
  pt := E.right.obj Y
  ι :=
    { app := fun g => E.hom.app g.left ≫ E.right.map g.hom
      naturality := fun g₁ g₂ φ => by
        dsimp
        rw [← CostructuredArrow.w φ]
        simp only [assoc, NatTrans.naturality_assoc, Functor.comp_map,
          Functor.map_comp, comp_id] }

Cocone for costructured arrows composition at $Y$ in a left extension

Informal description

Given a left extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$, and an object $Y \in D$, the cocone $\text{coconeAt}\, E\, Y$ is constructed with: - Cocone point: $E.\text{right}(Y)$ - Natural transformation components: For each object $g$ in the category of costructured arrows $\text{CostructuredArrow}\, L\, Y$, the component is given by $E.\text{hom}(g.\text{left}) \circ E.\text{right}.\text{map}(g.\text{hom})$, where $g.\text{left}$ is the source object in $C$ and $g.\text{hom}$ is the morphism in $D$ from $L(g.\text{left})$ to $Y$.

CategoryTheory.Functor.LeftExtension.coconeAtFunctor definition

(Y : D) : LeftExtension L F ⥤ Cocone (CostructuredArrow.proj L Y ⋙ F)

Full source

/-- The cocones for `CostructuredArrow.proj L Y ⋙ F`, as a functor from `LeftExtension L F`. -/
@[simps]
def coconeAtFunctor (Y : D) :
    LeftExtensionLeftExtension L F ⥤ Cocone (CostructuredArrow.proj L Y ⋙ F) where
  obj E := E.coconeAt Y
  map {E E'} φ := CoconeMorphism.mk (φ.right.app Y) (fun G => by
    dsimp
    rw [← StructuredArrow.w φ]
    simp)

Functor assigning cocones to left extensions at $Y$

Informal description

For a given object $Y$ in category $D$, the functor $\text{coconeAtFunctor}$ maps each left extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$ to the cocone $\text{coconeAt}\, E\, Y$ over the composition $\text{CostructuredArrow.proj}\, L\, Y \circ F$. For a morphism $\phi$ between left extensions $E$ and $E'$, the functor maps $\phi$ to a cocone morphism whose component at $Y$ is $\phi.\text{right}(Y)$, and whose naturality condition is given by the commutativity of the appropriate diagram.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt definition

(Y : D)

Full source

/-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension at `Y` when
`E.coconeAt Y` is a colimit cocone. -/
def IsPointwiseLeftKanExtensionAt (Y : D) := IsColimit (E.coconeAt Y)

Pointwise left Kan extension at an object $ Y $

Informal description

A left extension $ E $ of functors $ L \colon C \to D $ and $ F \colon C \to H $ is a *pointwise left Kan extension at $ Y \in D $* if the cocone $ \text{coconeAt}\, E\, Y $ is a colimit cocone for the functor $ \text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H $.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt theorem

{Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) : HasPointwiseLeftKanExtensionAt L F Y

Full source

lemma IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt
    {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) :
    HasPointwiseLeftKanExtensionAt L F Y := ⟨_, h⟩

Existence of Pointwise Left Kan Extension from Pointwise Kan Extension Condition

Informal description

Given a left extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$, if $E$ is a pointwise left Kan extension at an object $Y \in D$, then $F$ has a pointwise left Kan extension along $L$ at $Y$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app theorem

{X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : IsIso (E.hom.app X)

Full source

lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
    {X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
    IsIso (E.hom.app X) := by
  simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal

Isomorphism of Natural Transformation Component in Pointwise Left Kan Extension

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a left extension of $L$ along $F$. If $E$ is a pointwise left Kan extension at $L(X)$ for some object $X \in C$, and if $L$ is fully faithful, then the component of the natural transformation $E.\text{hom}$ at $X$ is an isomorphism.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit definition

: E.right.obj Y ≅ colimit (CostructuredArrow.proj L Y ⋙ F)

Full source

/-- A pointwise left Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
`colimit (CostructuredArrow.proj L Y ⋙ F)`. -/
noncomputable def isoColimit :
    E.right.obj Y ≅ colimit (CostructuredArrow.proj L Y ⋙ F) :=
  h.coconePointUniqueUpToIso (colimit.isColimit _)

Isomorphism between pointwise left Kan extension and colimit

Informal description

Given a left extension $ E $ of functors $ L \colon C \to D $ and $ F \colon C \to H $, and an object $ Y \in D $, if $ E $ is a pointwise left Kan extension at $ Y $, then there exists an isomorphism between $ E.\text{right}(Y) $ and the colimit of the functor $ \text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H $.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv theorem

(g : CostructuredArrow L Y) : colimit.ι _ g ≫ h.isoColimit.inv = E.hom.app g.left ≫ E.right.map g.hom

Full source

@[reassoc (attr := simp)]
lemma ι_isoColimit_inv (g : CostructuredArrow L Y) :
    colimit.ιcolimit.ι _ g ≫ h.isoColimit.inv = E.hom.app g.left ≫ E.right.map g.hom :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Compatibility of colimit coprojection with pointwise left Kan extension isomorphism

Informal description

For any object $g$ in the category of $L$-costructured arrows over $Y$, the composition of the colimit coprojection $\iota_g$ with the inverse of the isomorphism $\text{isoColimit}$ is equal to the composition of the natural transformation component $E.\text{hom}(g.\text{left})$ with the functorial image $E.\text{right}.\text{map}(g.\text{hom})$. In symbols: $$ \iota_g \circ \text{isoColimit}^{-1} = E.\text{hom}(g.\text{left}) \circ E.\text{right}.\text{map}(g.\text{hom}). $$

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom theorem

 (g : CostructuredArrow L Y) :
  E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom = colimit.ι (CostructuredArrow.proj L Y ⋙ F) g

Full source

@[reassoc (attr := simp)]
lemma ι_isoColimit_hom (g : CostructuredArrow L Y) :
    E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom =
      colimit.ι (CostructuredArrow.projCostructuredArrow.proj L Y ⋙ F) g := by
  simpa using h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g

Compatibility of Left Kan Extension with Colimit Coprojections

Informal description

Let $E$ be a left extension of functors $L \colon C \to D$ and $F \colon C \to H$, and let $Y \in D$. If $E$ is a pointwise left Kan extension at $Y$, then for any object $g$ in the category of costructured arrows $\mathrm{CostructuredArrow}\, L\, Y$, the composition $$ E.\mathrm{hom}(g.\mathrm{left}) \circ E.\mathrm{right}(g.\mathrm{hom}) \circ h.\mathrm{isoColimit}.\mathrm{hom} $$ equals the colimit coprojection $\mathrm{colimit}.\iota_g$ of the functor $\mathrm{CostructuredArrow.proj}\, L\, Y \circ F$ at $g$. Here: - $g.\mathrm{left}$ denotes the source object in $C$ of the costructured arrow $g \colon L(g.\mathrm{left}) \to Y$, - $g.\mathrm{hom}$ is the morphism $L(g.\mathrm{left}) \to Y$ in $D$, - $h.\mathrm{isoColimit}.\mathrm{hom}$ is the isomorphism $E.\mathrm{right}(Y) \cong \mathrm{colimit}(\mathrm{CostructuredArrow.proj}\, L\, Y \circ F)$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension abbrev

Full source

/-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension when
it is a pointwise left Kan extension at any object. -/
abbrev IsPointwiseLeftKanExtension := ∀ (Y : D), E.IsPointwiseLeftKanExtensionAt Y

Pointwise Left Kan Extension Condition for All Objects

Informal description

A left extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$ is called a *pointwise left Kan extension* if for every object $Y \in D$, the cocone $\text{coconeAt}\, E\, Y$ is a colimit cocone for the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso definition

(e : E ≅ E') (Y : D) : E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y

Full source

/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
left Kan extension at `Y` iff `E'` is. -/
def isPointwiseLeftKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
    E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y :=
  IsColimit.equivIsoColimit ((coconeAtFunctor L F Y).mapIso e)

Equivalence of pointwise left Kan extension properties under isomorphism of extensions

Informal description

Given an isomorphism $e \colon E \cong E'$ between two left extensions of functors $L \colon C \to D$ and $F \colon C \to H$, and an object $Y \in D$, there is an equivalence between the property of $E$ being a pointwise left Kan extension at $Y$ and the property of $E'$ being a pointwise left Kan extension at $Y$. This equivalence is obtained by transporting the colimit property along the isomorphism of cocones induced by $e$.

CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso definition

(e : E ≅ E') : E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension

Full source

/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
left Kan extension iff `E'` is. -/
def isPointwiseLeftKanExtensionEquivOfIso (e : E ≅ E') :
    E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension where
  toFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)
  invFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)
  left_inv h := by simp
  right_inv h := by simp

Equivalence of pointwise left Kan extension properties under isomorphism of extensions

Informal description

Given an isomorphism $e \colon E \cong E'$ between two left extensions of functors $L \colon C \to D$ and $F \colon C \to H$, there is an equivalence between the property of $E$ being a pointwise left Kan extension and the property of $E'$ being a pointwise left Kan extension. This equivalence is obtained by transporting the colimit property along the isomorphism of cocones induced by $e$ at each object $Y \in D$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension theorem

: HasPointwiseLeftKanExtension L F

Full source

lemma IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension :
    HasPointwiseLeftKanExtension L F :=
  fun Y => (h Y).hasPointwiseLeftKanExtensionAt

Existence of Pointwise Left Kan Extension from Pointwise Kan Extension Property

Informal description

If a left extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$ is a pointwise left Kan extension (i.e., for every object $Y \in D$, the cocone $\text{coconeAt}\, E\, Y$ is a colimit cocone for the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F$), then $F$ has a pointwise left Kan extension along $L$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom definition

(G : LeftExtension L F) : E ⟶ G

Full source

/-- The (unique) morphism from a pointwise left Kan extension. -/
def IsPointwiseLeftKanExtension.homFrom (G : LeftExtension L F) : E ⟶ G :=
  StructuredArrow.homMk
    { app := fun Y => (h Y).desc (LeftExtension.coconeAt G Y)
      naturality := fun Y₁ Y₂ φ => (h Y₁).hom_ext (fun X => by
        rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]
        simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)) }
    (by
      ext X
      simpa using (h (L.obj X)).fac (LeftExtension.coconeAt G _) (CostructuredArrow.mk (𝟙 _)))

Unique morphism from a pointwise left Kan extension to another left extension

Informal description

Given a pointwise left Kan extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$, and another left extension $G$ of the same functors, the morphism $\text{homFrom}\, G$ is the unique morphism from $E$ to $G$ in the category of left extensions. This morphism is constructed using the universal property of colimits, where for each object $Y \in D$, the component at $Y$ is the unique morphism induced by the colimit property of $E.\text{coconeAt}\, Y$ applied to $G.\text{coconeAt}\, Y$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hom_ext theorem

{G : LeftExtension L F} {f₁ f₂ : E ⟶ G} : f₁ = f₂

Full source

lemma IsPointwiseLeftKanExtension.hom_ext
    {G : LeftExtension L F} {f₁ f₂ : E ⟶ G} : f₁ = f₂ := by
  ext Y
  apply (h Y).hom_ext
  intro X
  have eq₁ := congr_app (StructuredArrow.w f₁) X.left
  have eq₂ := congr_app (StructuredArrow.w f₂) X.left
  dsimp at eq₁ eq₂ ⊢
  simp only [assoc, NatTrans.naturality]
  rw [reassoc_of% eq₁, reassoc_of% eq₂]

Extensionality of Morphisms in the Category of Left Extensions

Informal description

For any two morphisms $f_1, f_2 \colon E \to G$ in the category of left extensions of $L$ and $F$, if their underlying natural transformations are equal, then $f_1 = f_2$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isUniversal definition

: E.IsUniversal

Full source

/-- A pointwise left Kan extension is universal, i.e. it is a left Kan extension. -/
def IsPointwiseLeftKanExtension.isUniversal : E.IsUniversal :=
  IsInitial.ofUniqueHom h.homFrom (fun _ _ => h.hom_ext)

Universal property of pointwise left Kan extension

Informal description

A pointwise left Kan extension $E$ of functors $L \colon C \to D$ and $F \colon C \to H$ satisfies the universal property of being initial in the category of left extensions. Specifically, for any other left extension $G$, there exists a unique morphism from $E$ to $G$, and any two such morphisms are equal.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension theorem

: E.right.IsLeftKanExtension E.hom

Full source

lemma IsPointwiseLeftKanExtension.isLeftKanExtension :
    E.right.IsLeftKanExtension E.hom where
  nonempty_isUniversal := ⟨h.isUniversal⟩

Pointwise Left Kan Extension Implies Left Kan Extension

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a left extension of $F$ along $L$. If $E$ is a pointwise left Kan extension, then the functor $E.\text{right} \colon D \to H$ together with the natural transformation $E.\text{hom} \colon F \to L \circ E.\text{right}$ forms a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasLeftKanExtension theorem

: HasLeftKanExtension L F

Full source

lemma IsPointwiseLeftKanExtension.hasLeftKanExtension :
    HasLeftKanExtension L F :=
  have := h.isLeftKanExtension
  HasLeftKanExtension.mk E.right E.hom

Existence of Left Kan Extension from Pointwise Left Kan Extension Condition

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, if a left extension $E$ of $F$ along $L$ is a pointwise left Kan extension, then there exists a left Kan extension of $F$ along $L$.

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom theorem

[L.Full] [L.Faithful] : IsIso (E.hom)

Full source

lemma IsPointwiseLeftKanExtension.isIso_hom [L.Full] [L.Faithful] :
    IsIso (E.hom) :=
  have := fun X => (h (L.obj X)).isIso_hom_app
  NatIso.isIso_of_isIso_app ..

Natural Transformation in Pointwise Left Kan Extension is Isomorphism when $L$ is Fully Faithful

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a left extension of $L$ along $F$. If $E$ is a pointwise left Kan extension and $L$ is fully faithful, then the natural transformation $E.\text{hom} \colon F \to L \circ E.\text{right}$ is an isomorphism.

CategoryTheory.Functor.RightExtension.coneAt definition

(Y : D) : Cone (StructuredArrow.proj Y L ⋙ F)

Full source

/-- The cone for `StructuredArrow.proj Y L ⋙ F` attached to `E : RightExtension L F`.
The point of this cone is `E.left.obj Y` -/
@[simps]
def coneAt (Y : D) : Cone (StructuredArrow.projStructuredArrow.proj Y L ⋙ F) where
  pt := E.left.obj Y
  π :=
    { app := fun g ↦ E.left.map g.hom ≫ E.hom.app g.right
      naturality := fun g₁ g₂ φ ↦ by
        dsimp
        rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]
        congr 1
        apply E.hom.naturality }

Cone for the right extension at an object $Y$

Informal description

Given a right extension $E$ of a functor $F$ along a functor $L$, and an object $Y$ in the target category $D$, the cone $\text{coneAt}\, Y$ is constructed over the functor $\text{StructuredArrow.proj}\, Y\, L \circ F$. The cone point is $E.\text{left}(Y)$, and the natural transformation components are given by mapping each structured arrow $g$ to the composition $E.\text{left}(g.\text{hom}) \circ E.\text{hom}(g.\text{right})$.

CategoryTheory.Functor.RightExtension.coneAtFunctor definition

(Y : D) : RightExtension L F ⥤ Cone (StructuredArrow.proj Y L ⋙ F)

Full source

/-- The cones for `StructuredArrow.proj Y L ⋙ F`, as a functor from `RightExtension L F`. -/
@[simps]
def coneAtFunctor (Y : D) :
    RightExtensionRightExtension L F ⥤ Cone (StructuredArrow.proj Y L ⋙ F) where
  obj E := E.coneAt Y
  map {E E'} φ := ConeMorphism.mk (φ.left.app Y) (fun G ↦ by
    dsimp
    rw [← CostructuredArrow.w φ]
    simp)

Functor assigning cones to right extensions at an object $Y$

Informal description

For a given object $Y$ in category $D$, the functor $\text{coneAtFunctor}\, Y$ maps each right extension $E$ of $F$ along $L$ to the cone $E.\text{coneAt}\, Y$ over the functor $\text{StructuredArrow.proj}\, Y\, L \circ F$. For a morphism $\phi$ between right extensions $E$ and $E'$, the functor maps $\phi$ to the cone morphism whose component at $Y$ is $\phi.\text{left}(Y)$ and whose naturality condition is given by the commutativity of the appropriate diagram.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt definition

(Y : D)

Full source

/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension at `Y` when
`E.coneAt Y` is a limit cone. -/
def IsPointwiseRightKanExtensionAt (Y : D) := IsLimit (E.coneAt Y)

Pointwise right Kan extension at an object $ Y $

Informal description

A right extension $ E $ of a functor $ F $ along a functor $ L $ is called a *pointwise right Kan extension at $ Y $* if the cone $ E.\text{coneAt}\, Y $ is a limit cone for the functor $ \text{StructuredArrow.proj}\, Y\, L \circ F $.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt theorem

{Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) : HasPointwiseRightKanExtensionAt L F Y

Full source

lemma IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt
    {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) :
    HasPointwiseRightKanExtensionAt L F Y := ⟨_, h⟩

Existence of Pointwise Right Kan Extension at an Object from Pointwise Right Kan Extension Condition

Informal description

Given a right extension $E$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, if $E$ is a pointwise right Kan extension at an object $Y \colon D$, then $F$ has a pointwise right Kan extension along $L$ at $Y$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app theorem

{X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : IsIso (E.hom.app X)

Full source

lemma IsPointwiseRightKanExtensionAt.isIso_hom_app
    {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
    IsIso (E.hom.app X) := by
  simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial

Isomorphism of natural transformation components in pointwise right Kan extensions under fully faithful functors

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a right extension of $F$ along $L$. For any object $X \in C$, if $E$ is a pointwise right Kan extension at $L(X)$, and $L$ is fully faithful, then the component $E.\text{hom}_X$ of the natural transformation $E.\text{hom}$ at $X$ is an isomorphism.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit definition

: E.left.obj Y ≅ limit (StructuredArrow.proj Y L ⋙ F)

Full source

/-- A pointwise right Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
`limit (StructuredArrow.proj Y L ⋙ F)`. -/
noncomputable def isoLimit :
    E.left.obj Y ≅ limit (StructuredArrow.proj Y L ⋙ F) :=
  h.conePointUniqueUpToIso (limit.isLimit _)

Isomorphism between pointwise right Kan extension and limit

Informal description

Given a right extension $ E $ of a functor $ F \colon C \to H $ along a functor $ L \colon C \to D $, if $ E $ is a pointwise right Kan extension at an object $ Y \in D $, then the object $ E.\text{left}(Y) $ is isomorphic to the limit of the functor $ \text{StructuredArrow.proj}\, Y\, L \circ F \colon \text{StructuredArrow}\, Y\, L \to H $.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π theorem

(g : StructuredArrow Y L) : h.isoLimit.hom ≫ limit.π _ g = E.left.map g.hom ≫ E.hom.app g.right

Full source

@[reassoc (attr := simp)]
lemma isoLimit_hom_π (g : StructuredArrow Y L) :
    h.isoLimit.hom ≫ limit.π _ g = E.left.map g.hom ≫ E.hom.app g.right :=
  IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Compatibility of Kan Extension Isomorphism with Limit Projections

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a right extension of $F$ along $L$. For an object $Y \in D$, suppose $E$ is a pointwise right Kan extension at $Y$, with isomorphism $\varphi \colon E.\text{left}(Y) \to \text{limit}\, (\text{StructuredArrow.proj}\, Y\, L \circ F)$. Then for any structured arrow $g \colon Y \to L(X)$ (where $X \in C$), the composition $\varphi \circ \pi_g$ equals $E.\text{left}(g) \circ E.\text{hom}_X$, where $\pi_g$ is the limit projection corresponding to $g$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π theorem

 (g : StructuredArrow Y L) :
  h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right = limit.π (StructuredArrow.proj Y L ⋙ F) g

Full source

@[reassoc (attr := simp)]
lemma isoLimit_inv_π (g : StructuredArrow Y L) :
    h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right =
      limit.π (StructuredArrow.projStructuredArrow.proj Y L ⋙ F) g := by
  simpa using h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

Compatibility of Inverse Isomorphism with Limit Projections in Pointwise Right Kan Extensions

Informal description

For a right extension $E$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, if $E$ is a pointwise right Kan extension at an object $Y \in D$, then for any structured arrow $g \colon Y \to L(X)$ (where $X \in C$), the composition of the inverse isomorphism $h.\text{isoLimit}^{-1} \colon \text{limit}(\text{StructuredArrow.proj}\, Y\, L \circ F) \to E.\text{left}(Y)$ with the morphism $E.\text{left}(g.\text{hom}) \circ E.\text{hom}(X)$ equals the limit projection $\pi_g \colon \text{limit}(\text{StructuredArrow.proj}\, Y\, L \circ F) \to F(X)$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension abbrev

Full source

/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension when
it is a pointwise right Kan extension at any object. -/
abbrev IsPointwiseRightKanExtension := ∀ (Y : D), E.IsPointwiseRightKanExtensionAt Y

Pointwise Right Kan Extension Condition

Informal description

A right extension $E$ of a functor $F$ along a functor $L$ is called a *pointwise right Kan extension* if for every object $Y$ in the target category, the cone $E.\text{coneAt}\, Y$ is a limit cone for the functor $\text{StructuredArrow.proj}\, Y\, L \circ F$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso definition

(e : E ≅ E') (Y : D) : E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y

Full source

/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
right Kan extension at `Y` iff `E'` is. -/
def isPointwiseRightKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
    E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y :=
  IsLimit.equivIsoLimit ((coneAtFunctor L F Y).mapIso e)

Equivalence of pointwise right Kan extension conditions under isomorphism of extensions

Informal description

Given an isomorphism $e \colon E \cong E'$ between two right extensions of a functor $F$ along a functor $L$, and an object $Y$ in the target category $D$, there is an equivalence between the statements that $E$ is a pointwise right Kan extension at $Y$ and that $E'$ is a pointwise right Kan extension at $Y$. This equivalence is constructed by transporting the limit cone property along the isomorphism $e$ via the functor that assigns cones to right extensions at $Y$.

CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfIso definition

(e : E ≅ E') : E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension

Full source

/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
right Kan extension iff `E'` is. -/
def isPointwiseRightKanExtensionEquivOfIso (e : E ≅ E') :
    E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension where
  toFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)
  invFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)
  left_inv h := by simp
  right_inv h := by simp

Equivalence of pointwise right Kan extension conditions under isomorphism of extensions

Informal description

Given an isomorphism $e \colon E \cong E'$ between two right extensions of a functor $F$ along a functor $L$, there is an equivalence between the statements that $E$ is a pointwise right Kan extension and that $E'$ is a pointwise right Kan extension. This equivalence is constructed by transporting the limit cone property along the isomorphism $e$ for every object in the target category.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension theorem

: HasPointwiseRightKanExtension L F

Full source

lemma IsPointwiseRightKanExtension.hasPointwiseRightKanExtension :
    HasPointwiseRightKanExtension L F :=
  fun Y => (h Y).hasPointwiseRightKanExtensionAt

Existence of Pointwise Right Kan Extension from Pointwise Right Kan Extension Condition

Informal description

If a right extension $E$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$ is a pointwise right Kan extension (i.e., for every object $Y$ in $D$, the cone $E.\text{coneAt}\, Y$ is a limit cone for the functor $\text{StructuredArrow.proj}\, Y\, L \circ F$), then $F$ has a pointwise right Kan extension along $L$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.homTo definition

(G : RightExtension L F) : G ⟶ E

Full source

/-- The (unique) morphism to a pointwise right Kan extension. -/
def IsPointwiseRightKanExtension.homTo (G : RightExtension L F) : G ⟶ E :=
  CostructuredArrow.homMk
    { app := fun Y ↦ (h Y).lift (RightExtension.coneAt G Y)
      naturality := fun Y₁ Y₂ φ ↦ (h Y₂).hom_ext (fun X ↦ by
        rw [assoc, (h Y₂).fac (coneAt G Y₂) X]
        simpa using ((h Y₁).fac (coneAt G Y₁) ((StructuredArrow.map φ).obj X)).symm) }
    (by
      ext X
      simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _)) )

Unique morphism to a pointwise right Kan extension

Informal description

Given a right extension $E$ of a functor $F$ along a functor $L$, and another right extension $G$ of $F$ along $L$, the morphism $\text{homTo}\, G$ is the unique morphism from $G$ to $E$ in the category of right extensions. This morphism is constructed using the universal property of $E$ as a pointwise right Kan extension, ensuring compatibility with the natural transformations involved.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hom_ext theorem

{G : RightExtension L F} {f₁ f₂ : G ⟶ E} : f₁ = f₂

Full source

lemma IsPointwiseRightKanExtension.hom_ext
    {G : RightExtension L F} {f₁ f₂ : G ⟶ E} : f₁ = f₂ := by
  ext Y
  apply (h Y).hom_ext
  intro X
  have eq₁ := congr_app (CostructuredArrow.w f₁) X.right
  have eq₂ := congr_app (CostructuredArrow.w f₂) X.right
  dsimp at eq₁ eq₂ ⊢
  simp only [assoc, ← NatTrans.naturality_assoc, eq₁, eq₂]

Uniqueness of Morphisms Between Right Extensions via Natural Transformation Equality

Informal description

For any two morphisms $f_1, f_2 \colon G \to E$ in the category of right extensions of $F$ along $L$, if $f_1$ and $f_2$ are equal as natural transformations, then $f_1 = f_2$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isUniversal definition

: E.IsUniversal

Full source

/-- A pointwise right Kan extension is universal, i.e. it is a right Kan extension. -/
def IsPointwiseRightKanExtension.isUniversal : E.IsUniversal :=
  IsTerminal.ofUniqueHom h.homTo (fun _ _ => h.hom_ext)

Universality of pointwise right Kan extension

Informal description

A pointwise right Kan extension $E$ of a functor $F$ along a functor $L$ is universal, meaning it satisfies the universal property of being terminal in the category of right extensions of $F$ along $L$. Specifically, for any other right extension $G$, there exists a unique morphism from $G$ to $E$ in this category.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension theorem

: E.left.IsRightKanExtension E.hom

Full source

lemma IsPointwiseRightKanExtension.isRightKanExtension :
    E.left.IsRightKanExtension E.hom where
  nonempty_isUniversal := ⟨h.isUniversal⟩

Pointwise Right Kan Extension Implies Right Kan Extension

Informal description

Given a right extension $E$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$, if $E$ is a pointwise right Kan extension, then the functor $E.\text{left}$ together with the natural transformation $E.\text{hom}$ forms a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension theorem

: HasRightKanExtension L F

Full source

lemma IsPointwiseRightKanExtension.hasRightKanExtension :
    HasRightKanExtension L F :=
  have := h.isRightKanExtension
  HasRightKanExtension.mk E.left E.hom

Existence of Right Kan Extension from Pointwise Condition

Informal description

If a right extension $E$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$ is a pointwise right Kan extension, then there exists a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isIso_hom theorem

[L.Full] [L.Faithful] : IsIso (E.hom)

Full source

lemma IsPointwiseRightKanExtension.isIso_hom [L.Full] [L.Faithful] :
    IsIso (E.hom) :=
  have := fun X => (h (L.obj X)).isIso_hom_app
  NatIso.isIso_of_isIso_app ..

Natural Transformation Isomorphism in Pointwise Right Kan Extensions via Fully Faithful Functors

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $E$ be a right extension of $F$ along $L$. If $E$ is a pointwise right Kan extension and $L$ is fully faithful, then the natural transformation $E.\text{hom}$ is an isomorphism.

CategoryTheory.Functor.pointwiseLeftKanExtension definition

: D ⥤ H

Full source

/-- The constructed pointwise left Kan extension when `HasPointwiseLeftKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseLeftKanExtension : D ⥤ H where
  obj Y := colimit (CostructuredArrow.projCostructuredArrow.proj L Y ⋙ F)
  map {Y₁ Y₂} f :=
    colimit.desc (CostructuredArrow.projCostructuredArrow.proj L Y₁ ⋙ F)
      (Cocone.mk (colimit (CostructuredArrow.projCostructuredArrow.proj L Y₂ ⋙ F))
        { app := fun g => colimit.ι (CostructuredArrow.projCostructuredArrow.proj L Y₂ ⋙ F)
            ((CostructuredArrow.map f).obj g)
          naturality := fun g₁ g₂ φ => by
            simpa using colimit.w (CostructuredArrow.projCostructuredArrow.proj L Y₂ ⋙ F)
              ((CostructuredArrow.map f).map φ) })
  map_id Y := colimit.hom_ext (fun j => by
    dsimp
    simp only [colimit.ι_desc, comp_id]
    congr
    apply CostructuredArrow.map_id)
  map_comp {Y₁ Y₂ Y₃} f f' := colimit.hom_ext (fun j => by
    dsimp
    simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]
    congr 1
    apply CostructuredArrow.map_comp)

Pointwise Left Kan Extension Functor

Informal description

The functor `pointwiseLeftKanExtension L F : D ⥤ H` is constructed as the pointwise left Kan extension of a functor $F : C \to H$ along a functor $L : C \to D$. For each object $Y$ in $D$, the value of the functor at $Y$ is given by the colimit of the composite functor $\text{CostructuredArrow.proj}\, L\, Y \circ F : \text{CostructuredArrow}\, L\, Y \to H$. The morphism part of the functor is defined using the universal property of colimits, ensuring functoriality.

CategoryTheory.Functor.pointwiseLeftKanExtensionUnit definition

: F ⟶ L ⋙ pointwiseLeftKanExtension L F

Full source

/-- The unit of the constructed pointwise left Kan extension when
`HasPointwiseLeftKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseLeftKanExtensionUnit : F ⟶ L ⋙ pointwiseLeftKanExtension L F where
  app X := colimit.ι (CostructuredArrow.projCostructuredArrow.proj L (L.obj X) ⋙ F)
    (CostructuredArrow.mk (𝟙 (L.obj X)))
  naturality {X₁ X₂} f := by
    simp only [comp_obj, pointwiseLeftKanExtension_obj, comp_map,
      pointwiseLeftKanExtension_map, colimit.ι_desc, CostructuredArrow.map_mk]
    rw [id_comp]
    let φ : CostructuredArrow.mkCostructuredArrow.mk (L.map f) ⟶ CostructuredArrow.mk (𝟙 (L.obj X₂)) :=
      CostructuredArrow.homMk f
    exact colimit.w (CostructuredArrow.projCostructuredArrow.proj L (L.obj X₂) ⋙ F) φ

Unit of the pointwise left Kan extension

Informal description

The natural transformation $\eta \colon F \Rightarrow L \circ \text{pointwiseLeftKanExtension}\, L\, F$ is the unit of the pointwise left Kan extension of $F$ along $L$. For each object $X$ in $C$, the component $\eta_X \colon F(X) \to \text{pointwiseLeftKanExtension}\, L\, F (L(X))$ is given by the coprojection $\iota_{\text{mk}\, \text{id}_{L(X)}}$ from $F(X)$ to the colimit of the functor $\text{CostructuredArrow.proj}\, L\, (L(X)) \circ F \colon \text{CostructuredArrow}\, L\, (L(X)) \to H$, where $\text{mk}\, \text{id}_{L(X)}$ denotes the object in $\text{CostructuredArrow}\, L\, (L(X))$ consisting of the identity morphism $\text{id}_{L(X)} \colon L(X) \to L(X)$. The naturality of $\eta$ follows from the universal property of colimits.

CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension definition

: (LeftExtension.mk _ (pointwiseLeftKanExtensionUnit L F)).IsPointwiseLeftKanExtension

Full source

/-- The functor `pointwiseLeftKanExtension L F` is a pointwise left Kan
extension of `F` along `L`. -/
noncomputable def pointwiseLeftKanExtensionIsPointwiseLeftKanExtension :
    (LeftExtension.mk _ (pointwiseLeftKanExtensionUnit L F)).IsPointwiseLeftKanExtension :=
  fun X => IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Iso.refl _) (fun j => by
    dsimp
    simp only [comp_id, colimit.ι_desc, CostructuredArrow.map_mk]
    congr 1
    rw [id_comp, ← CostructuredArrow.eq_mk]))

Pointwise left Kan extension property

Informal description

The left extension formed by the functor `pointwiseLeftKanExtension L F` and the natural transformation `pointwiseLeftKanExtensionUnit L F` is a pointwise left Kan extension. This means that for every object $Y$ in $D$, the cocone at $Y$ is a colimit cocone for the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$.

CategoryTheory.Functor.pointwiseLeftKanExtensionIsUniversal definition

: (LeftExtension.mk _ (pointwiseLeftKanExtensionUnit L F)).IsUniversal

Full source

/-- The functor `pointwiseLeftKanExtension L F` is a left Kan extension of `F` along `L`. -/
noncomputable def pointwiseLeftKanExtensionIsUniversal :
    (LeftExtension.mk _ (pointwiseLeftKanExtensionUnit L F)).IsUniversal :=
  (pointwiseLeftKanExtensionIsPointwiseLeftKanExtension L F).isUniversal

Universal property of the pointwise left Kan extension

Informal description

The left extension formed by the functor $\text{pointwiseLeftKanExtension}\, L\, F$ and the natural transformation $\text{pointwiseLeftKanExtensionUnit}\, L\, F$ satisfies the universal property of being initial in the category of left extensions of $F$ along $L$. This means that for any other left extension $G$, there exists a unique morphism from this extension to $G$.

CategoryTheory.Functor.instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit instance

: (pointwiseLeftKanExtension L F).IsLeftKanExtension (pointwiseLeftKanExtensionUnit L F)

Full source

instance : (pointwiseLeftKanExtension L F).IsLeftKanExtension
    (pointwiseLeftKanExtensionUnit L F) where
  nonempty_isUniversal := ⟨pointwiseLeftKanExtensionIsUniversal L F⟩

Pointwise Left Kan Extension Property

Informal description

The functor $\text{pointwiseLeftKanExtension}\, L\, F$, equipped with the natural transformation $\text{pointwiseLeftKanExtensionUnit}\, L\, F$, forms a left Kan extension of $F$ along $L$. This means that for every object $Y$ in $D$, the cocone at $Y$ is a colimit cocone for the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$.

CategoryTheory.Functor.instHasLeftKanExtension instance

: HasLeftKanExtension L F

Full source

instance : HasLeftKanExtension L F :=
  HasLeftKanExtension.mk _ (pointwiseLeftKanExtensionUnit L F)

Existence of Left Kan Extension

Informal description

For any functors $L \colon C \to D$ and $F \colon C \to H$, there exists a left Kan extension of $F$ along $L$. This means there is 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.costructuredArrowMapCocone definition

(G : D ⥤ H) (α : F ⟶ L ⋙ G) (Y : D) : Cocone (CostructuredArrow.proj L Y ⋙ F)

Full source

/-- An auxiliary cocone used in the lemma `pointwiseLeftKanExtension_desc_app` -/
@[simps]
def costructuredArrowMapCocone (G : D ⥤ H) (α : F ⟶ L ⋙ G) (Y : D) :
    Cocone (CostructuredArrow.projCostructuredArrow.proj L Y ⋙ F) where
  pt := G.obj Y
  ι := {
    app := fun f ↦ α.app f.left ≫ G.map f.hom
    naturality := by simp [← G.map_comp] }

Cocone induced by natural transformation on costructured arrows

Informal description

Given functors $L : C \to D$, $F : C \to H$, and $G : D \to H$, along with a natural transformation $\alpha : F \Rightarrow L \circ G$ and an object $Y \in D$, the cocone `costructuredArrowMapCocone L F G α Y` has as its cocone point $G(Y)$ and its natural transformation components given by $\alpha_X \circ G(f)$ for each object $(f : L(X) \to Y)$ in the costructured arrow category $\mathrm{CostructuredArrow}(L, Y)$.

CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app theorem

 (G : D ⥤ H) (α : F ⟶ L ⋙ G) (Y : D) :
  ((pointwiseLeftKanExtension L F).descOfIsLeftKanExtension (pointwiseLeftKanExtensionUnit L F) G α |>.app Y) =
    colimit.desc _ (costructuredArrowMapCocone L F G α Y)

Full source

@[simp]
lemma pointwiseLeftKanExtension_desc_app (G : D ⥤ H) (α :  F ⟶ L ⋙ G) (Y : D) :
    ((pointwiseLeftKanExtension L F).descOfIsLeftKanExtension (pointwiseLeftKanExtensionUnit L F)
      G α |>.app Y) = colimit.desc _ (costructuredArrowMapCocone L F G α Y) := by
  let β : L.pointwiseLeftKanExtension F ⟶ G :=
    { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }
  have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
      (pointwiseLeftKanExtensionUnit L F) G α = β := by
    apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
    aesop
  exact NatTrans.congr_app h Y

Universal Property of Pointwise Left Kan Extension at Component Level: $\text{desc}_Y = \text{colimit.desc}\, \mathcal{C}_Y$

Informal description

Let $L \colon C \to D$ and $F \colon C \to H$ be functors, and let $\text{pointwiseLeftKanExtension}\, L\, F \colon D \to H$ be the pointwise left Kan extension of $F$ along $L$ with unit natural transformation $\eta \colon F \Rightarrow L \circ \text{pointwiseLeftKanExtension}\, L\, F$. For any functor $G \colon D \to H$ and natural transformation $\alpha \colon F \Rightarrow L \circ G$, the component at $Y \in D$ of the induced morphism $\text{descOfIsLeftKanExtension}\, \eta\, G\, \alpha \colon \text{pointwiseLeftKanExtension}\, L\, F \to G$ is equal to the universal morphism $\text{colimit.desc}$ applied to the cocone $\text{costructuredArrowMapCocone}\, L\, F\, G\, \alpha\, Y$ over the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F$.

CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension definition

(F' : D ⥤ H) (α : F ⟶ L ⋙ F') [F'.IsLeftKanExtension α] : (LeftExtension.mk _ α).IsPointwiseLeftKanExtension

Full source

/-- If `F` admits a pointwise left Kan extension along `L`, then any left Kan extension of `F`
along `L` is a pointwise left Kan extension. -/
noncomputable def isPointwiseLeftKanExtensionOfIsLeftKanExtension (F' : D ⥤ H) (α : F ⟶ L ⋙ F')
    [F'.IsLeftKanExtension α] :
    (LeftExtension.mk _ α).IsPointwiseLeftKanExtension :=
  LeftExtension.isPointwiseLeftKanExtensionEquivOfIso
    (IsColimit.coconePointUniqueUpToIso (pointwiseLeftKanExtensionIsUniversal L F)
      (F'.isUniversalOfIsLeftKanExtension α))
    (pointwiseLeftKanExtensionIsPointwiseLeftKanExtension L F)

Pointwise left Kan extension property from left Kan extension

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, if a functor $F' \colon D \to H$ equipped with a natural transformation $\alpha \colon F \Rightarrow L \circ F'$ is a left Kan extension of $F$ along $L$, then the left extension $(F', \alpha)$ is a pointwise left Kan extension. This means that for every object $Y \in D$, the cocone at $Y$ is a colimit cocone for the functor $\text{CostructuredArrow.proj}\, L\, Y \circ F \colon \text{CostructuredArrow}\, L\, Y \to H$.

CategoryTheory.Functor.pointwiseRightKanExtension definition

: D ⥤ H

Full source

/-- The constructed pointwise right Kan extension
when `HasPointwiseRightKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseRightKanExtension : D ⥤ H where
  obj Y := limit (StructuredArrow.projStructuredArrow.proj Y L ⋙ F)
  map {Y₁ Y₂} f := limit.lift (StructuredArrow.projStructuredArrow.proj Y₂ L ⋙ F)
      (Cone.mk (limit (StructuredArrow.projStructuredArrow.proj Y₁ L ⋙ F))
        { app := fun g ↦ limit.π (StructuredArrow.projStructuredArrow.proj Y₁ L ⋙ F)
            ((StructuredArrow.map f).obj g)
          naturality := fun g₁ g₂ φ ↦ by
            simpa using (limit.w (StructuredArrow.projStructuredArrow.proj Y₁ L ⋙ F)
              ((StructuredArrow.map f).map φ)).symm })
  map_id Y := limit.hom_ext (fun j => by
    dsimp
    simp only [limit.lift_π, id_comp]
    congr
    apply StructuredArrow.map_id)
  map_comp {Y₁ Y₂ Y₃} f f' := limit.hom_ext (fun j => by
    dsimp
    simp only [limit.lift_π, assoc]
    congr 1
    apply StructuredArrow.map_comp)

Pointwise Right Kan Extension Functor

Informal description

The functor `pointwiseRightKanExtension L F : D ⥤ H` is the pointwise right Kan extension of a functor `F : C ⥤ H` along a functor `L : C ⥤ D`. For each object `Y` in `D`, the value of the Kan extension at `Y` is defined as the limit of the functor `StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H`. Given a morphism `f : Y₁ ⟶ Y₂` in `D`, the induced morphism between the Kan extensions at `Y₁` and `Y₂` is constructed using the universal property of limits, ensuring compatibility with the structured arrows and their morphisms. The functoriality properties (identity and composition) are verified using the uniqueness of the limit-induced morphisms.

CategoryTheory.Functor.pointwiseRightKanExtensionCounit definition

: L ⋙ pointwiseRightKanExtension L F ⟶ F

Full source

/-- The counit of the constructed pointwise right Kan extension when
`HasPointwiseRightKanExtension L F` holds. -/
@[simps]
noncomputable def pointwiseRightKanExtensionCounit :
    L ⋙ pointwiseRightKanExtension L FL ⋙ pointwiseRightKanExtension L F ⟶ F where
  app X := limit.π (StructuredArrow.projStructuredArrow.proj (L.obj X) L ⋙ F)
    (StructuredArrow.mk (𝟙 (L.obj X)))
  naturality {X₁ X₂} f := by
    simp only [comp_obj, pointwiseRightKanExtension_obj, comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]
    rw [comp_id]
    let φ : StructuredArrow.mkStructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) :=
      StructuredArrow.homMk f
    exact (limit.w (StructuredArrow.projStructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

Counit of the pointwise right Kan extension

Informal description

The counit natural transformation $\varepsilon \colon L \circ \text{pointwiseRightKanExtension } L F \to F$ of the pointwise right Kan extension, where for each object $X$ in $C$, the component $\varepsilon_X$ is given by the projection morphism from the limit of the functor $\text{StructuredArrow.proj } (L(X)) L \circ F$ evaluated at the structured arrow $\text{StructuredArrow.mk } (1_{L(X)})$.

CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension definition

: (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsPointwiseRightKanExtension

Full source

/-- The functor `pointwiseRightKanExtension L F` is a pointwise right Kan
extension of `F` along `L`. -/
noncomputable def pointwiseRightKanExtensionIsPointwiseRightKanExtension :
    (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsPointwiseRightKanExtension :=
  fun X => IsLimit.ofIsoLimit (limit.isLimit _) (Cones.ext (Iso.refl _) (fun j => by
    dsimp
    simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]
    congr
    rw [comp_id, ← StructuredArrow.eq_mk]))

Pointwise right Kan extension property

Informal description

The functor `pointwiseRightKanExtension L F` is a pointwise right Kan extension of `F` along `L`, meaning that for every object `Y` in `D`, the cone `(RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).coneAt Y` is a limit cone for the functor `StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H`. More precisely, the cone at each `Y` is isomorphic to the limit cone of `StructuredArrow.proj Y L ⋙ F`, with the isomorphism given by the identity morphism on the limit object and the naturality conditions satisfied via the universal property of limits.

CategoryTheory.Functor.pointwiseRightKanExtensionIsUniversal definition

: (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsUniversal

Full source

/-- The functor `pointwiseRightKanExtension L F` is a right Kan extension of `F` along `L`. -/
noncomputable def pointwiseRightKanExtensionIsUniversal :
    (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsUniversal :=
  (pointwiseRightKanExtensionIsPointwiseRightKanExtension L F).isUniversal

Universality of the pointwise right Kan extension

Informal description

The pointwise right Kan extension $\text{pointwiseRightKanExtension } L F$ of a functor $F \colon C \to H$ along a functor $L \colon C \to D$ is universal, meaning it satisfies the universal property of being terminal in the category of right extensions of $F$ along $L$. Specifically, for any other right extension $G$ of $F$ along $L$, there exists a unique morphism from $G$ to $\text{pointwiseRightKanExtension } L F$ in this category.

CategoryTheory.Functor.instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit instance

: (pointwiseRightKanExtension L F).IsRightKanExtension (pointwiseRightKanExtensionCounit L F)

Full source

instance : (pointwiseRightKanExtension L F).IsRightKanExtension
    (pointwiseRightKanExtensionCounit L F) where
  nonempty_isUniversal := ⟨pointwiseRightKanExtensionIsUniversal L F⟩

The Pointwise Right Kan Extension Property

Informal description

The functor $\text{pointwiseRightKanExtension}\, L\, F$ equipped with the counit natural transformation $\text{pointwiseRightKanExtensionCounit}\, L\, F$ forms a right Kan extension of the functor $F \colon C \to H$ along the functor $L \colon C \to D$. This means that for every object $Y$ in $D$, the cone over the diagram $\text{StructuredArrow.proj}\, Y\, L \circ F$ with apex $\text{pointwiseRightKanExtension}\, L\, F\, Y$ is a limit cone, and the counit transformation exhibits the universal property of the right Kan extension.

CategoryTheory.Functor.instHasRightKanExtension instance

: HasRightKanExtension L F

Full source

instance : HasRightKanExtension L F :=
  HasRightKanExtension.mk _ (pointwiseRightKanExtensionCounit L F)

Existence of Right Kan Extension

Informal description

Given functors $L \colon C \to D$ and $F \colon C \to H$, there exists a right Kan extension of $F$ along $L$.

CategoryTheory.Functor.structuredArrowMapCone definition

(G : D ⥤ H) (α : L ⋙ G ⟶ F) (Y : D) : Cone (StructuredArrow.proj Y L ⋙ F)

Full source

/-- An auxiliary cocone used in the lemma `pointwiseRightKanExtension_lift_app` -/
@[simps]
def structuredArrowMapCone (G : D ⥤ H) (α : L ⋙ GL ⋙ G ⟶ F) (Y : D) :
    Cone (StructuredArrow.projStructuredArrow.proj Y L ⋙ F) where
  pt := G.obj Y
  π := {
    app := fun f ↦ G.map f.hom ≫ α.app f.right
    naturality := by simp [← α.naturality, ← G.map_comp_assoc] }

Cone over structured arrows induced by natural transformation

Informal description

Given functors $L \colon C \to D$, $F \colon C \to H$, and $G \colon D \to H$, along with a natural transformation $\alpha \colon L \circ G \Rightarrow F$ and an object $Y \colon D$, the cone `structuredArrowMapCone L F G α Y` is constructed with: - The cone point being $G(Y)$. - The natural transformation components given by composing $G$ applied to the morphism part of each structured arrow with the corresponding component of $\alpha$. This cone is over the functor $\text{StructuredArrow.proj}\,Y\,L \circ F \colon \text{StructuredArrow}\,Y\,L \to H$.

CategoryTheory.Functor.pointwiseRightKanExtension_lift_app theorem

 (G : D ⥤ H) (α : L ⋙ G ⟶ F) (Y : D) :
  ((pointwiseRightKanExtension L F).liftOfIsRightKanExtension (pointwiseRightKanExtensionCounit L F) G α |>.app Y) =
    limit.lift _ (structuredArrowMapCone L F G α Y)

Full source

@[simp]
lemma pointwiseRightKanExtension_lift_app (G : D ⥤ H) (α : L ⋙ GL ⋙ G ⟶ F) (Y : D) :
    ((pointwiseRightKanExtension L F).liftOfIsRightKanExtension
      (pointwiseRightKanExtensionCounit L F) G α |>.app Y) =
        limit.lift _ (structuredArrowMapCone L F G α Y) := by
  let β : G ⟶ L.pointwiseRightKanExtension F :=
    { app := fun Y ↦ limit.lift _ (structuredArrowMapCone L F G α Y) }
  have h : (pointwiseRightKanExtension L F).liftOfIsRightKanExtension
      (pointwiseRightKanExtensionCounit L F) G α = β := by
    apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)
    aesop
  exact NatTrans.congr_app h Y

Component Formula for Induced Morphism into Pointwise Right 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 a functor with a natural transformation $\alpha \colon L \circ G \to F$. For any object $Y$ in $D$, the component at $Y$ of the induced morphism from $G$ to the pointwise right Kan extension $\text{pointwiseRightKanExtension}\, L\, F$ is equal to the universal morphism $\text{limit.lift}$ applied to the cone $\text{structuredArrowMapCone}\, L\, F\, G\, \alpha\, Y$ over the diagram $\text{StructuredArrow.proj}\, Y\, L \circ F$. In symbols: \[ (\text{liftOfIsRightKanExtension}\, (\text{pointwiseRightKanExtensionCounit}\, L\, F)\, G\, \alpha)_Y = \text{limit.lift}\, (\text{StructuredArrow.proj}\, Y\, L \circ F)\, (\text{structuredArrowMapCone}\, L\, F\, G\, \alpha\, Y) \]

CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension definition

 (F' : D ⥤ H) (α : L ⋙ F' ⟶ F) [F'.IsRightKanExtension α] : (RightExtension.mk _ α).IsPointwiseRightKanExtension

Full source

/-- If `F` admits a pointwise right Kan extension along `L`, then any right Kan extension of `F`
along `L` is a pointwise right Kan extension. -/
noncomputable def isPointwiseRightKanExtensionOfIsRightKanExtension (F' : D ⥤ H) (α : L ⋙ F'L ⋙ F' ⟶ F)
    [F'.IsRightKanExtension α] :
    (RightExtension.mk _ α).IsPointwiseRightKanExtension :=
  RightExtension.isPointwiseRightKanExtensionEquivOfIso
    (IsLimit.conePointUniqueUpToIso (pointwiseRightKanExtensionIsUniversal L F)
      (F'.isUniversalOfIsRightKanExtension α))
    (pointwiseRightKanExtensionIsPointwiseRightKanExtension L F)

Right Kan extension implies pointwise right Kan 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 $, if $ (F', \alpha) $ is a right Kan extension of $ F $ along $ L $, then it is also a pointwise right Kan extension. This means that for every object $ Y $ in $ D $, the cone $ (F', \alpha).\text{coneAt}\, Y $ is a limit cone for the functor $ \text{StructuredArrow.proj}\, Y\, L \circ F \colon \text{StructuredArrow}\, Y\, L \to H $.

References