mathlib documentation

category_theory.adjunction.evaluation

Adjunctions involving evaluation #

We show that evaluation of functors have adjoints, given the existence of (co)products.

noncomputable def category_theory.evaluation_left_adjoint {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_coproducts_of_shape (a b) D] (c : C) :
D C D

The left adjoint of evaluation.

Equations
@[simp]
theorem category_theory.evaluation_left_adjoint_map_app {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_coproducts_of_shape (a b) D] (c : C) (d₁ d₂ : D) (f : d₁ d₂) (e : C) :
@[simp]
theorem category_theory.evaluation_left_adjoint_obj_obj {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_coproducts_of_shape (a b) D] (c : C) (d : D) (t : C) :
@[simp]
theorem category_theory.evaluation_left_adjoint_obj_map {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_coproducts_of_shape (a b) D] (c : C) (d : D) (u v : C) (f : u v) :

The adjunction showing that evaluation is a right adjoint.

Equations
theorem category_theory.nat_trans.mono_iff_app_mono {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_coproducts_of_shape (a b) D] {F G : C D} (η : F G) :
@[simp]
theorem category_theory.evaluation_right_adjoint_obj_obj {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_products_of_shape (a b) D] (c : C) (d : D) (t : C) :
noncomputable def category_theory.evaluation_right_adjoint {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_products_of_shape (a b) D] (c : C) :
D C D

The right adjoint of evaluation.

Equations
@[simp]
theorem category_theory.evaluation_right_adjoint_map_app {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_products_of_shape (a b) D] (c : C) (d₁ d₂ : D) (f : d₁ d₂) (t : C) :
@[simp]
theorem category_theory.evaluation_right_adjoint_obj_map {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_products_of_shape (a b) D] (c : C) (d : D) (u v : C) (f : u v) :

The adjunction showing that evaluation is a left adjoint.

Equations
theorem category_theory.nat_trans.epi_iff_app_epi {C : Type u₁} [category_theory.category C] (D : Type u₂) [category_theory.category D] [∀ (a b : C), category_theory.limits.has_products_of_shape (a b) D] {F G : C D} (η : F G) :