Adjunctions involving evaluation

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The left adjoint of evaluation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

The adjunction showing that evaluation is a right adjoint.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.evaluationIsRightAdjoint D c = { left := CategoryTheory.evaluationLeftAdjoint D c, adj := CategoryTheory.evaluationAdjunctionRight D c }

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The right adjoint of evaluation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

The adjunction showing that evaluation is a left adjoint.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.evaluationIsLeftAdjoint D c = { right := CategoryTheory.evaluationRightAdjoint D c, adj := CategoryTheory.evaluationAdjunctionLeft D c }

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