Library HoTT.Categories.KanExtensions.Core
Require Import Category.Core Functor.Core.
Require Import FunctorCategory.Core.
Require Import Functor.Composition.Functorial.Core.
Require Import UniversalProperties.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Local Open Scope category_scope.
Require Import FunctorCategory.Core.
Require Import Functor.Composition.Functorial.Core.
Require Import UniversalProperties.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Local Open Scope category_scope.
Quoting nCatLab on Kan Exensions:
The Kan extension of a functor F : C → D with respect to a
functor
is, if it exists, a kind of best approximation to the problem of
finding a functor C' → D such that
hence to extending the domain of F through p from C to C'.
More generally, this makes sense not only in Cat but in any
2-category.
Similarly, a Kan lift is the best approximation to lifting a
morphism F : C → D through a morphism
to a morphism F̂
Kan extensions are ubiquitous. See the discussion at Examples
below.
There are various slight variants of the definition of Kan
extension. In good cases they all exist and all coincide, but in
some cases only some of these will actually exist.
We (have to) distinguish the following cases:
If the pointwise version exists, then it coincides with the
“ordinary” or “weak” version, but the former may exist without the
pointwise version existing. See below for more.
Some authors (such as Kelly) assert that only pointwise Kan
extensions deserve the name “Kan extension,” and use the term as
“weak Kan extension” for a functor equipped with a universal
natural transformation. It is certainly true that most Kan
extensions which arise in practice are pointwise. This distinction
is even more important in enriched category theory.
Idea
C | | p ↓ C'
F C -----> D | ↗ | p / | / ↓ / C'
D' | ↓ D
D' ↗ | / | F̂ / | / | / F ↓ C --------> D
Definitions
- “ordinary” or “weak” Kan extensions
- global Kan extensions,
- local Kan extensions,
- global Kan extensions,
- “pointwise” or “strong” Kan extensions
Ordinary or weak Kan extensions
Global Kan extensions
p h p* h : C --> C' --> D
Pullback-along functor
Context `{Funext}.
Variables C C' D : PreCategory.
Section pullback_along.
Definition pullback_along_functor
: object ((C → C') → (C' → D) → (C → D))
:= Functor.Composition.Functorial.Core.compose_functor _ _ _.
Definition pullback_along (p : Functor C C')
: object ((C' → D) → (C → D))
:= Eval hnf in pullback_along_functor p.
End pullback_along.
Variables C C' D : PreCategory.
Section pullback_along.
Definition pullback_along_functor
: object ((C → C') → (C' → D) → (C → D))
:= Functor.Composition.Functorial.Core.compose_functor _ _ _.
Definition pullback_along (p : Functor C C')
: object ((C' → D) → (C → D))
:= Eval hnf in pullback_along_functor p.
End pullback_along.
Definition. If p× has a left adjoint, typically denoted p_! :
(C → D) → (C' → D) or Lan_p : (C → D) → (C' → D) then this
left adjoint is called the (ordinary or weak) left Kan extension
operation along p. For h ∈ (C → D) we call p_! h the left
Kan extension of h along p.
Similarly, if p× has a right adjoint, this right adjoint is
called the right Kan extension operation along p. It is
typically denoted p_× : (C → D) → (C' → D) or Ran = Ran_p :
(C → D) → (C' → D).
The analogous definition clearly makes sense as stated in other
contexts, such as in enriched category theory.
Observation. If C' = 1 is the terminal category, then
- the left Kan extension operation forms the colimit of a functor;
- the right Kan extension operation forms the limit of a functor.
Left Kan extensions
Colimits are initial morphisms.
Definition IsLeftKanExtensionAlong (p : Functor C C') (h : Functor C D)
:= @IsInitialMorphism (_ → _) _ h (pullback_along p).
:= @IsInitialMorphism (_ → _) _ h (pullback_along p).
Definition IsRightKanExtensionAlong (p : Functor C C') (h : Functor C D)
:= @IsTerminalMorphism _ (_ → _) (pullback_along p) h.
End kan_extensions.
:= @IsTerminalMorphism _ (_ → _) (pullback_along p) h.
End kan_extensions.