Documentation

Mathlib.CategoryTheory.Adjunction.Basic

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:

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.

source
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.

We use the unit-counit definition of an adjunction. There is a constructor Adjunction.mk' which constructs an adjunction from the data of a hom set equivalence, a unit, and a counit, together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other.

There is also a constructor Adjunction.mkOfHomEquiv which constructs an adjunction from a natural hom set equivalence.

To construct adjoints to a given functor, there are constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as well as their duals).

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

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

Instances For
source
@[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} (self : F ⊣ G) (X : C) :
CategoryTheory.CategoryStruct.comp (F.map (self.unit.app X)) (self.counit.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)

Equality of the composition of the unit and counit with the identity F ⟶ FGF ⟶ F = 𝟙

source
@[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} (self : F ⊣ G) (Y : D) :
CategoryTheory.CategoryStruct.comp (self.unit.app (G.obj Y)) (G.map (self.counit.app Y)) = CategoryTheory.CategoryStruct.id (G.obj Y)

Equality of the composition of the unit and counit with the identity G ⟶ GFG ⟶ G = 𝟙

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

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

Equations
source
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.

Instances
source
theorem CategoryTheory.Functor.IsLeftAdjoint.exists_rightAdjoint {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {left : CategoryTheory.Functor C D} [self : left.IsLeftAdjoint], ∃ (right : CategoryTheory.Functor D C), Nonempty (left ⊣ right)
source
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.

Instances
source
theorem CategoryTheory.Functor.IsRightAdjoint.exists_leftAdjoint {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {right : CategoryTheory.Functor D C} [self : right.IsRightAdjoint], ∃ (left : CategoryTheory.Functor C D), Nonempty (left ⊣ right)
source
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
Instances For
source
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
Instances For
source
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
source
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
source
@[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} (self : F ⊣ G) (X : C) {Z : D} (h : F.obj X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (F.map (self.unit.app X)) (CategoryTheory.CategoryStruct.comp (self.counit.app (F.obj X)) h) = h
source
@[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} (self : F ⊣ G) (Y : D) {Z : C} (h : G.obj Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (self.unit.app (G.obj Y)) (CategoryTheory.CategoryStruct.comp (G.map (self.counit.app Y)) h) = h
source
@[simp]
theorem CategoryTheory.Adjunction.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) (X : C) (Y : D) (f : F.obj X ⟶ Y) :
(adj.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)
source
@[simp]
theorem CategoryTheory.Adjunction.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 : F ⊣ G) (X : C) (Y : D) (g : X ⟶ G.obj Y) :
(adj.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)
source
def CategoryTheory.Adjunction.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 : F ⊣ G) (X : C) (Y : D) :
(F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)

The hom set equivalence associated to an adjunction.

Equations
  • One or more equations did not get rendered due to their size.
source
@[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} (adj : F ⊣ G) (X : C) (Y : D) (f : F.obj X ⟶ Y) :
(adj.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)

Alias of CategoryTheory.Adjunction.homEquiv_apply.

source
@[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} (adj : F ⊣ G) (X : C) (Y : D) (g : X ⟶ G.obj Y) :
(adj.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)

Alias of CategoryTheory.Adjunction.homEquiv_symm_apply.

source
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
source
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
source
instance CategoryTheory.Adjunction.instIsLeftAdjointLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [R.IsRightAdjoint] :
R.leftAdjoint.IsLeftAdjoint
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLeftAdjoint] :
L.rightAdjoint.IsRightAdjoint
Equations
  • ⋯ = ⋯
source
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
source
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
source
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)
source
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)
source
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)
source
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
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_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} {X : C} {Y : D} {Y' : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h✝ k) {Z : C} (h : G.obj Y' ⟶ Z) :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y') g) h) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h✝) (CategoryTheory.CategoryStruct.comp (G.map k) h)
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square {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} {Y' : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k) :
CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k)
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square_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} {X : C} {Y : D} {Y' : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h✝ (G.map k)) {Z : D} (h : Y' ⟶ Z) :
CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y').symm g) h) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h✝) (CategoryTheory.CategoryStruct.comp k h)
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square {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} {Y' : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)) :
CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff {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} {Y' : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') :
CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y') g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (G.map k) ↔ CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k
source
theorem CategoryTheory.Adjunction.homEquiv_naturality_right_square_iff {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} {Y' : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y') (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') :
CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y').symm g) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y).symm h) k ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp h (G.map k)
source
@[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)
source
@[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))
source
@[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)
source
@[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
source
@[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)
source
@[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)
source
theorem CategoryTheory.Adjunction.unit_comp_map_eq_iff {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) :
CategoryTheory.CategoryStruct.comp (adj.unit.app A) (G.map f) = g ↔ f = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app B)
source
theorem CategoryTheory.Adjunction.eq_unit_comp_map_iff {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 = CategoryTheory.CategoryStruct.comp (adj.unit.app A) (G.map f) ↔ CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app B) = f
source
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
source
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
source
structure CategoryTheory.Adjunction.CoreHomEquivUnitCounit {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.mk'. 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) 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)

    The relationship between the unit and hom set equivalence 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)

    The relationship between the counit and hom set equivalence of an adjunction

source
@[simp]
theorem CategoryTheory.Adjunction.CoreHomEquivUnitCounit.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 : CategoryTheory.Adjunction.CoreHomEquivUnitCounit 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)

The relationship between the unit and hom set equivalence of an adjunction

source
@[simp]
theorem CategoryTheory.Adjunction.CoreHomEquivUnitCounit.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 : CategoryTheory.Adjunction.CoreHomEquivUnitCounit 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)

The relationship between the counit and hom set equivalence of an adjunction

source
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.

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

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

source
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)
source
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
source
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.

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

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

source
@[simp]
theorem CategoryTheory.Adjunction.mk'_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.CoreHomEquivUnitCounit F G) :
(CategoryTheory.Adjunction.mk' adj).counit = adj.counit
source
@[simp]
theorem CategoryTheory.Adjunction.mk'_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.CoreHomEquivUnitCounit F G) :
(CategoryTheory.Adjunction.mk' adj).unit = adj.unit
source
def CategoryTheory.Adjunction.mk' {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.CoreHomEquivUnitCounit F G) :
F ⊣ G

Construct an adjunction from the data of a CoreHomEquivUnitCounit, i.e. a hom set equivalence, unit and counit natural transformations together with proofs of the equalities homEquiv_unit and homEquiv_counit relating them to each other.

Equations
source
theorem CategoryTheory.Adjunction.mk'_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.CoreHomEquivUnitCounit F G) :
(CategoryTheory.Adjunction.mk' adj).homEquiv = adj.homEquiv
source
@[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) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
source
@[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))
source
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.
source
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) :
(CategoryTheory.Adjunction.mkOfHomEquiv adj).homEquiv = adj.homEquiv
source
@[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
source
@[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
source
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
source
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.
source
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 }
source
@[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
source
@[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
source
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.
source
@[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)
source
@[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)
source
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.
source
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.
source
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.
source
@[simp]
theorem CategoryTheory.Adjunction.compYonedaIso_hom_app_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 : D) (X : Cᵒᵖ) :
∀ (a : ((G.comp CategoryTheory.yoneda).obj X✝).obj X), (adj.compYonedaIso.hom.app X✝).app X a = CategoryTheory.CategoryStruct.comp (F.map a) (adj.counit.app X✝)
source
@[simp]
theorem CategoryTheory.Adjunction.compYonedaIso_inv_app_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 : D) (X : Cᵒᵖ) :
∀ (a : ((CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op)).obj X✝).obj X), (adj.compYonedaIso.inv.app X✝).app X a = CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X)) (G.map a)
source
def CategoryTheory.Adjunction.compYonedaIso {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.comp CategoryTheory.yoneda ≅ CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op)

The isomorpism which an adjunction F ⊣ G induces on G ⋙ yoneda. This states that Adjunction.homEquiv is natural in both arguments.

Equations
source
@[simp]
theorem CategoryTheory.Adjunction.compCoyonedaIso_hom_app_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ᵒᵖ) (X : D) :
∀ (a : ((F.op.comp CategoryTheory.coyoneda).obj X✝).obj X), (adj.compCoyonedaIso.hom.app X✝).app X a = CategoryTheory.CategoryStruct.comp (adj.unit.app (Opposite.unop X✝)) (G.map a)
source
@[simp]
theorem CategoryTheory.Adjunction.compCoyonedaIso_inv_app_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ᵒᵖ) (X : D) :
∀ (a : ((CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft D C (Type v₁)).obj G)).obj X✝).obj X), (adj.compCoyonedaIso.inv.app X✝).app X a = CategoryTheory.CategoryStruct.comp (F.map a) (adj.counit.app X)
source
def CategoryTheory.Adjunction.compCoyonedaIso {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.op.comp CategoryTheory.coyoneda ≅ CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft D C (Type v₁)).obj G)

The isomorpism which an adjunction F ⊣ G induces on F.op ⋙ coyoneda. This states that Adjunction.homEquiv is natural in both arguments.

Equations
source
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 https://stacks.math.columbia.edu/tag/0DV0.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem CategoryTheory.Adjunction.comp_unit_app_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} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) (X : C) {Z : C} (h : G.obj (I.obj (H.obj (F.obj X))) ⟶ Z) :
CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).unit.app X) h = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (adj₂.unit.app (F.obj X))) h)
source
@[simp]
theorem CategoryTheory.Adjunction.comp_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} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) (X : C) :
(adj₁.comp adj₂).unit.app X = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (G.map (adj₂.unit.app (F.obj X)))
source
theorem CategoryTheory.Adjunction.comp_counit_app_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} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) (X : E) {Z : E} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).counit.app X) h = CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (CategoryTheory.CategoryStruct.comp (adj₂.counit.app X) h)
source
@[simp]
theorem CategoryTheory.Adjunction.comp_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} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) (X : E) :
(adj₁.comp adj₂).counit.app X = CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (adj₂.counit.app X)
source
theorem CategoryTheory.Adjunction.comp_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} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) :
(adj₁.comp adj₂).homEquiv = fun (x : C) (x_1 : E) => (adj₂.homEquiv (F.obj x) x_1).trans (adj₁.homEquiv x (I.obj x_1))
source
@[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'))))
source
@[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
source
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.
source
@[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))
source
@[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))
source
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
source
@[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
source
@[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)
source
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.
source
@[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))
source
@[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))
source
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
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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)
source
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.
source
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.

source
@[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
source
@[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
source
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 = { unit := e.unit, counit := e.counit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
source
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
source
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
source
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
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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.

source
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.

source
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
source
@[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
  • ⋯ = ⋯
source
@[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
  • ⋯ = ⋯