Adjunctions involving evaluation

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

noncomputable def CategoryTheory.evaluationLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) : Functor D (Functor C D)

The left adjoint of evaluation.

@[simp]

theorem CategoryTheory.evaluationLeftAdjoint_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (d : D) (t : C) : ((evaluationLeftAdjoint D c).obj d).obj t = ∐ fun (x : c ⟶ t) => d

@[simp]

theorem CategoryTheory.evaluationLeftAdjoint_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((evaluationLeftAdjoint D c).obj d).map f = Limits.Sigma.desc fun (g : c ⟶ X✝) => Limits.Sigma.ι (fun (x : c ⟶ Y✝) => d) (CategoryStruct.comp g f)

@[simp]

theorem CategoryTheory.evaluationLeftAdjoint_map_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) {x✝ d₂ : D} (f : x✝ ⟶ d₂) (x✝¹ : C) : ((evaluationLeftAdjoint D c).map f).app x✝¹ = Limits.Sigma.desc fun (h : c ⟶ x✝¹) => CategoryStruct.comp f (Limits.Sigma.ι (fun (x : c ⟶ x✝¹) => d₂) h)

noncomputable def CategoryTheory.evaluationAdjunctionRight {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) : evaluationLeftAdjoint D c ⊣ (evaluation C D).obj c

The adjunction showing that evaluation is a right adjoint.

@[simp]

theorem CategoryTheory.evaluationAdjunctionRight_unit_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (X : D) : (evaluationAdjunctionRight D c).unit.app X = Limits.Sigma.ι (fun (x : c ⟶ c) => X) (CategoryStruct.id c)

@[simp]

theorem CategoryTheory.evaluationAdjunctionRight_counit_app_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (Y : Functor C D) (x✝ : C) : ((evaluationAdjunctionRight D c).counit.app Y).app x✝ = Limits.Sigma.desc fun (h : c ⟶ x✝) => Y.map h

instance CategoryTheory.evaluationIsRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) : ((evaluation C D).obj c).IsRightAdjoint

theorem CategoryTheory.NatTrans.mono_iff_mono_app' {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] {F G : Functor C D} (η : F ⟶ G) : Mono η ↔ ∀ (c : C), Mono (η.app c)

See also the file Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean for a similar result under a HasPullbacks assumption.

noncomputable def CategoryTheory.evaluationRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : Functor D (Functor C D)

The right adjoint of evaluation.

@[simp]

theorem CategoryTheory.evaluationRightAdjoint_map_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (x✝ : C) : ((evaluationRightAdjoint D c).map f).app x✝ = Limits.Pi.lift fun (g : x✝ ⟶ c) => CategoryStruct.comp (Limits.Pi.π (fun (x : x✝ ⟶ c) => X✝) g) f

@[simp]

theorem CategoryTheory.evaluationRightAdjoint_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) (t : C) : ((evaluationRightAdjoint D c).obj d).obj t = ∏ᶜ fun (x : t ⟶ c) => d

@[simp]

theorem CategoryTheory.evaluationRightAdjoint_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((evaluationRightAdjoint D c).obj d).map f = Limits.Pi.lift fun (g : Y✝ ⟶ c) => Limits.Pi.π (fun (x : X✝ ⟶ c) => d) (CategoryStruct.comp f g)

noncomputable def CategoryTheory.evaluationAdjunctionLeft {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : (evaluation C D).obj c ⊣ evaluationRightAdjoint D c

The adjunction showing that evaluation is a left adjoint.

@[simp]

theorem CategoryTheory.evaluationAdjunctionLeft_counit_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (Y : D) : (evaluationAdjunctionLeft D c).counit.app Y = Limits.Pi.π (fun (x : c ⟶ c) => Y) (CategoryStruct.id c)

@[simp]

theorem CategoryTheory.evaluationAdjunctionLeft_unit_app_app {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (X : Functor C D) (x✝ : C) : ((evaluationAdjunctionLeft D c).unit.app X).app x✝ = Limits.Pi.lift fun (g : x✝ ⟶ c) => X.map g

instance CategoryTheory.evaluationIsLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] (c : C) : ((evaluation C D).obj c).IsLeftAdjoint

theorem CategoryTheory.NatTrans.epi_iff_epi_app' {C : Type u₁} [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] {F G : Functor C D} (η : F ⟶ G) : Epi η ↔ ∀ (c : C), Epi (η.app c)

See also the file Mathlib/CategoryTheory/Limits/FunctorCategory/EpiMono.lean for a similar result under a HasPushouts assumption.