mathlib3 documentation

category_theory.adjunction.basic

Adjunctions between functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

There are also typeclasses is_left_adjoint / is_right_adjoint, carrying data witnessing that a given functor is a left or right adjoint. Given [is_left_adjoint F], a right adjoint of F can be constructed as right_adjoint F.

adjunction.comp composes adjunctions.

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

structure category_theory.adjunction {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) :
Type (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 mk_of_hom_equiv or mk_of_unit_counit. To construct a left adjoint, there are also constructors left_adjoint_of_equiv and adjunction_of_equiv_left (as well as their duals) which can be simpler in practice.

Uniqueness of adjoints is shown in category_theory.adjunction.opposites.

See https://stacks.math.columbia.edu/tag/0037.

Instances for category_theory.adjunction
@[class]
structure category_theory.is_left_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (left : C D) :
Type (max u₁ u₂ v₁ v₂)

A class giving a chosen right adjoint to the functor left.

Instances of this typeclass
Instances of other typeclasses for category_theory.is_left_adjoint
  • category_theory.is_left_adjoint.has_sizeof_inst
@[class]
structure category_theory.is_right_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (right : D C) :
Type (max u₁ u₂ v₁ v₂)

A class giving a chosen left adjoint to the functor right.

Instances of this typeclass
Instances of other typeclasses for category_theory.is_right_adjoint
  • category_theory.is_right_adjoint.has_sizeof_inst

Extract the left adjoint from the instance giving the chosen adjoint.

Equations

Extract the right adjoint from the instance giving the chosen adjoint.

Equations

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

Equations
@[simp]
theorem category_theory.adjunction.hom_equiv_unit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (self : F G) {X : C} {Y : D} {f : F.obj X Y} :
(self.hom_equiv X Y) f = self.unit.app X G.map f
@[simp]
theorem category_theory.adjunction.hom_equiv_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (self : F G) {X : C} {Y : D} {g : X G.obj Y} :
((self.hom_equiv X Y).symm) g = F.map g self.counit.app Y
theorem category_theory.adjunction.hom_equiv_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) (X : C) :
(adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X)) = adj.unit.app X
theorem category_theory.adjunction.hom_equiv_symm_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) (X : D) :
((adj.hom_equiv (G.obj X) X).symm) (𝟙 (G.obj X)) = adj.counit.app X
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_left_symm {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
((adj.hom_equiv X' Y).symm) (f g) = F.map f ((adj.hom_equiv X Y).symm) g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
(adj.hom_equiv X' Y) (F.map f g) = f (adj.hom_equiv X Y) g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X : C} {Y Y' : D} (f : F.obj X Y) (g : Y Y') :
(adj.hom_equiv X Y') (f g) = (adj.hom_equiv X Y) f G.map g
@[simp]
theorem category_theory.adjunction.hom_equiv_naturality_right_symm {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
((adj.hom_equiv X Y').symm) (f G.map g) = ((adj.hom_equiv X Y).symm) f g
@[simp]
theorem category_theory.adjunction.left_triangle_components {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X : C} :
F.map (adj.unit.app X) adj.counit.app (F.obj X) = 𝟙 (F.obj X)
@[simp]
theorem category_theory.adjunction.left_triangle_components_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X : C} {X' : D} (f' : (𝟭 D).obj (F.obj X) X') :
F.map (adj.unit.app X) adj.counit.app (F.obj X) f' = f'
@[simp]
theorem category_theory.adjunction.right_triangle_components {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {Y : D} :
adj.unit.app (G.obj Y) G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
@[simp]
theorem category_theory.adjunction.right_triangle_components_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {Y : D} {X' : C} (f' : G.obj ((𝟭 D).obj Y) X') :
adj.unit.app (G.obj Y) G.map (adj.counit.app Y) f' = f'
@[simp]
theorem category_theory.adjunction.counit_naturality_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : D} (f : X Y) {X' : D} (f' : (𝟭 D).obj Y X') :
F.map (G.map f) adj.counit.app Y f' = adj.counit.app X f f'
@[simp]
theorem category_theory.adjunction.counit_naturality {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : D} (f : X Y) :
F.map (G.map f) adj.counit.app Y = adj.counit.app X f
@[simp]
theorem category_theory.adjunction.unit_naturality_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : C} (f : X Y) {X' : C} (f' : G.obj (F.obj Y) X') :
adj.unit.app X G.map (F.map f) f' = f adj.unit.app Y f'
@[simp]
theorem category_theory.adjunction.unit_naturality {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : C} (f : X Y) :
adj.unit.app X G.map (F.map f) = f adj.unit.app Y
theorem category_theory.adjunction.hom_equiv_apply_eq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
(adj.hom_equiv A B) f = g f = ((adj.hom_equiv A B).symm) g
theorem category_theory.adjunction.eq_hom_equiv_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {A : C} {B : D} (f : F.obj A B) (g : A G.obj B) :
g = (adj.hom_equiv A B) f ((adj.hom_equiv A B).symm) g = f
@[nolint]
structure category_theory.adjunction.core_hom_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) :
Type (max u₁ u₂ v₁ v₂)

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

Instances for category_theory.adjunction.core_hom_equiv
  • category_theory.adjunction.core_hom_equiv.has_sizeof_inst
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (self : category_theory.adjunction.core_hom_equiv F G) {X' X : C} {Y : D} (f : X' X) (g : X G.obj Y) :
((self.hom_equiv X' Y).symm) (f g) = F.map f ((self.hom_equiv X Y).symm) g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (self : category_theory.adjunction.core_hom_equiv F G) {X : C} {Y Y' : D} (f : F.obj X Y) (g : Y Y') :
(self.hom_equiv X Y') (f g) = (self.hom_equiv X Y) f G.map g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : category_theory.adjunction.core_hom_equiv F G) {X' X : C} {Y : D} (f : X' X) (g : F.obj X Y) :
(adj.hom_equiv X' Y) (F.map f g) = f (adj.hom_equiv X Y) g
@[simp]
theorem category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right_symm {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : category_theory.adjunction.core_hom_equiv F G) {X : C} {Y Y' : D} (f : X G.obj Y) (g : Y Y') :
((adj.hom_equiv X Y').symm) (f G.map g) = ((adj.hom_equiv X Y).symm) f g
@[nolint]
structure category_theory.adjunction.core_unit_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) :
Type (max u₁ u₂ v₁ v₂)

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

Instances for category_theory.adjunction.core_unit_counit
  • category_theory.adjunction.core_unit_counit.has_sizeof_inst

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

Equations

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

Equations

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

Equations
def category_theory.adjunction.equiv_homset_left_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : 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
def category_theory.adjunction.equiv_homset_right_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G G' : 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
def category_theory.adjunction.of_nat_iso_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C D} {H : D C} (adj : F H) (iso : F G) :
G H

Transport an adjunction along an natural isomorphism on the left.

Equations
def category_theory.adjunction.of_nat_iso_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G H : D C} (adj : F G) (iso : G H) :
F H

Transport an adjunction along an natural isomorphism on the right.

Equations
def category_theory.adjunction.comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} {E : Type u₃} [ℰ : category_theory.category E] {H : D E} {I : E D} (adj₁ : F G) (adj₂ : H I) :
F H I G

Composition of adjunctions.

See https://stacks.math.columbia.edu/tag/0DV0.

Equations
@[simp]
theorem category_theory.adjunction.left_adjoint_of_equiv_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) (ᾰ : C) :
@[simp]
theorem category_theory.adjunction.left_adjoint_of_equiv_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) (X X' : C) (f : X X') :
(category_theory.adjunction.left_adjoint_of_equiv e he).map f = ((e X (F_obj X')).symm) (f (e X' (F_obj X')) (𝟙 (F_obj X')))
def category_theory.adjunction.left_adjoint_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) :
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 right_adjoint_of_equiv.

Equations
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_unit_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) (X : C) :
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_counit_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) (Y : D) :
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_left_hom_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) (X : C) (Y : D) :
def category_theory.adjunction.adjunction_of_equiv_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : 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') (h g) = (e X Y) h G.map g) :

Show that the functor given by left_adjoint_of_equiv is indeed left adjoint to G. Dual to adjunction_of_equiv_right.

Equations
def category_theory.adjunction.right_adjoint_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) :
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 left_adjoint_of_equiv.

Equations
@[simp]
theorem category_theory.adjunction.right_adjoint_of_equiv_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) (ᾰ : D) :
@[simp]
theorem category_theory.adjunction.right_adjoint_of_equiv_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) (Y Y' : D) (g : Y Y') :
(category_theory.adjunction.right_adjoint_of_equiv e he).map g = (e (G_obj Y) Y') (((e (G_obj Y) Y).symm) (𝟙 (G_obj Y)) g)
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_hom_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) (X : C) (Y : D) :
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_counit_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) (Y : D) :
def category_theory.adjunction.adjunction_of_equiv_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) :

Show that the functor given by right_adjoint_of_equiv is indeed right adjoint to F. Dual to adjunction_of_equiv_left.

Equations
@[simp]
theorem category_theory.adjunction.adjunction_of_equiv_right_unit_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : 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) (F.map f g) = f (e X Y) g) (X : C) :
@[simp]
theorem category_theory.adjunction.to_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) [ (X : C), category_theory.is_iso (adj.unit.app X)] [ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
@[simp]
theorem category_theory.adjunction.to_equivalence_functor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) [ (X : C), category_theory.is_iso (adj.unit.app X)] [ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
noncomputable def category_theory.adjunction.to_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) [ (X : C), category_theory.is_iso (adj.unit.app X)] [ (Y : D), category_theory.is_iso (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

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

Equations

An equivalence E is left adjoint to its inverse.

Equations
@[protected, instance]

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

Equations