Kan extensions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the right and left Kan extensions of a functor. They exist under the assumption that the target category has enough limits resp. colimits.
The main definitions are Ran ι and Lan ι, where ι : S ⥤ L is a functor.
Namely, Ran ι is the right Kan extension, while Lan ι is the left Kan extension,
both as functors (S ⥤ D) ⥤ (L ⥤ D).
To access the right resp. left adjunction associated to these, use Ran.adjunction
resp. Lan.adjunction.
Projects #
A lot of boilerplate could be generalized by defining and working with pseudofunctors.
@[reducible]
def
category_theory.Ran.diagram
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
(x : L) :
The diagram indexed by Ran.index ι x used to define Ran.
@[simp]
def
category_theory.Ran.cone
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
{ι : S ⥤ L}
{F : S ⥤ D}
{G : L ⥤ D}
(x : L)
(f : ι ⋙ G ⟶ F) :
A cone over Ran.diagram ι F x used to define Ran.
Equations
- category_theory.Ran.cone x f = {X := G.obj x, π := {app := λ (i : category_theory.structured_arrow x ι), G.map i.hom ≫ f.app i.right, naturality' := _}}
noncomputable
def
category_theory.Ran.loc
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)] :
L ⥤ D
An auxiliary definition used to define Ran.
Equations
- category_theory.Ran.loc ι F = {obj := λ (x : L), category_theory.limits.limit (category_theory.Ran.diagram ι F x), map := λ (x y : L) (f : x ⟶ y), category_theory.limits.limit.pre (category_theory.Ran.diagram ι F x) (category_theory.structured_arrow.map f), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.Ran.loc_map
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)]
(x y : L)
(f : x ⟶ y) :
@[simp]
theorem
category_theory.Ran.loc_obj
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)]
(x : L) :
@[simp]
theorem
category_theory.Ran.equiv_symm_apply_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)]
(G : L ⥤ D)
(f : ((category_theory.whiskering_left S L D).obj ι).obj G ⟶ F)
(x : L) :
(⇑((category_theory.Ran.equiv ι F G).symm) f).app x = category_theory.limits.limit.lift (category_theory.Ran.diagram ι F x) (category_theory.Ran.cone x f)
noncomputable
def
category_theory.Ran.equiv
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)]
(G : L ⥤ D) :
(G ⟶ category_theory.Ran.loc ι F) ≃ (((category_theory.whiskering_left S L D).obj ι).obj G ⟶ F)
An auxiliary definition used to define Ran and Ran.adjunction.
Equations
- category_theory.Ran.equiv ι F G = {to_fun := λ (f : G ⟶ category_theory.Ran.loc ι F), {app := λ (x : S), f.app (ι.obj x) ≫ category_theory.limits.limit.π (category_theory.Ran.diagram ι F (ι.obj x)) (category_theory.structured_arrow.mk (𝟙 (ι.obj x))), naturality' := _}, inv_fun := λ (f : ((category_theory.whiskering_left S L D).obj ι).obj G ⟶ F), {app := λ (x : L), category_theory.limits.limit.lift (category_theory.Ran.diagram ι F x) (category_theory.Ran.cone x f), naturality' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.Ran.equiv_apply_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)]
(G : L ⥤ D)
(f : G ⟶ category_theory.Ran.loc ι F)
(x : S) :
(⇑(category_theory.Ran.equiv ι F G) f).app x = f.app (ι.obj x) ≫ category_theory.limits.limit.π (category_theory.Ran.diagram ι F (ι.obj x)) (category_theory.structured_arrow.mk (𝟙 (ι.obj x)))
@[simp]
theorem
category_theory.Ran_obj_map
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D]
(G : S ⥤ D)
(x y : L)
(f : x ⟶ y) :
noncomputable
def
category_theory.Ran
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D] :
The right Kan extension of a functor.
Equations
- category_theory.Ran ι = category_theory.adjunction.right_adjoint_of_equiv (λ (F : L ⥤ D) (G : S ⥤ D), (category_theory.Ran.equiv ι G F).symm) _
@[simp]
theorem
category_theory.Ran_obj_obj
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D]
(G : S ⥤ D)
(x : L) :
((category_theory.Ran ι).obj G).obj x = category_theory.limits.limit (category_theory.Ran.diagram ι G x)
@[simp]
theorem
category_theory.Ran_map_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D]
(Y Y' : S ⥤ D)
(g : Y ⟶ Y')
(x : L) :
((category_theory.Ran ι).map g).app x = category_theory.limits.limit.lift (category_theory.Ran.diagram ι Y' x) {X := category_theory.limits.limit (category_theory.Ran.diagram ι Y x) _, π := {app := λ (i : category_theory.structured_arrow x ι), category_theory.limits.limit.pre (category_theory.Ran.diagram ι Y x) (category_theory.structured_arrow.map i.hom) ≫ (𝟙 (category_theory.limits.limit (category_theory.Ran.diagram ι Y (ι.obj i.right))) ≫ category_theory.limits.limit.π (category_theory.Ran.diagram ι Y (ι.obj i.right)) (category_theory.structured_arrow.mk (𝟙 (ι.obj i.right)))) ≫ g.app i.right, naturality' := _}}
noncomputable
def
category_theory.Ran.adjunction
{S : Type u₁}
{L : Type u₂}
(D : Type u₃)
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D] :
(category_theory.whiskering_left S L D).obj ι ⊣ category_theory.Ran ι
The adjunction associated to Ran.
Equations
- category_theory.Ran.adjunction D ι = category_theory.adjunction.adjunction_of_equiv_right (λ (F : L ⥤ D) (G : S ⥤ D), (category_theory.Ran.equiv ι G F).symm) _
theorem
category_theory.Ran.reflective
{S : Type u₁}
{L : Type u₂}
(D : Type u₃)
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[category_theory.full ι]
[category_theory.faithful ι]
[∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D] :
@[reducible]
def
category_theory.Lan.diagram
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
(x : L) :
The diagram indexed by Ran.index ι x used to define Ran.
@[simp]
def
category_theory.Lan.cocone
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
{ι : S ⥤ L}
{F : S ⥤ D}
{G : L ⥤ D}
(x : L)
(f : F ⟶ ι ⋙ G) :
A cocone over Lan.diagram ι F x used to define Lan.
Equations
- category_theory.Lan.cocone x f = {X := G.obj x, ι := {app := λ (i : category_theory.costructured_arrow ι x), f.app i.left ≫ G.map i.hom, naturality' := _}}
@[simp]
theorem
category_theory.Lan.loc_map
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)]
(x y : L)
(f : x ⟶ y) :
@[simp]
theorem
category_theory.Lan.loc_obj
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)]
(x : L) :
noncomputable
def
category_theory.Lan.loc
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)] :
L ⥤ D
An auxiliary definition used to define Lan.
Equations
- category_theory.Lan.loc ι F = {obj := λ (x : L), category_theory.limits.colimit (category_theory.Lan.diagram ι F x), map := λ (x y : L) (f : x ⟶ y), category_theory.limits.colimit.pre (category_theory.Lan.diagram ι F y) (category_theory.costructured_arrow.map f), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.Lan.equiv_symm_apply_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)]
(G : L ⥤ D)
(f : F ⟶ ((category_theory.whiskering_left S L D).obj ι).obj G)
(x : L) :
(⇑((category_theory.Lan.equiv ι F G).symm) f).app x = category_theory.limits.colimit.desc (category_theory.Lan.diagram ι F x) (category_theory.Lan.cocone x f)
noncomputable
def
category_theory.Lan.equiv
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)]
(G : L ⥤ D) :
(category_theory.Lan.loc ι F ⟶ G) ≃ (F ⟶ ((category_theory.whiskering_left S L D).obj ι).obj G)
An auxiliary definition used to define Lan and Lan.adjunction.
Equations
- category_theory.Lan.equiv ι F G = {to_fun := λ (f : category_theory.Lan.loc ι F ⟶ G), {app := λ (x : S), category_theory.limits.colimit.ι (category_theory.Lan.diagram ι F (ι.obj x)) (category_theory.costructured_arrow.mk (𝟙 (ι.obj x))) ≫ f.app (ι.obj x), naturality' := _}, inv_fun := λ (f : F ⟶ ((category_theory.whiskering_left S L D).obj ι).obj G), {app := λ (x : L), category_theory.limits.colimit.desc (category_theory.Lan.diagram ι F x) (category_theory.Lan.cocone x f), naturality' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.Lan.equiv_apply_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
(F : S ⥤ D)
[I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)]
(G : L ⥤ D)
(f : category_theory.Lan.loc ι F ⟶ G)
(x : S) :
(⇑(category_theory.Lan.equiv ι F G) f).app x = category_theory.limits.colimit.ι (category_theory.Lan.diagram ι F (ι.obj x)) (category_theory.costructured_arrow.mk (𝟙 (ι.obj x))) ≫ f.app (ι.obj x)
@[simp]
theorem
category_theory.Lan_obj_obj
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D]
(F : S ⥤ D)
(x : L) :
((category_theory.Lan ι).obj F).obj x = category_theory.limits.colimit (category_theory.Lan.diagram ι F x)
@[simp]
theorem
category_theory.Lan_map_app
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D]
(X X' : S ⥤ D)
(f : X ⟶ X')
(x : L) :
((category_theory.Lan ι).map f).app x = category_theory.limits.colimit.desc (category_theory.Lan.diagram ι X x) {X := category_theory.limits.colimit (category_theory.Lan.diagram ι X' x) _, ι := {app := λ (i : category_theory.costructured_arrow ι x), (f.app i.left ≫ category_theory.limits.colimit.ι (category_theory.Lan.diagram ι X' (ι.obj i.left)) (category_theory.costructured_arrow.mk (𝟙 (ι.obj i.left))) ≫ 𝟙 (category_theory.limits.colimit (category_theory.Lan.diagram ι X' (ι.obj i.left)))) ≫ category_theory.limits.colimit.pre (category_theory.Lan.diagram ι X' x) (category_theory.costructured_arrow.map i.hom), naturality' := _}}
noncomputable
def
category_theory.Lan
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D] :
The left Kan extension of a functor.
Equations
- category_theory.Lan ι = category_theory.adjunction.left_adjoint_of_equiv (λ (F : S ⥤ D) (G : L ⥤ D), category_theory.Lan.equiv ι F G) _
@[simp]
theorem
category_theory.Lan_obj_map
{S : Type u₁}
{L : Type u₂}
{D : Type u₃}
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D]
(F : S ⥤ D)
(x y : L)
(f : x ⟶ y) :
noncomputable
def
category_theory.Lan.adjunction
{S : Type u₁}
{L : Type u₂}
(D : Type u₃)
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D] :
category_theory.Lan ι ⊣ (category_theory.whiskering_left S L D).obj ι
The adjunction associated to Lan.
Equations
- category_theory.Lan.adjunction D ι = category_theory.adjunction.adjunction_of_equiv_left (λ (F : S ⥤ D) (G : L ⥤ D), category_theory.Lan.equiv ι F G) _
theorem
category_theory.Lan.coreflective
{S : Type u₁}
{L : Type u₂}
(D : Type u₃)
[category_theory.category S]
[category_theory.category L]
[category_theory.category D]
(ι : S ⥤ L)
[category_theory.full ι]
[category_theory.faithful ι]
[∀ (X : L), category_theory.limits.has_colimits_of_shape (category_theory.costructured_arrow ι X) D] :