Adjunctions involving evaluation #
We show that evaluation of functors have adjoints, given the existence of (co)products.
@[simp]
theorem
CategoryTheory.evaluationLeftAdjoint_obj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
(d : D)
:
∀ {X Y : C} (f : X ⟶ Y),
((CategoryTheory.evaluationLeftAdjoint D c).obj d).map f = CategoryTheory.Limits.Sigma.desc fun (g : c ⟶ X) =>
CategoryTheory.Limits.Sigma.ι (fun (x : c ⟶ Y) => d) (CategoryTheory.CategoryStruct.comp g f)
@[simp]
theorem
CategoryTheory.evaluationLeftAdjoint_map_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
:
∀ {x d₂ : D} (f : x ⟶ d₂) (e : C),
((CategoryTheory.evaluationLeftAdjoint D c).map f).app e = CategoryTheory.Limits.Sigma.desc fun (h : c ⟶ e) =>
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Sigma.ι (fun (x : c ⟶ e) => d₂) h)
@[simp]
theorem
CategoryTheory.evaluationLeftAdjoint_obj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
(d : D)
(t : C)
:
((CategoryTheory.evaluationLeftAdjoint D c).obj d).obj t = ∐ fun (x : c ⟶ t) => d
def
CategoryTheory.evaluationLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
:
The left adjoint of evaluation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.evaluationAdjunctionRight_counit_app_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
(Y : CategoryTheory.Functor C D)
(e : C)
:
((CategoryTheory.evaluationAdjunctionRight D c).counit.app Y).app e = CategoryTheory.Limits.Sigma.desc fun (h : c ⟶ e) => Y.map h
@[simp]
theorem
CategoryTheory.evaluationAdjunctionRight_unit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
(X : D)
:
(CategoryTheory.evaluationAdjunctionRight D c).unit.app X = CategoryTheory.Limits.Sigma.ι (fun (x : c ⟶ c) => X) (CategoryTheory.CategoryStruct.id c)
def
CategoryTheory.evaluationAdjunctionRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
:
CategoryTheory.evaluationLeftAdjoint D c ⊣ (CategoryTheory.evaluation C D).obj c
The adjunction showing that evaluation is a right adjoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.evaluationIsRightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
(c : C)
:
((CategoryTheory.evaluation C D).obj c).IsRightAdjoint
Equations
- ⋯ = ⋯
theorem
CategoryTheory.NatTrans.mono_iff_mono_app'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(η : F ⟶ G)
:
CategoryTheory.Mono η ↔ ∀ (c : C), CategoryTheory.Mono (η.app c)
See also the file CategoryTheory.Limits.FunctorCategoryEpiMono
for a similar result under a HasPullbacks
assumption.
@[simp]
theorem
CategoryTheory.evaluationRightAdjoint_map_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
:
∀ {X Y : D} (f : X ⟶ Y) (t : C),
((CategoryTheory.evaluationRightAdjoint D c).map f).app t = CategoryTheory.Limits.Pi.lift fun (g : t ⟶ c) =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (x : t ⟶ c) => X) g) f
@[simp]
theorem
CategoryTheory.evaluationRightAdjoint_obj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
(d : D)
(t : C)
:
((CategoryTheory.evaluationRightAdjoint D c).obj d).obj t = ∏ᶜ fun (x : t ⟶ c) => d
@[simp]
theorem
CategoryTheory.evaluationRightAdjoint_obj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
(d : D)
:
∀ {X Y : C} (f : X ⟶ Y),
((CategoryTheory.evaluationRightAdjoint D c).obj d).map f = CategoryTheory.Limits.Pi.lift fun (g : Y ⟶ c) =>
CategoryTheory.Limits.Pi.π (fun (x : X ⟶ c) => d) (CategoryTheory.CategoryStruct.comp f g)
def
CategoryTheory.evaluationRightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
:
The right adjoint of evaluation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.evaluationAdjunctionLeft_counit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
(Y : D)
:
(CategoryTheory.evaluationAdjunctionLeft D c).counit.app Y = CategoryTheory.Limits.Pi.π (fun (x : c ⟶ c) => Y) (CategoryTheory.CategoryStruct.id c)
@[simp]
theorem
CategoryTheory.evaluationAdjunctionLeft_unit_app_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
(X : CategoryTheory.Functor C D)
(t : C)
:
((CategoryTheory.evaluationAdjunctionLeft D c).unit.app X).app t = CategoryTheory.Limits.Pi.lift fun (g : t ⟶ c) => X.map g
def
CategoryTheory.evaluationAdjunctionLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
:
(CategoryTheory.evaluation C D).obj c ⊣ CategoryTheory.evaluationRightAdjoint D c
The adjunction showing that evaluation is a left adjoint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.evaluationIsLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
(c : C)
:
((CategoryTheory.evaluation C D).obj c).IsLeftAdjoint
Equations
- ⋯ = ⋯
theorem
CategoryTheory.NatTrans.epi_iff_epi_app'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(D : Type u₂)
[CategoryTheory.Category.{v₂, u₂} D]
[∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(η : F ⟶ G)
:
CategoryTheory.Epi η ↔ ∀ (c : C), CategoryTheory.Epi (η.app c)
See also the file CategoryTheory.Limits.FunctorCategoryEpiMono
for a similar result under a HasPushouts
assumption.