# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations
@[simp]
theorem category_theory.evaluation_left_adjoint_map_app {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d₁ d₂ : D) (f : d₁ d₂) (e : C) :
@[simp]
theorem category_theory.evaluation_left_adjoint_obj_obj {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d : D) (t : C) :
.obj t = λ (i : c t), d
@[simp]
theorem category_theory.evaluation_left_adjoint_obj_map {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d : D) (u v : C) (f : u v) :
@[simp]
theorem category_theory.evaluation_adjunction_right_counit_app_app {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (Y : C D) (e : C) :
noncomputable def category_theory.evaluation_adjunction_right {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) :

Equations
@[simp]
theorem category_theory.evaluation_adjunction_right_unit_app {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (X : D) :
= category_theory.limits.sigma.ι (λ (_x : c c), X) (𝟙 c)
@[protected, instance]
noncomputable def category_theory.evaluation_is_right_adjoint {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) :
Equations
theorem category_theory.nat_trans.mono_iff_mono_app {C : Type u₁} (D : Type u₂) [ (a b : C), ] {F G : C D} (η : F G) :
(c : C), category_theory.mono (η.app c)
@[simp]
theorem category_theory.evaluation_right_adjoint_obj_obj {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d : D) (t : C) :
.obj t = λ (i : t c), d
noncomputable def category_theory.evaluation_right_adjoint {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) :
D C D

Equations
@[simp]
theorem category_theory.evaluation_right_adjoint_map_app {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d₁ d₂ : D) (f : d₁ d₂) (t : C) :
.app t = category_theory.limits.pi.lift (λ (g : t c), category_theory.limits.pi.π (λ (i : t c), d₁) g f)
@[simp]
theorem category_theory.evaluation_right_adjoint_obj_map {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) (d : D) (u v : C) (f : u v) :
.map f = category_theory.limits.pi.lift (λ (g : v c), category_theory.limits.pi.π (λ (i : u c), d) (f g))
noncomputable def category_theory.evaluation_adjunction_left {C : Type u₁} (D : Type u₂) [ (a b : C), ] (c : C) :