Adjunctions between functors

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

We provide various useful constructors:

• mkOfHomEquiv
• mkOfUnitCounit
• leftAdjointOfEquiv / rightAdjointOfEquiv construct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.
• adjunctionOfEquivLeft / adjunctionOfEquivRight witness that these constructions give adjunctions.

There are also typeclasses IsLeftAdjoint / IsRightAdjoint, which asserts the existence of a adjoint functor. Given [F.IsLeftAdjoint], a chosen right adjoint can be obtained as F.rightAdjoint.

Adjunction.comp composes adjunctions.

toEquivalence upgrades an adjunction to an equivalence, given witnesses that the unit and counit are pointwise isomorphisms. Conversely Equivalence.toAdjunction recovers the underlying adjunction from an equivalence.

structure CategoryTheory.Adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) : Type (max (max (max u₁ u₂) v₁) v₂)

F ⊣ G represents the data of an adjunction between two functors F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.

To construct an adjunction between two functors, it's often easier to instead use the constructors mkOfHomEquiv or mkOfUnitCounit. To construct a left adjoint, there are also constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as well as their duals) which can be simpler in practice.

Uniqueness of adjoints is shown in CategoryTheory.Adjunction.Opposites.

See .

• homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)

  The equivalence between Hom (F X) Y and Hom X (G Y) coming from an adjunction

• unit : CategoryTheory.Functor.id C ⟶ F.comp G

  The unit of an adjunction

• counit : G.comp F ⟶ CategoryTheory.Functor.id D

  The counit of an adjunction

• homEquiv_unit : ∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, (self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)

  Naturality of the unit of an adjunction

• homEquiv_counit : ∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, (self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)

  Naturality of the counit of an adjunction

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F ⊣ G) {X : C} {Y : D} {f : F.obj X ⟶ Y} : (self.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (self.unit.app X) (G.map f)

Naturality of the unit of an adjunction

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : F ⊣ G) {X : C} {Y : D} {g : X ⟶ G.obj Y} : (self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)

Naturality of the counit of an adjunction

def CategoryTheory.«term_⊣_» : Lean.TrailingParserDescr

The notation F ⊣ G stands for Adjunction F G representing that F is left adjoint to G

Equations

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

class CategoryTheory.Functor.IsLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (left : CategoryTheory.Functor C D) : Prop

A class asserting the existence of a right adjoint.

• exists_rightAdjoint : ∃ (right : CategoryTheory.Functor D C), Nonempty (left ⊣ right)

theorem CategoryTheory.Functor.IsLeftAdjoint.exists_rightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {left : CategoryTheory.Functor C D} [self : left.IsLeftAdjoint] : ∃ (right : CategoryTheory.Functor D C), Nonempty (left ⊣ right)

class CategoryTheory.Functor.IsRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (right : CategoryTheory.Functor D C) : Prop

A class asserting the existence of a left adjoint.

• exists_leftAdjoint : ∃ (left : CategoryTheory.Functor C D), Nonempty (left ⊣ right)

theorem CategoryTheory.Functor.IsRightAdjoint.exists_leftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {right : CategoryTheory.Functor D C} [self : right.IsRightAdjoint] : ∃ (left : CategoryTheory.Functor C D), Nonempty (left ⊣ right)

noncomputable def CategoryTheory.Functor.leftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [R.IsRightAdjoint] : CategoryTheory.Functor C D

A chosen left adjoint to a functor that is a right adjoint.

Equations

• R.leftAdjoint = ⋯.choose

noncomputable def CategoryTheory.Functor.rightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLeftAdjoint] : CategoryTheory.Functor D C

A chosen right adjoint to a functor that is a left adjoint.

Equations

• L.rightAdjoint = ⋯.choose

noncomputable def CategoryTheory.Adjunction.ofIsLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (left : CategoryTheory.Functor C D) [left.IsLeftAdjoint] : left ⊣ left.rightAdjoint

The adjunction associated to a functor known to be a left adjoint.

Equations

• CategoryTheory.Adjunction.ofIsLeftAdjoint left = ⋯.some

noncomputable def CategoryTheory.Adjunction.ofIsRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (right : CategoryTheory.Functor C D) [right.IsRightAdjoint] : right.leftAdjoint ⊣ right

The adjunction associated to a functor known to be a right adjoint.

Equations

• CategoryTheory.Adjunction.ofIsRightAdjoint right = ⋯.some

theorem CategoryTheory.Adjunction.isLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : F.IsLeftAdjoint

theorem CategoryTheory.Adjunction.isRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : G.IsRightAdjoint

theorem CategoryTheory.Adjunction.homEquiv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) : (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) = adj.unit.app X

theorem CategoryTheory.Adjunction.homEquiv_symm_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D) : (adj.homEquiv (G.obj X) X).symm (CategoryTheory.CategoryStruct.id (G.obj X)) = adj.counit.app X

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_naturality_left_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' : C} {X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y) : (adj.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_naturality_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' : C} {X : C} {Y : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y) : (adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_naturality_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y : D} {Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y') : (adj.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (G.map g)

@[simp]

theorem CategoryTheory.Adjunction.homEquiv_naturality_right_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y : D} {Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') : (adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g

@[simp]

theorem CategoryTheory.Adjunction.left_triangle {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight adj.unit F) (CategoryTheory.whiskerLeft F adj.counit) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).comp F)

@[simp]

theorem CategoryTheory.Adjunction.right_triangle {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G adj.unit) (CategoryTheory.whiskerRight adj.counit G) = CategoryTheory.CategoryStruct.id (G.comp (CategoryTheory.Functor.id C))

@[simp]

theorem CategoryTheory.Adjunction.left_triangle_components_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj X)) h) = h

@[simp]

theorem CategoryTheory.Adjunction.left_triangle_components {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) : CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (adj.counit.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Adjunction.right_triangle_components_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (Y : D) {Z : C} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (CategoryTheory.CategoryStruct.comp (G.map (adj.counit.app Y)) h) = h

@[simp]

theorem CategoryTheory.Adjunction.right_triangle_components {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (Y : D) : CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (G.map (adj.counit.app Y)) = CategoryTheory.CategoryStruct.id (G.obj Y)

@[simp]

theorem CategoryTheory.Adjunction.counit_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : D} {Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (CategoryTheory.CategoryStruct.comp (adj.counit.app Y) h) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Adjunction.counit_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : D} {Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (adj.counit.app Y) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) f

@[simp]

theorem CategoryTheory.Adjunction.unit_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : G.obj (F.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (adj.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (F.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (adj.unit.app Y) h)

@[simp]

theorem CategoryTheory.Adjunction.unit_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) = CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)

theorem CategoryTheory.Adjunction.homEquiv_apply_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) : (adj.homEquiv A B) f = g ↔ f = (adj.homEquiv A B).symm g

theorem CategoryTheory.Adjunction.eq_homEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) : g = (adj.homEquiv A B) f ↔ (adj.homEquiv A B).symm g = f

structure CategoryTheory.Adjunction.CoreHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) : Type (max (max (max u₁ u₂) v₁) v₂)

This is an auxiliary data structure useful for constructing adjunctions. See Adjunction.mkOfHomEquiv. This structure won't typically be used anywhere else.

• homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)

  The equivalence between Hom (F X) Y and Hom X (G Y)

• homEquiv_naturality_left_symm : ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y), (self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)

  The property that describes how homEquiv.symm transforms compositions X' ⟶ X ⟶ G Y

• homEquiv_naturality_right : ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)

  The property that describes how homEquiv transforms compositions F X ⟶ Y ⟶ Y'

@[simp]

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' : C} {X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y) : (self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)

The property that describes how homEquiv.symm transforms compositions X' ⟶ X ⟶ G Y

@[simp]

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreHomEquiv F G) {X : C} {Y : D} {Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y') : (self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)

The property that describes how homEquiv transforms compositions F X ⟶ Y ⟶ Y'

@[simp]

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_aux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' : C} {X : C} {Y : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' (F.obj X)) (F.map f)) (G.map g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X' : C} {X : C} {Y : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y) : (adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)

@[simp]

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm_aux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X : C} {Y : D} {Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv (G.obj Y) Y').symm (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g

theorem CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) {X : C} {Y : D} {Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') : (adj.homEquiv X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y).symm f) g

structure CategoryTheory.Adjunction.CoreUnitCounit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) : Type (max (max (max u₁ u₂) v₁) v₂)

This is an auxiliary data structure useful for constructing adjunctions. See Adjunction.mkOfUnitCounit. This structure won't typically be used anywhere else.

• unit : CategoryTheory.Functor.id C ⟶ F.comp G

  The unit of an adjunction between F and G

• counit : G.comp F ⟶ CategoryTheory.Functor.id D

  The counit of an adjunction between F and Gs

• left_triangle : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight self.unit F) (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (CategoryTheory.whiskerLeft F self.counit)) = CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)

  Equality of the composition of the unit, associator, and counit with the identity F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F

• right_triangle : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G self.unit) (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.whiskerRight self.counit G)) = CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))

  Equality of the composition of the unit, associator, and counit with the identity G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G

@[simp]

theorem CategoryTheory.Adjunction.CoreUnitCounit.left_triangle {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreUnitCounit F G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight self.unit F) (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (CategoryTheory.whiskerLeft F self.counit)) = CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)

Equality of the composition of the unit, associator, and counit with the identity F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F

@[simp]

theorem CategoryTheory.Adjunction.CoreUnitCounit.right_triangle {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (self : CategoryTheory.Adjunction.CoreUnitCounit F G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G self.unit) (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.whiskerRight self.counit G)) = CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))

Equality of the composition of the unit, associator, and counit with the identity G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G

@[simp]

theorem CategoryTheory.Adjunction.mkOfHomEquiv_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) (Y : D) : (CategoryTheory.Adjunction.mkOfHomEquiv adj).counit.app Y = (adj.homEquiv (G.obj Y) ((CategoryTheory.Functor.id D).obj Y)).invFun (CategoryTheory.CategoryStruct.id (G.obj Y))

@[simp]

theorem CategoryTheory.Adjunction.mkOfHomEquiv_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) (X : C) : (CategoryTheory.Adjunction.mkOfHomEquiv adj).unit.app X = (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))

@[simp]

theorem CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) (X : C) (Y : D) : (CategoryTheory.Adjunction.mkOfHomEquiv adj).homEquiv X Y = adj.homEquiv X Y

def CategoryTheory.Adjunction.mkOfHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G) : F ⊣ G

Construct an adjunction between F and G out of a natural bijection between each F.obj X ⟶ Y and X ⟶ G.obj Y.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreUnitCounit F G) (X : C) (Y : D) (g : X ⟶ G.obj Y) : ((CategoryTheory.Adjunction.mkOfUnitCounit adj).homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)

@[simp]

theorem CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreUnitCounit F G) (X : C) (Y : D) (f : F.obj X ⟶ Y) : ((CategoryTheory.Adjunction.mkOfUnitCounit adj).homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)

@[simp]

theorem CategoryTheory.Adjunction.mkOfUnitCounit_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreUnitCounit F G) : (CategoryTheory.Adjunction.mkOfUnitCounit adj).unit = adj.unit

@[simp]

theorem CategoryTheory.Adjunction.mkOfUnitCounit_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreUnitCounit F G) : (CategoryTheory.Adjunction.mkOfUnitCounit adj).counit = adj.counit

def CategoryTheory.Adjunction.mkOfUnitCounit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreUnitCounit F G) : F ⊣ G

Construct an adjunction between functors F and G given a unit and counit for the adjunction satisfying the triangle identities.

Equations

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

def CategoryTheory.Adjunction.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor.id C ⊣ CategoryTheory.Functor.id C

The adjunction between the identity functor on a category and itself.

Equations

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

instance CategoryTheory.Adjunction.instInhabitedId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (CategoryTheory.Functor.id C ⊣ CategoryTheory.Functor.id C)

Equations

• CategoryTheory.Adjunction.instInhabitedId = { default := CategoryTheory.Adjunction.id }

@[simp]

theorem CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (g : F'.obj X ⟶ Y) : (CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp (iso.hom.app X) g

@[simp]

theorem CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) : (CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso) f = CategoryTheory.CategoryStruct.comp (iso.inv.app X) f

def CategoryTheory.Adjunction.equivHomsetLeftOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} : (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y)

If F and G are naturally isomorphic functors, establish an equivalence of hom-sets.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.equivHomsetRightOfNatIso_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (iso : G ≅ G') {X : C} {Y : D} (f : X ⟶ G.obj Y) : (CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso) f = CategoryTheory.CategoryStruct.comp f (iso.hom.app Y)

@[simp]

theorem CategoryTheory.Adjunction.equivHomsetRightOfNatIso_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (iso : G ≅ G') {X : C} {Y : D} (g : X ⟶ G'.obj Y) : (CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp g (iso.inv.app Y)

def CategoryTheory.Adjunction.equivHomsetRightOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (iso : G ≅ G') {X : C} {Y : D} : (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y)

If G and H are naturally isomorphic functors, establish an equivalence of hom-sets.

Equations

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

def CategoryTheory.Adjunction.ofNatIsoLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G) : G ⊣ H

Transport an adjunction along a natural isomorphism on the left.

Equations

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

def CategoryTheory.Adjunction.ofNatIsoRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D C} (adj : F ⊣ G) (iso : G ≅ H) : F ⊣ H

Transport an adjunction along a natural isomorphism on the right.

Equations

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

def CategoryTheory.Adjunction.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F.comp H ⊣ I.comp G

Composition of adjunctions.

See .

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) {X : C} {X' : C} (f : X ⟶ X') : (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).map f = (e X (F_obj X')).symm (CategoryTheory.CategoryStruct.comp f ((e X' (F_obj X')) (CategoryTheory.CategoryStruct.id (F_obj X'))))

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointOfEquiv_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) : ∀ (a : C), (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a = F_obj a

def CategoryTheory.Adjunction.leftAdjointOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) : CategoryTheory.Functor C D

Construct a left adjoint functor to G, given the functor's value on objects F_obj and a bijection e between F_obj X ⟶ Y and X ⟶ G.obj Y satisfying a naturality law he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g. Dual to rightAdjointOfEquiv.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (X : C) : (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).unit.app X = (e X (F_obj X)) (CategoryTheory.CategoryStruct.id (F_obj X))

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (X : C) (Y : D) : (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).homEquiv X Y = e X Y

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivLeft_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (Y : D) : (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).counit.app Y = (e (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))

def CategoryTheory.Adjunction.adjunctionOfEquivLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) : CategoryTheory.Adjunction.leftAdjointOfEquiv e he ⊣ G

Show that the functor given by leftAdjointOfEquiv is indeed left adjoint to G. Dual to adjunctionOfRightEquiv.

Equations

• CategoryTheory.Adjunction.adjunctionOfEquivLeft e he = CategoryTheory.Adjunction.mkOfHomEquiv { homEquiv := e, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) {Y : D} {Y' : D} (g : Y ⟶ Y') : (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).map g = (e (G_obj Y) Y') (CategoryTheory.CategoryStruct.comp ((e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))) g)

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointOfEquiv_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) : ∀ (a : D), (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a = G_obj a

def CategoryTheory.Adjunction.rightAdjointOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) : CategoryTheory.Functor D C

Construct a right adjoint functor to F, given the functor's value on objects G_obj and a bijection e between F.obj X ⟶ Y and X ⟶ G_obj Y satisfying a naturality law he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g. Dual to leftAdjointOfEquiv.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (Y : D) : (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).counit.app Y = (e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (X : C) (Y : D) : (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).homEquiv X Y = e X Y

@[simp]

theorem CategoryTheory.Adjunction.adjunctionOfEquivRight_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (X : C) : (CategoryTheory.Adjunction.adjunctionOfEquivRight e he).unit.app X = (e X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))

def CategoryTheory.Adjunction.adjunctionOfEquivRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) : F ⊣ CategoryTheory.Adjunction.rightAdjointOfEquiv e he

Show that the functor given by rightAdjointOfEquiv is indeed right adjoint to F. Dual to adjunctionOfEquivRight.

Equations

• CategoryTheory.Adjunction.adjunctionOfEquivRight e he = CategoryTheory.Adjunction.mkOfHomEquiv { homEquiv := e, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_counitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D) : adj.toEquivalence.counitIso.hom.app X = adj.counit.app X

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D) : adj.toEquivalence.counitIso.inv.app X = CategoryTheory.inv (adj.counit.app X)

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] : adj.toEquivalence.functor = F

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_unitIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C) : adj.toEquivalence.unitIso.hom.app X = adj.unit.app X

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] : adj.toEquivalence.inverse = G

@[simp]

theorem CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : C) : adj.toEquivalence.unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)

noncomputable def CategoryTheory.Adjunction.toEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] : C ≌ D

If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the adjunction to an equivalence.

Equations

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

theorem CategoryTheory.Functor.isEquivalence_of_isRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [G.IsRightAdjoint] [∀ (X : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).unit.app X)] [∀ (Y : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).counit.app Y)] : G.IsEquivalence

If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise) isomorphisms, then the functor is an equivalence of categories.

@[simp]

theorem CategoryTheory.Equivalence.toAdjunction_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.toAdjunction.unit = e.unit

@[simp]

theorem CategoryTheory.Equivalence.toAdjunction_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.toAdjunction.counit = e.counit

def CategoryTheory.Equivalence.toAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.functor ⊣ e.inverse

The adjunction given by an equivalence of categories. (To obtain the opposite adjunction, simply use e.symm.toAdjunction.

Equations

• e.toAdjunction = CategoryTheory.Adjunction.mkOfUnitCounit { unit := e.unit, counit := e.counit, left_triangle := ⋯, right_triangle := ⋯ }

theorem CategoryTheory.Equivalence.isLeftAdjoint_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.functor.IsLeftAdjoint

theorem CategoryTheory.Equivalence.isRightAdjoint_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.inverse.IsRightAdjoint

theorem CategoryTheory.Equivalence.isLeftAdjoint_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.inverse.IsLeftAdjoint

theorem CategoryTheory.Equivalence.isRightAdjoint_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.functor.IsRightAdjoint

instance CategoryTheory.Functor.isLeftAdjoint_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsLeftAdjoint] [G.IsLeftAdjoint] : (F.comp G).IsLeftAdjoint

If F and G are left adjoints then F ⋙ G is a left adjoint too.

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.isRightAdjoint_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.IsRightAdjoint] [G.IsRightAdjoint] : (F.comp G).IsRightAdjoint

If F and G are right adjoints then F ⋙ G is a right adjoint too.

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.isRightAdjoint_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [F.IsRightAdjoint] : G.IsRightAdjoint

Transport being a right adjoint along a natural isomorphism.

theorem CategoryTheory.Functor.isLeftAdjoint_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [F.IsLeftAdjoint] : G.IsLeftAdjoint

Transport being a left adjoint along a natural isomorphism.

noncomputable def CategoryTheory.Functor.adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [E.IsEquivalence] : E ⊣ E.inv

An equivalence E is left adjoint to its inverse.

Equations

• E.adjunction = E.asEquivalence.toAdjunction

@[instance 10]

instance CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.IsEquivalence] : F.IsLeftAdjoint

If F is an equivalence, it's a left adjoint.

Equations

• ⋯ = ⋯

@[instance 10]

instance CategoryTheory.Functor.isRightAdjoint_of_isEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.IsEquivalence] : F.IsRightAdjoint

If F is an equivalence, it's a right adjoint.

Equations

• ⋯ = ⋯