mathlib3 documentation

category_theory.adjunction.evaluation

Adjunctions involving evaluation #

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.

The left adjoint of evaluation.

Equations
@[simp]

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) :