Adjunctions between functors #
F ⊣ G
represents the data of an adjunction between two functors
F : C ⥤ D
and G : D ⥤ C
. F
is the left adjoint and G
is the right adjoint.
We provide various useful constructors:
mkOfHomEquiv
mkOfUnitCounit
leftAdjointOfEquiv
/rightAdjointOfEquiv
construct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.adjunctionOfEquivLeft
/adjunctionOfEquivRight
witness that these constructions give adjunctions.
There are also typeclasses IsLeftAdjoint
/ IsRightAdjoint
, which asserts the
existence of a adjoint functor. Given [F.IsLeftAdjoint]
, a chosen right
adjoint can be obtained as F.rightAdjoint
.
Adjunction.comp
composes adjunctions.
toEquivalence
upgrades an adjunction to an equivalence,
given witnesses that the unit and counit are pointwise isomorphisms.
Conversely Equivalence.toAdjunction
recovers the underlying adjunction from an equivalence.
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.
- 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
- left_triangle_components : ∀ (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 = 𝟙
- right_triangle_components : ∀ (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 = 𝟙
Instances For
Equality of the composition of the unit and counit with the identity F ⟶ FGF ⟶ F = 𝟙
Equality of the composition of the unit and counit with the identity G ⟶ GFG ⟶ G = 𝟙
The notation F ⊣ G
stands for Adjunction F G
representing that F
is left adjoint to G
Equations
- CategoryTheory.«term_⊣_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_⊣_ 15 15 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊣ ") (Lean.ParserDescr.cat `term 16))
Instances For
A class asserting the existence of a right adjoint.
- exists_rightAdjoint : ∃ (right : CategoryTheory.Functor D C), Nonempty (left ⊣ right)
Instances
A class asserting the existence of a left adjoint.
- exists_leftAdjoint : ∃ (left : CategoryTheory.Functor C D), Nonempty (left ⊣ right)
Instances
A chosen left adjoint to a functor that is a right adjoint.
Equations
- R.leftAdjoint = ⋯.choose
Instances For
A chosen right adjoint to a functor that is a left adjoint.
Equations
- L.rightAdjoint = ⋯.choose
Instances For
The adjunction associated to a functor known to be a left adjoint.
Equations
- CategoryTheory.Adjunction.ofIsLeftAdjoint left = ⋯.some
Instances For
The adjunction associated to a functor known to be a right adjoint.
Equations
- CategoryTheory.Adjunction.ofIsRightAdjoint right = ⋯.some
Instances For
The hom set equivalence associated to an adjunction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of CategoryTheory.Adjunction.homEquiv_apply
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This is an auxiliary data structure useful for constructing adjunctions.
See Adjunction.mk'
. This structure won't typically be used anywhere else.
The equivalence between
Hom (F X) Y
andHom 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
Instances For
The relationship between the unit and hom set equivalence of an adjunction
The relationship between the counit and hom set equivalence of an adjunction
This is an auxiliary data structure useful for constructing adjunctions.
See Adjunction.mkOfHomEquiv
.
This structure won't typically be used anywhere else.
The equivalence between
Hom (F X) Y
andHom X (G Y)
- homEquiv_naturality_left_symm : ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y), (self.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) ((self.homEquiv X Y).symm g)
The property that describes how
homEquiv.symm
transforms compositionsX' ⟶ X ⟶ G Y
- homEquiv_naturality_right : ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (self.homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.homEquiv X Y) f) (G.map g)
The property that describes how
homEquiv
transforms compositionsF X ⟶ Y ⟶ Y'
Instances For
The property that describes how homEquiv.symm
transforms compositions X' ⟶ X ⟶ G Y
The property that describes how homEquiv
transforms compositions F X ⟶ Y ⟶ Y'
This is an auxiliary data structure useful for constructing adjunctions.
See Adjunction.mkOfUnitCounit
.
This structure won't typically be used anywhere else.
- unit : CategoryTheory.Functor.id C ⟶ F.comp G
The unit of an adjunction between
F
andG
- counit : G.comp F ⟶ CategoryTheory.Functor.id D
The counit of an adjunction between
F
andG
s - left_triangle : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight self.unit F) (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (CategoryTheory.whiskerLeft F self.counit)) = CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)
Equality of the composition of the unit, associator, and counit with the identity
F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F
- right_triangle : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G self.unit) (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.whiskerRight self.counit G)) = CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))
Equality of the composition of the unit, associator, and counit with the identity
G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G
Instances For
Equality of the composition of the unit, associator, and counit with the identity
F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F
Equality of the composition of the unit, associator, and counit with the identity
G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id 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
- CategoryTheory.Adjunction.mk' adj = { unit := adj.unit, counit := adj.counit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
Instances For
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.
Instances For
Construct an adjunction between functors F
and G
given a unit and counit for the adjunction
satisfying the triangle identities.
Equations
- CategoryTheory.Adjunction.mkOfUnitCounit adj = { unit := adj.unit, counit := adj.counit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
Instances For
The adjunction between the identity functor on a category and itself.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.Adjunction.instInhabitedId = { default := CategoryTheory.Adjunction.id }
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.
Instances For
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.
Instances For
Transport an adjunction along a natural isomorphism on the left.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport an adjunction along a natural isomorphism on the right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The isomorpism which an adjunction F ⊣ G
induces on G ⋙ yoneda
. This states that
Adjunction.homEquiv
is natural in both arguments.
Equations
- adj.compYonedaIso = CategoryTheory.NatIso.ofComponents (fun (X : D) => CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (adj.homEquiv (Opposite.unop Y) X).toIso.symm) ⋯) ⋯
Instances For
The isomorpism which an adjunction F ⊣ G
induces on F.op ⋙ coyoneda
. This states that
Adjunction.homEquiv
is natural in both arguments.
Equations
- adj.compCoyonedaIso = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.NatIso.ofComponents (fun (Y : D) => (adj.homEquiv (Opposite.unop X) Y).toIso) ⋯) ⋯
Instances For
Composition of adjunctions.
See https://stacks.math.columbia.edu/tag/0DV0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Show that the functor given by leftAdjointOfEquiv
is indeed left adjoint to G
. Dual
to adjunctionOfRightEquiv
.
Equations
- CategoryTheory.Adjunction.adjunctionOfEquivLeft e he = CategoryTheory.Adjunction.mkOfHomEquiv { homEquiv := e, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
Instances For
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.
Instances For
Show that the functor given by rightAdjointOfEquiv
is indeed right adjoint to F
. Dual
to adjunctionOfEquivRight
.
Equations
- CategoryTheory.Adjunction.adjunctionOfEquivRight e he = CategoryTheory.Adjunction.mkOfHomEquiv { homEquiv := e, homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
Instances For
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.
Instances For
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.
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 := ⋯ }
Instances For
If F
and G
are left adjoints then F ⋙ G
is a left adjoint too.
Equations
- ⋯ = ⋯
If F
and G
are right adjoints then F ⋙ G
is a right adjoint too.
Equations
- ⋯ = ⋯
Transport being a right adjoint along a natural isomorphism.
Transport being a left adjoint along a natural isomorphism.
An equivalence E
is left adjoint to its inverse.
Equations
- E.adjunction = E.asEquivalence.toAdjunction
Instances For
If F
is an equivalence, it's a left adjoint.
Equations
- ⋯ = ⋯
If F
is an equivalence, it's a right adjoint.
Equations
- ⋯ = ⋯