# Documentation

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

@[simp]
theorem CategoryTheory.evaluationLeftAdjoint_obj_map {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (d : D) :
∀ {X Y : C} (f : X Y), (.obj d).map f = CategoryTheory.Limits.Sigma.desc fun (g : c X) => CategoryTheory.Limits.Sigma.ι (fun (x : c Y) => d)
@[simp]
theorem CategoryTheory.evaluationLeftAdjoint_obj_obj {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (d : D) (t : C) :
(.obj d).obj t = fun (x : c t) => d
@[simp]
theorem CategoryTheory.evaluationLeftAdjoint_map_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :
∀ {x d₂ : D} (f : x d₂) (e : C), (.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₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.evaluationAdjunctionRight_counit_app_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (Y : ) (e : C) :
(.counit.app Y).app e = CategoryTheory.Limits.Sigma.desc fun (h : c e) => Y.map h
@[simp]
theorem CategoryTheory.evaluationAdjunctionRight_unit_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (X : D) :
.unit.app X = CategoryTheory.Limits.Sigma.ι (fun (x : c c) => X)
def CategoryTheory.evaluationAdjunctionRight {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :
.obj c

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.evaluationIsRightAdjoint {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :
Equations
• =
theorem CategoryTheory.NatTrans.mono_iff_mono_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] {F : } {G : } (η : F G) :
∀ (c : C), CategoryTheory.Mono (η.app c)
@[simp]
theorem CategoryTheory.evaluationRightAdjoint_obj_map {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (d : D) :
∀ {X Y : C} (f : X Y), (.obj d).map f = CategoryTheory.Limits.Pi.lift fun (g : Y c) => CategoryTheory.Limits.Pi.π (fun (x : X c) => d)
@[simp]
theorem CategoryTheory.evaluationRightAdjoint_map_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :
∀ {X Y : D} (f : X Y) (t : C), (.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₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (d : D) (t : C) :
(.obj d).obj t = ∏ᶜ fun (x : t c) => d
def CategoryTheory.evaluationRightAdjoint {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.evaluationAdjunctionLeft_counit_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (Y : D) :
.counit.app Y = CategoryTheory.Limits.Pi.π (fun (x : c c) => Y)
@[simp]
theorem CategoryTheory.evaluationAdjunctionLeft_unit_app_app {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) (X : ) (t : C) :
(.unit.app X).app t = CategoryTheory.Limits.Pi.lift fun (g : t c) => X.map g
def CategoryTheory.evaluationAdjunctionLeft {C : Type u₁} [] (D : Type u₂) [] [∀ (a b : C), ] (c : C) :
.obj c