category_theory.adjunction.evaluation

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

category_theory.evaluation_left_adjoint D c = {obj := λ (d : D), {obj := λ (t : C), ∐ λ (i : c ⟶ t), d, map := λ (u v : C) (f : u ⟶ v), category_theory.limits.sigma.desc (λ (g : c ⟶ u), category_theory.limits.sigma.ι (λ (_x : c ⟶ v), d) (g ≫ f)), map_id' := _, map_comp' := _}, map := λ (d₁ d₂ : D) (f : d₁ ⟶ d₂), {app := λ (e : C), category_theory.limits.sigma.desc (λ (h : c ⟶ e), f ≫ category_theory.limits.sigma.ι (λ (_x : c ⟶ e), d₂) h), naturality' := _}, map_id' := _, map_comp' := _}

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

category_theory.evaluation_adjunction_right D c = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (d : D) (F : C ⥤ D), {to_fun := λ (f : (category_theory.evaluation_left_adjoint D c).obj d ⟶ F), category_theory.limits.sigma.ι (λ (_x : c ⟶ c), d) (𝟙 c) ≫ f.app c, inv_fun := λ (f : d ⟶ ((category_theory.evaluation C D).obj c).obj F), {app := λ (e : C), category_theory.limits.sigma.desc (λ (h : c ⟶ e), f ≫ F.map h), naturality' := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

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

category_theory.evaluation_is_right_adjoint D c = {left := category_theory.evaluation_left_adjoint D c, adj := category_theory.evaluation_adjunction_right D c}

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

category_theory.evaluation_right_adjoint D c = {obj := λ (d : D), {obj := λ (t : C), ∏ λ (i : t ⟶ c), d, map := λ (u v : C) (f : u ⟶ v), category_theory.limits.pi.lift (λ (g : v ⟶ c), category_theory.limits.pi.π (λ (i : u ⟶ c), d) (f ≫ g)), map_id' := _, map_comp' := _}, map := λ (d₁ d₂ : D) (f : d₁ ⟶ d₂), {app := λ (t : C), category_theory.limits.pi.lift (λ (g : t ⟶ c), category_theory.limits.pi.π (λ (i : t ⟶ c), d₁) g ≫ f), naturality' := _}, map_id' := _, map_comp' := _}

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

category_theory.evaluation_adjunction_left D c = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (F : C ⥤ D) (d : D), {to_fun := λ (f : ((category_theory.evaluation C D).obj c).obj F ⟶ d), {app := λ (t : C), category_theory.limits.pi.lift (λ (g : t ⟶ c), F.map g ≫ f), naturality' := _}, inv_fun := λ (f : F ⟶ (category_theory.evaluation_right_adjoint D c).obj d), f.app c ≫ category_theory.limits.pi.π (λ (i : c ⟶ c), d) (𝟙 c), left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

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

category_theory.evaluation_is_left_adjoint D c = {right := category_theory.evaluation_right_adjoint D c, adj := category_theory.evaluation_adjunction_left D c}

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)

mathlib documentation

Adjunctions involving evaluation #