category_theory.adjunction.basic

source

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₂)

hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
unit : 𝟭 C ⟶ F ⋙ G
counit : G ⋙ F ⟶ 𝟭 D
hom_equiv_unit' : (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, ⇑(self.hom_equiv X Y) f = self.unit.app X ≫ G.map f) . "obviously"
hom_equiv_counit' : (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, ⇑((self.hom_equiv X Y).symm) g = F.map g ≫ self.counit.app Y) . "obviously"

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

category_theory.adjunction.has_sizeof_inst
category_theory.adjunction.inhabited

source

@[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₂)

right : D ⥤ C
adj : left ⊣ category_theory.is_left_adjoint.right left

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

source

@[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₂)

left : C ⥤ D
adj : category_theory.is_right_adjoint.left right ⊣ right

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

source

def category_theory.left_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.is_right_adjoint R] :

C ⥤ D

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

Equations

category_theory.left_adjoint R = category_theory.is_right_adjoint.left R

source

def category_theory.right_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (L : C ⥤ D) [category_theory.is_left_adjoint L] :

D ⥤ C

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

Equations

category_theory.right_adjoint L = category_theory.is_left_adjoint.right L

source

def category_theory.adjunction.of_left_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (left : C ⥤ D) [category_theory.is_left_adjoint left] :

left ⊣ category_theory.right_adjoint left

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

Equations

category_theory.adjunction.of_left_adjoint left = category_theory.is_left_adjoint.adj

source

def category_theory.adjunction.of_right_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (right : C ⥤ D) [category_theory.is_right_adjoint right] :

category_theory.left_adjoint right ⊣ right

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

Equations

category_theory.adjunction.of_right_adjoint right = category_theory.is_right_adjoint.adj

source

@[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

source

@[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

source

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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[simp]

theorem category_theory.adjunction.left_triangle {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :

category_theory.whisker_right adj.unit F ≫ category_theory.whisker_left F adj.counit = category_theory.nat_trans.id (𝟭 C ⋙ F)

source

@[simp]

theorem category_theory.adjunction.right_triangle {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :

category_theory.whisker_left G adj.unit ≫ category_theory.whisker_right adj.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C)

source

@[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)

source

@[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'

source

@[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)

source

@[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'

source

@[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'

source

@[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

source

@[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'

source

@[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

source

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

source

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

source

@[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₂)

hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
hom_equiv_naturality_left_symm' : (∀ {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) . "obviously"
hom_equiv_naturality_right' : (∀ {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) . "obviously"

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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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₂)

unit : 𝟭 C ⟶ F ⋙ G
counit : G ⋙ F ⟶ 𝟭 D
left_triangle' : category_theory.whisker_right self.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F self.counit = category_theory.nat_trans.id (𝟭 C ⋙ F) . "obviously"
right_triangle' : category_theory.whisker_left G self.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right self.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C) . "obviously"

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

source

@[simp]

theorem category_theory.adjunction.core_unit_counit.left_triangle {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_unit_counit F G) :

category_theory.whisker_right self.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F self.counit = category_theory.nat_trans.id (𝟭 C ⋙ F)

source

@[simp]

theorem category_theory.adjunction.core_unit_counit.right_triangle {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_unit_counit F G) :

category_theory.whisker_left G self.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right self.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C)

source

@[simp]

theorem category_theory.adjunction.mk_of_hom_equiv_unit_app {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) :

(category_theory.adjunction.mk_of_hom_equiv adj).unit.app X = ⇑(adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X))

source

def category_theory.adjunction.mk_of_hom_equiv {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) :

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

category_theory.adjunction.mk_of_hom_equiv adj = {hom_equiv := adj.hom_equiv, unit := {app := λ (X : C), ⇑(adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X)), naturality' := _}, counit := {app := λ (Y : D), (adj.hom_equiv (G.obj Y) ((𝟭 D).obj Y)).inv_fun (𝟙 (G.obj Y)), naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[simp]

theorem category_theory.adjunction.mk_of_hom_equiv_hom_equiv {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 : D) :

(category_theory.adjunction.mk_of_hom_equiv adj).hom_equiv X Y = adj.hom_equiv X Y

source

@[simp]

theorem category_theory.adjunction.mk_of_hom_equiv_counit_app {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) (Y : D) :

(category_theory.adjunction.mk_of_hom_equiv adj).counit.app Y = (adj.hom_equiv (G.obj Y) ((𝟭 D).obj Y)).inv_fun (𝟙 (G.obj Y))

source

def category_theory.adjunction.mk_of_unit_counit {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_unit_counit 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

category_theory.adjunction.mk_of_unit_counit adj = {hom_equiv := λ (X : C) (Y : D), {to_fun := λ (f : F.obj X ⟶ Y), adj.unit.app X ≫ G.map f, inv_fun := λ (g : X ⟶ G.obj Y), F.map g ≫ adj.counit.app Y, left_inv := _, right_inv := _}, unit := adj.unit, counit := adj.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[simp]

theorem category_theory.adjunction.mk_of_unit_counit_hom_equiv_symm_apply {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_unit_counit F G) (X : C) (Y : D) (g : X ⟶ G.obj Y) :

⇑(((category_theory.adjunction.mk_of_unit_counit adj).hom_equiv X Y).symm) g = F.map g ≫ adj.counit.app Y

source

@[simp]

theorem category_theory.adjunction.mk_of_unit_counit_unit {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_unit_counit F G) :

(category_theory.adjunction.mk_of_unit_counit adj).unit = adj.unit

source

@[simp]

theorem category_theory.adjunction.mk_of_unit_counit_counit {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_unit_counit F G) :

(category_theory.adjunction.mk_of_unit_counit adj).counit = adj.counit

source

@[simp]

theorem category_theory.adjunction.mk_of_unit_counit_hom_equiv_apply {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_unit_counit F G) (X : C) (Y : D) (f : F.obj X ⟶ Y) :

⇑((category_theory.adjunction.mk_of_unit_counit adj).hom_equiv X Y) f = adj.unit.app X ≫ G.map f

source

def category_theory.adjunction.id {C : Type u₁} [category_theory.category C] :

𝟭 C ⊣ 𝟭 C

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

Equations

category_theory.adjunction.id = {hom_equiv := λ (X Y : C), equiv.refl ((𝟭 C).obj X ⟶ Y), unit := 𝟙 (𝟭 C), counit := 𝟙 (𝟭 C ⋙ 𝟭 C), hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[protected, instance]

def category_theory.adjunction.inhabited {C : Type u₁} [category_theory.category C] :

inhabited (𝟭 C ⊣ 𝟭 C)

Equations

category_theory.adjunction.inhabited = {default := category_theory.adjunction.id _inst_1}

source

@[simp]

theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_symm_apply {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} (g : F'.obj X ⟶ Y) :

⇑((category_theory.adjunction.equiv_homset_left_of_nat_iso iso).symm) g = iso.hom.app X ≫ g

source

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

category_theory.adjunction.equiv_homset_left_of_nat_iso iso = {to_fun := λ (f : F.obj X ⟶ Y), iso.inv.app X ≫ f, inv_fun := λ (g : F'.obj X ⟶ Y), iso.hom.app X ≫ g, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.adjunction.equiv_homset_left_of_nat_iso_apply {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 : F.obj X ⟶ Y) :

⇑(category_theory.adjunction.equiv_homset_left_of_nat_iso iso) f = iso.inv.app X ≫ f

source

@[simp]

theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_apply {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} (f : X ⟶ G.obj Y) :

⇑(category_theory.adjunction.equiv_homset_right_of_nat_iso iso) f = f ≫ iso.hom.app Y

source

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

category_theory.adjunction.equiv_homset_right_of_nat_iso iso = {to_fun := λ (f : X ⟶ G.obj Y), f ≫ iso.hom.app Y, inv_fun := λ (g : X ⟶ G'.obj Y), g ≫ iso.inv.app Y, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.adjunction.equiv_homset_right_of_nat_iso_symm_apply {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} (g : X ⟶ G'.obj Y) :

⇑((category_theory.adjunction.equiv_homset_right_of_nat_iso iso).symm) g = g ≫ iso.inv.app Y

source

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

adj.of_nat_iso_left iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (category_theory.adjunction.equiv_homset_left_of_nat_iso iso.symm).trans (adj.hom_equiv X Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

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

adj.of_nat_iso_right iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (adj.hom_equiv X Y).trans (category_theory.adjunction.equiv_homset_right_of_nat_iso iso), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

def category_theory.adjunction.right_adjoint_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [r : category_theory.is_right_adjoint F] :

category_theory.is_right_adjoint G

Transport being a right adjoint along a natural isomorphism.

Equations

category_theory.adjunction.right_adjoint_of_nat_iso h = {left := category_theory.is_right_adjoint.left F r, adj := category_theory.is_right_adjoint.adj.of_nat_iso_right h}

source

def category_theory.adjunction.left_adjoint_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [r : category_theory.is_left_adjoint F] :

category_theory.is_left_adjoint G

Transport being a left adjoint along a natural isomorphism.

Equations

category_theory.adjunction.left_adjoint_of_nat_iso h = {right := category_theory.is_left_adjoint.right F r, adj := category_theory.is_left_adjoint.adj.of_nat_iso_left h}

source

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

adj₁.comp adj₂ = {hom_equiv := λ (X : C) (Z : E), (adj₂.hom_equiv (F.obj X) Z).trans (adj₁.hom_equiv X (I.obj Z)), unit := adj₁.unit ≫ category_theory.whisker_left F (category_theory.whisker_right adj₂.unit G) ≫ (F.associator (H ⋙ I) G).inv, counit := (I.associator G (F ⋙ H)).hom ≫ category_theory.whisker_left I (category_theory.whisker_right adj₁.counit H) ≫ adj₂.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[protected, instance]

def category_theory.adjunction.left_adjoint_of_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [Fl : category_theory.is_left_adjoint F] [Gl : category_theory.is_left_adjoint G] :

category_theory.is_left_adjoint (F ⋙ G)

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

Equations

category_theory.adjunction.left_adjoint_of_comp F G = {right := category_theory.is_left_adjoint.right G ⋙ category_theory.is_left_adjoint.right F, adj := category_theory.is_left_adjoint.adj.comp category_theory.is_left_adjoint.adj}

source

@[protected, instance]

def category_theory.adjunction.right_adjoint_of_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] {F : C ⥤ D} {G : D ⥤ E} [Fr : category_theory.is_right_adjoint F] [Gr : category_theory.is_right_adjoint G] :

category_theory.is_right_adjoint (F ⋙ G)

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

Equations

category_theory.adjunction.right_adjoint_of_comp = {left := category_theory.is_right_adjoint.left G ⋙ category_theory.is_right_adjoint.left F, adj := category_theory.is_right_adjoint.adj.comp category_theory.is_right_adjoint.adj}

source

@[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) :

(category_theory.adjunction.left_adjoint_of_equiv e he).obj ᾰ = F_obj ᾰ

source

@[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')))

source

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

category_theory.adjunction.left_adjoint_of_equiv e he = {obj := F_obj, map := λ (X X' : C) (f : X ⟶ X'), ⇑((e X (F_obj X')).symm) (f ≫ ⇑(e X' (F_obj X')) (𝟙 (F_obj X'))), map_id' := _, map_comp' := _}

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_left e he).unit.app X = ⇑(e X (F_obj X)) (𝟙 (F_obj X))

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_left e he).counit.app Y = ⇑((e (G.obj Y) Y).symm) (𝟙 (G.obj Y))

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_left e he).hom_equiv X Y = e X Y

source

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) :

category_theory.adjunction.left_adjoint_of_equiv e he ⊣ G

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

Equations

category_theory.adjunction.adjunction_of_equiv_left e he = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := e, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

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

category_theory.adjunction.right_adjoint_of_equiv e he = {obj := G_obj, map := λ (Y Y' : D) (g : Y ⟶ Y'), ⇑(e (G_obj Y) Y') (⇑((e (G_obj Y) Y).symm) (𝟙 (G_obj Y)) ≫ g), map_id' := _, map_comp' := _}

source

@[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) :

(category_theory.adjunction.right_adjoint_of_equiv e he).obj ᾰ = G_obj ᾰ

source

@[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)

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_right e he).hom_equiv X Y = e X Y

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_right e he).counit.app Y = ⇑((e (G_obj Y) Y).symm) (𝟙 (G_obj Y))

source

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) :

F ⊣ category_theory.adjunction.right_adjoint_of_equiv e he

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

Equations

category_theory.adjunction.adjunction_of_equiv_right e he = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := e, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

@[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) :

(category_theory.adjunction.adjunction_of_equiv_right e he).unit.app X = ⇑(e X (F.obj X)) (𝟙 (F.obj X))

source

@[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)] :

adj.to_equivalence.inverse = G

source

@[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)] :

adj.to_equivalence.functor = F

source

@[simp]

theorem category_theory.adjunction.to_equivalence_unit_iso {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)] :

adj.to_equivalence.unit_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (adj.unit.app X)) _

source

@[simp]

theorem category_theory.adjunction.to_equivalence_counit_iso {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)] :

adj.to_equivalence.counit_iso = category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (adj.counit.app Y)) _

source

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

adj.to_equivalence = {functor := F, inverse := G, unit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (adj.unit.app X)) _, counit_iso := category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (adj.counit.app Y)) _, functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_inverse {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)] [∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] :

category_theory.is_equivalence.inverse G = category_theory.left_adjoint G

source

@[simp]

theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)] [∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] (X : C) :

category_theory.is_equivalence.counit_iso.hom.app X = category_theory.inv ((category_theory.adjunction.of_right_adjoint G).unit.app X)

source

@[simp]

theorem category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)] [∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] (X : C) :

category_theory.is_equivalence.counit_iso.inv.app X = (category_theory.adjunction.of_right_adjoint G).unit.app X

source

noncomputable def category_theory.adjunction.is_right_adjoint_to_is_equivalence {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : D ⥤ C} [category_theory.is_right_adjoint G] [∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)] [∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] :

category_theory.is_equivalence G

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.

Equations