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.

source
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
source
@[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) :
((category_theory.evaluation_left_adjoint D c).map f).app e = category_theory.limits.sigma.desc (λ (h : c ⟶ e), f ≫ category_theory.limits.sigma.ι (λ (_x : c ⟶ e), d₂) h)
source
@[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) :
((category_theory.evaluation_left_adjoint D c).obj d).obj t = ∐ λ (i : c ⟶ t), d
source
@[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) :
((category_theory.evaluation_left_adjoint D c).obj d).map f = category_theory.limits.sigma.desc (λ (g : c ⟶ u), category_theory.limits.sigma.ι (λ (_x : c ⟶ v), d) (g ≫ f))
source
@[simp]
theorem category_theory.evaluation_adjunction_right_counit_app_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) (Y : C ⥤ D) (e : C) :
((category_theory.evaluation_adjunction_right D c).counit.app Y).app e = category_theory.limits.sigma.desc Y.map
source
noncomputable def category_theory.evaluation_adjunction_right {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) :
category_theory.evaluation_left_adjoint D c ⊣ (category_theory.evaluation C D).obj c

The adjunction showing that evaluation is a right adjoint.

Equations
source
@[simp]
theorem category_theory.evaluation_adjunction_right_unit_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) (X : D) :
(category_theory.evaluation_adjunction_right D c).unit.app X = category_theory.limits.sigma.ι (λ (_x : c ⟶ c), X) (𝟙 c)
source
@[protected, instance]
noncomputable def category_theory.evaluation_is_right_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) :
category_theory.is_right_adjoint ((category_theory.evaluation C D).obj c)
Equations
source
theorem category_theory.nat_trans.mono_iff_mono_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] {F G : C ⥤ D} (η : F ⟶ G) :
category_theory.mono η ↔ ∀ (c : C), category_theory.mono (η.app c)
source
@[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) :
((category_theory.evaluation_right_adjoint D c).obj d).obj t = ∏ λ (i : t ⟶ c), d
source
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
source
@[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) :
((category_theory.evaluation_right_adjoint D c).map f).app t = category_theory.limits.pi.lift (λ (g : t ⟶ c), category_theory.limits.pi.π (λ (i : t ⟶ c), d₁) g ≫ f)
source
@[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) :
((category_theory.evaluation_right_adjoint D c).obj d).map f = category_theory.limits.pi.lift (λ (g : v ⟶ c), category_theory.limits.pi.π (λ (i : u ⟶ c), d) (f ≫ g))
source
noncomputable def category_theory.evaluation_adjunction_left {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) :
(category_theory.evaluation C D).obj c ⊣ category_theory.evaluation_right_adjoint D c

The adjunction showing that evaluation is a left adjoint.

Equations
source
@[simp]
theorem category_theory.evaluation_adjunction_left_unit_app_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) (X : C ⥤ D) (t : C) :
((category_theory.evaluation_adjunction_left D c).unit.app X).app t = category_theory.limits.pi.lift X.map
source
@[simp]
theorem category_theory.evaluation_adjunction_left_counit_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) (Y : D) :
(category_theory.evaluation_adjunction_left D c).counit.app Y = category_theory.limits.pi.π (λ (i : c ⟶ c), Y) (𝟙 c)
source
@[protected, instance]
noncomputable def category_theory.evaluation_is_left_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) :
category_theory.is_left_adjoint ((category_theory.evaluation C D).obj c)
Equations
source
theorem category_theory.nat_trans.epi_iff_epi_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] {F G : C ⥤ D} (η : F ⟶ G) :
category_theory.epi η ↔ ∀ (c : C), category_theory.epi (η.app c)