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:
mkOfHomEquivmkOfUnitCounitleftAdjointOfEquiv/rightAdjointOfEquivconstruct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.adjunctionOfEquivLeft/adjunctionOfEquivRightwitness that these constructions give adjunctions.
There are also typeclasses IsLeftAdjoint / IsRightAdjoint, carrying data witnessing
that a given functor is a left or right adjoint.
Given [IsLeftAdjoint F], a right adjoint of F can be constructed as rightAdjoint F.
Adjunction.comp composes adjunctions.
toEquivalence upgrades an adjunction to an equivalence,
given witnesses that the unit and counit are pointwise isomorphisms.
Conversely Equivalence.toAdjunction recovers the underlying adjunction from an equivalence.
structure
CategoryTheory.Adjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D C)
:
Type (max (max (max u₁ u₂) v₁) v₂)
The equivalence between
Hom (F X) YandHom X (G Y)coming from an adjunction- unit : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.comp F G
The unit of an adjunction
- counit : CategoryTheory.Functor.comp G F ⟶ CategoryTheory.Functor.id D
The counit of an adjunction
- homEquiv_unit : ∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, ↑(CategoryTheory.Adjunction.homEquiv s X Y) f = CategoryTheory.CategoryStruct.comp (s.unit.app X) (G.map f)
Naturality of the unit of an adjunction
- homEquiv_counit : ∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, ↑(CategoryTheory.Adjunction.homEquiv s X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (s.counit.app Y)
Naturality of the counit of an adjunction
F ⊣ G represents the data of an adjunction between two functors
F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.
To construct an adjunction between two functors, it's often easier to instead use the
constructors mkOfHomEquiv or mkOfUnitCounit. To construct a left adjoint,
there are also constructors leftAdjointOfEquiv and adjunctionOfEquivLeft (as
well as their duals) which can be simpler in practice.
Uniqueness of adjoints is shown in CategoryTheory.Adjunction.Opposites.
See https://stacks.math.columbia.edu/tag/0037.
Instances For
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
class
CategoryTheory.IsLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(left : CategoryTheory.Functor C D)
:
Type (max (max (max u₁ u₂) v₁) v₂)
- right : CategoryTheory.Functor D C
The right adjoint to
left - adj : left ⊣ CategoryTheory.IsLeftAdjoint.right left
A class giving a chosen right adjoint to the functor left.
Instances
class
CategoryTheory.IsRightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(right : CategoryTheory.Functor D C)
:
Type (max (max (max u₁ u₂) v₁) v₂)
- left : CategoryTheory.Functor C D
The left adjoint to
right - adj : CategoryTheory.IsRightAdjoint.left right ⊣ right
A class giving a chosen left adjoint to the functor right.
Instances
def
CategoryTheory.leftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(R : CategoryTheory.Functor D C)
[CategoryTheory.IsRightAdjoint R]
:
Extract the left adjoint from the instance giving the chosen adjoint.
Instances For
def
CategoryTheory.rightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(L : CategoryTheory.Functor C D)
[CategoryTheory.IsLeftAdjoint L]
:
Extract the right adjoint from the instance giving the chosen adjoint.
Instances For
def
CategoryTheory.Adjunction.ofLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(left : CategoryTheory.Functor C D)
[CategoryTheory.IsLeftAdjoint left]
:
left ⊣ CategoryTheory.rightAdjoint left
The adjunction associated to a functor known to be a left adjoint.
Equations
- CategoryTheory.Adjunction.ofLeftAdjoint left = CategoryTheory.IsLeftAdjoint.adj
Instances For
def
CategoryTheory.Adjunction.ofRightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(right : CategoryTheory.Functor C D)
[CategoryTheory.IsRightAdjoint right]
:
CategoryTheory.leftAdjoint right ⊣ right
The adjunction associated to a functor known to be a right adjoint.
Equations
- CategoryTheory.Adjunction.ofRightAdjoint right = CategoryTheory.IsRightAdjoint.adj
Instances For
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)
:
↑(CategoryTheory.Adjunction.homEquiv adj X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) = adj.unit.app X
theorem
CategoryTheory.Adjunction.homEquiv_symm_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
(X : D)
:
↑(CategoryTheory.Adjunction.homEquiv adj (G.obj X) X).symm (CategoryTheory.CategoryStruct.id (G.obj X)) = adj.counit.app X
@[simp]
theorem
CategoryTheory.Adjunction.homEquiv_naturality_left_symm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X' : C}
{X : C}
{Y : D}
(f : X' ⟶ X)
(g : X ⟶ G.obj Y)
:
↑(CategoryTheory.Adjunction.homEquiv adj X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) (↑(CategoryTheory.Adjunction.homEquiv adj X Y).symm g)
@[simp]
theorem
CategoryTheory.Adjunction.homEquiv_naturality_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X' : C}
{X : C}
{Y : D}
(f : X' ⟶ X)
(g : F.obj X ⟶ Y)
:
↑(CategoryTheory.Adjunction.homEquiv adj X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(CategoryTheory.Adjunction.homEquiv adj X Y) g)
@[simp]
theorem
CategoryTheory.Adjunction.homEquiv_naturality_right
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
{Y : D}
{Y' : D}
(f : F.obj X ⟶ Y)
(g : Y ⟶ Y')
:
↑(CategoryTheory.Adjunction.homEquiv adj X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.homEquiv adj X Y) f) (G.map g)
@[simp]
theorem
CategoryTheory.Adjunction.homEquiv_naturality_right_symm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
{Y : D}
{Y' : D}
(f : X ⟶ G.obj Y)
(g : Y ⟶ Y')
:
↑(CategoryTheory.Adjunction.homEquiv adj X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.homEquiv adj X Y).symm f) g
@[simp]
theorem
CategoryTheory.Adjunction.left_triangle
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
:
@[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)
:
@[simp]
theorem
CategoryTheory.Adjunction.left_triangle_components_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
{Z : D}
(h : (CategoryTheory.Functor.id D).obj (F.obj X) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X))
(CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj X)) h) = h
@[simp]
theorem
CategoryTheory.Adjunction.left_triangle_components
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
:
CategoryTheory.CategoryStruct.comp (F.map (adj.unit.app X)) (adj.counit.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem
CategoryTheory.Adjunction.right_triangle_components_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{Y : D}
{Z : C}
(h : G.obj ((CategoryTheory.Functor.id D).obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y))
(CategoryTheory.CategoryStruct.comp (G.map (adj.counit.app Y)) h) = h
@[simp]
theorem
CategoryTheory.Adjunction.right_triangle_components
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{Y : D}
:
CategoryTheory.CategoryStruct.comp (adj.unit.app (G.obj Y)) (G.map (adj.counit.app Y)) = CategoryTheory.CategoryStruct.id (G.obj Y)
@[simp]
theorem
CategoryTheory.Adjunction.counit_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : D}
{Y : D}
(f : X ⟶ Y)
{Z : D}
(h : (CategoryTheory.Functor.id D).obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (CategoryTheory.CategoryStruct.comp (adj.counit.app Y) h) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) (CategoryTheory.CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.Adjunction.counit_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : D}
{Y : D}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (F.map (G.map f)) (adj.counit.app Y) = CategoryTheory.CategoryStruct.comp (adj.counit.app X) f
@[simp]
theorem
CategoryTheory.Adjunction.unit_naturality_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(h : G.obj (F.obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (adj.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (F.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (adj.unit.app Y) h)
@[simp]
theorem
CategoryTheory.Adjunction.unit_naturality
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map (F.map f)) = CategoryTheory.CategoryStruct.comp f (adj.unit.app Y)
theorem
CategoryTheory.Adjunction.homEquiv_apply_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{A : C}
{B : D}
(f : F.obj A ⟶ B)
(g : A ⟶ G.obj B)
:
↑(CategoryTheory.Adjunction.homEquiv adj A B) f = g ↔ f = ↑(CategoryTheory.Adjunction.homEquiv adj A B).symm g
theorem
CategoryTheory.Adjunction.eq_homEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
{A : C}
{B : D}
(f : F.obj A ⟶ B)
(g : A ⟶ G.obj B)
:
g = ↑(CategoryTheory.Adjunction.homEquiv adj A B) f ↔ ↑(CategoryTheory.Adjunction.homEquiv adj A B).symm g = f
structure
CategoryTheory.Adjunction.CoreHomEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D C)
:
Type (max (max (max u₁ u₂) v₁) v₂)
The equivalence between
Hom (F X) YandHom X (G Y)- homEquiv_naturality_left_symm : ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y), ↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv s X' Y).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv s X Y).symm g)
The property that describes how
homEquiv.symmtransforms compositionsX' ⟶ X ⟶ G Y - homEquiv_naturality_right : ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv s X Y') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv s X Y) f) (G.map g)
The property that describes how
homEquivtransforms compositionsF X ⟶ Y ⟶ Y'
This is an auxiliary data structure useful for constructing adjunctions.
See Adjunction.mkOfHomEquiv.
This structure won't typically be used anywhere else.
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_aux
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
{X' : C}
{X : C}
{Y : D}
(f : X' ⟶ X)
(g : F.obj X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X' (F.obj X)) (F.map f))
(G.map g) = CategoryTheory.CategoryStruct.comp f (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X Y) g)
theorem
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
{X' : C}
{X : C}
{Y : D}
(f : X' ⟶ X)
(g : F.obj X ⟶ Y)
:
↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X Y) g)
@[simp]
theorem
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm_aux
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
{X : C}
{Y : D}
{Y' : D}
(f : X ⟶ G.obj Y)
(g : Y ⟶ Y')
:
CategoryTheory.CategoryStruct.comp (F.map f)
(↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj (G.obj Y) Y').symm (G.map g)) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X Y).symm f) g
theorem
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
{X : C}
{Y : D}
{Y' : D}
(f : X ⟶ G.obj Y)
(g : Y ⟶ Y')
:
↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X Y').symm (CategoryTheory.CategoryStruct.comp f (G.map g)) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X Y).symm f) g
structure
CategoryTheory.Adjunction.CoreUnitCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D C)
:
Type (max (max (max u₁ u₂) v₁) v₂)
- unit : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.comp F G
The unit of an adjunction between
FandG - counit : CategoryTheory.Functor.comp G F ⟶ CategoryTheory.Functor.id D
The counit of an adjunction between
FandGs - left_triangle : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight s.unit F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator F G F).hom (CategoryTheory.whiskerLeft F s.counit)) = CategoryTheory.NatTrans.id (CategoryTheory.Functor.comp (CategoryTheory.Functor.id C) 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 s.unit) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator G F G).inv (CategoryTheory.whiskerRight s.counit G)) = CategoryTheory.NatTrans.id (CategoryTheory.Functor.comp G (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
This is an auxiliary data structure useful for constructing adjunctions.
See Adjunction.mkOfUnitCounit.
This structure won't typically be used anywhere else.
Instances For
@[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 = ↑(CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X))
@[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 = Equiv.invFun (CategoryTheory.Adjunction.CoreHomEquiv.homEquiv adj (G.obj Y) ((CategoryTheory.Functor.id D).obj Y))
(CategoryTheory.CategoryStruct.id (G.obj Y))
@[simp]
theorem
CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
(X : C)
(Y : D)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.mkOfUnitCounit_unit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreUnitCounit F G)
:
(CategoryTheory.Adjunction.mkOfUnitCounit adj).unit = adj.unit
@[simp]
theorem
CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreUnitCounit F G)
(X : C)
(Y : D)
(f : F.obj X ⟶ Y)
:
↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.mkOfUnitCounit adj) X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)
@[simp]
theorem
CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreUnitCounit F G)
(X : C)
(Y : D)
(g : X ⟶ G.obj Y)
:
↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.mkOfUnitCounit adj) X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)
@[simp]
theorem
CategoryTheory.Adjunction.mkOfUnitCounit_counit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreUnitCounit F G)
:
(CategoryTheory.Adjunction.mkOfUnitCounit adj).counit = adj.counit
def
CategoryTheory.Adjunction.mkOfUnitCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : CategoryTheory.Adjunction.CoreUnitCounit F G)
:
F ⊣ G
Construct an adjunction between functors F and G given a unit and counit for the adjunction
satisfying the triangle identities.
Equations
- One or more equations did not get rendered due to their size.
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
instance
CategoryTheory.Adjunction.instInhabitedAdjunctionId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- CategoryTheory.Adjunction.instInhabitedAdjunctionId = { default := CategoryTheory.Adjunction.id }
@[simp]
theorem
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
(iso : F ≅ F')
{X : C}
{Y : D}
(g : F'.obj X ⟶ Y)
:
↑(CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp (iso.hom.app X) g
@[simp]
theorem
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
(iso : F ≅ F')
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
:
↑(CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso) f = CategoryTheory.CategoryStruct.comp (iso.inv.app X) f
def
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
(iso : F ≅ F')
{X : C}
{Y : D}
:
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
@[simp]
theorem
CategoryTheory.Adjunction.equivHomsetRightOfNatIso_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{G' : CategoryTheory.Functor D C}
(iso : G ≅ G')
{X : C}
{Y : D}
(f : X ⟶ G.obj Y)
:
↑(CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso) f = CategoryTheory.CategoryStruct.comp f (iso.hom.app Y)
@[simp]
theorem
CategoryTheory.Adjunction.equivHomsetRightOfNatIso_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{G' : CategoryTheory.Functor D C}
(iso : G ≅ G')
{X : C}
{Y : D}
(g : X ⟶ G'.obj Y)
:
↑(CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp g (iso.inv.app Y)
def
CategoryTheory.Adjunction.equivHomsetRightOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{G' : CategoryTheory.Functor D C}
(iso : G ≅ G')
{X : C}
{Y : D}
:
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
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.
Instances For
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.
Instances For
def
CategoryTheory.Adjunction.rightAdjointOfNatIso
{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)
[r : CategoryTheory.IsRightAdjoint F]
:
Transport being a right adjoint along a natural isomorphism.
Equations
- CategoryTheory.Adjunction.rightAdjointOfNatIso h = { left := CategoryTheory.IsRightAdjoint.left F, adj := CategoryTheory.Adjunction.ofNatIsoRight CategoryTheory.IsRightAdjoint.adj h }
Instances For
def
CategoryTheory.Adjunction.leftAdjointOfNatIso
{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)
[r : CategoryTheory.IsLeftAdjoint F]
:
Transport being a left adjoint along a natural isomorphism.
Equations
- CategoryTheory.Adjunction.leftAdjointOfNatIso h = { right := CategoryTheory.IsLeftAdjoint.right F, adj := CategoryTheory.Adjunction.ofNatIsoLeft CategoryTheory.IsLeftAdjoint.adj h }
Instances For
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)
:
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
instance
CategoryTheory.Adjunction.leftAdjointOfComp
{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)
[Fl : CategoryTheory.IsLeftAdjoint F]
[Gl : CategoryTheory.IsLeftAdjoint G]
:
If F and G are left adjoints then F ⋙ G is a left adjoint too.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Adjunction.rightAdjointOfComp
{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}
[Fr : CategoryTheory.IsRightAdjoint F]
[Gr : CategoryTheory.IsRightAdjoint G]
:
If F and G are right adjoints then F ⋙ G is a right adjoint too.
Equations
- One or more equations did not get rendered due to their size.
@[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
@[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'))))
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))
:
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
@[simp]
theorem
CategoryTheory.Adjunction.adjunctionOfEquivLeft_homEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{F_obj : C → D}
(e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
↑(e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp (↑(e X Y) h) (G.map g))
(X : C)
(Y : D)
:
@[simp]
theorem
CategoryTheory.Adjunction.adjunctionOfEquivLeft_unit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{F_obj : C → D}
(e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
↑(e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp (↑(e X Y) h) (G.map g))
(X : C)
:
(CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).unit.app X = ↑(e X (F_obj X)) (CategoryTheory.CategoryStruct.id (F_obj X))
@[simp]
theorem
CategoryTheory.Adjunction.adjunctionOfEquivLeft_counit_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{F_obj : C → D}
(e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
↑(e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp (↑(e X Y) h) (G.map g))
(Y : D)
:
(CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).counit.app Y = ↑(e (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
def
CategoryTheory.Adjunction.adjunctionOfEquivLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
{F_obj : C → D}
(e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
↑(e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp (↑(e X Y) h) (G.map g))
:
Show that the functor given by leftAdjointOfEquiv is indeed left adjoint to G. Dual
to adjunctionOfRightEquiv.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.rightAdjointOfEquiv_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G_obj : D → C}
(e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
↑(e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(e X Y) g))
{Y : D}
{Y' : D}
(g : Y ⟶ Y')
:
(CategoryTheory.Adjunction.rightAdjointOfEquiv e he).map g = ↑(e (G_obj Y) Y')
(CategoryTheory.CategoryStruct.comp (↑(e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))) g)
@[simp]
theorem
CategoryTheory.Adjunction.rightAdjointOfEquiv_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G_obj : D → C}
(e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
↑(e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(e X Y) g))
:
∀ (a : D), (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a = G_obj a
def
CategoryTheory.Adjunction.rightAdjointOfEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G_obj : D → C}
(e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
↑(e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(e X Y) g))
:
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
@[simp]
theorem
CategoryTheory.Adjunction.adjunctionOfEquivRight_homEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G_obj : D → C}
(e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
↑(e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f (↑(e X Y) g))
(X : C)
(Y : D)
:
@[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))
@[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))
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))
:
Show that the functor given by rightAdjointOfEquiv is indeed right adjoint to F. Dual
to adjunctionOfEquivRight.
Equations
Instances For
@[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)
:
(CategoryTheory.Adjunction.toEquivalence adj).unitIso.hom.app X = adj.unit.app X
@[simp]
theorem
CategoryTheory.Adjunction.toEquivalence_inverse
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)]
:
(CategoryTheory.Adjunction.toEquivalence adj).inverse = G
@[simp]
theorem
CategoryTheory.Adjunction.toEquivalence_unitIso_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)]
(X : C)
:
(CategoryTheory.Adjunction.toEquivalence adj).unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)
@[simp]
theorem
CategoryTheory.Adjunction.toEquivalence_counitIso_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)]
(X : D)
:
(CategoryTheory.Adjunction.toEquivalence adj).counitIso.inv.app X = CategoryTheory.inv (adj.counit.app X)
@[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)
:
(CategoryTheory.Adjunction.toEquivalence adj).counitIso.hom.app X = adj.counit.app X
@[simp]
theorem
CategoryTheory.Adjunction.toEquivalence_functor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)]
:
(CategoryTheory.Adjunction.toEquivalence adj).functor = F
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.
Instances For
@[simp]
theorem
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence_counitIso_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
(X : C)
:
CategoryTheory.IsEquivalence.counitIso.inv.app X = (CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X
@[simp]
theorem
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence_counitIso_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
(X : C)
:
CategoryTheory.IsEquivalence.counitIso.hom.app X = CategoryTheory.inv ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)
@[simp]
theorem
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence_unitIso_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
(X : D)
:
CategoryTheory.IsEquivalence.unitIso.inv.app X = (CategoryTheory.Adjunction.ofRightAdjoint G).counit.app X
@[simp]
theorem
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence_unitIso_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
(X : D)
:
CategoryTheory.IsEquivalence.unitIso.hom.app X = CategoryTheory.inv ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app X)
@[simp]
theorem
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence_inverse
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
:
noncomputable def
CategoryTheory.Adjunction.isRightAdjointToIsEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor D C}
[CategoryTheory.IsRightAdjoint G]
[∀ (X : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).unit.app X)]
[∀ (Y : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint G).counit.app Y)]
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Equivalence.toAdjunction_unit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ D)
:
e.toAdjunction.unit = e.unit
@[simp]
theorem
CategoryTheory.Equivalence.toAdjunction_counit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ D)
:
e.toAdjunction.counit = e.counit
def
CategoryTheory.Equivalence.toAdjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ D)
:
e.functor ⊣ e.inverse
The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
simply use e.symm.toAdjunction.
Equations
- e.toAdjunction = CategoryTheory.Adjunction.mkOfUnitCounit (CategoryTheory.Adjunction.CoreUnitCounit.mk e.unit e.counit)
Instances For
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)
[CategoryTheory.IsEquivalence E]
:
An equivalence E is left adjoint to its inverse.
Equations
- CategoryTheory.Functor.adjunction E = (CategoryTheory.Functor.asEquivalence E).toAdjunction
Instances For
instance
CategoryTheory.Functor.leftAdjointOfEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[CategoryTheory.IsEquivalence F]
:
If F is an equivalence, it's a left adjoint.
Equations
- CategoryTheory.Functor.leftAdjointOfEquivalence = { right := CategoryTheory.Functor.inv F, adj := CategoryTheory.Functor.adjunction F }
@[simp]
theorem
CategoryTheory.Functor.rightAdjoint_of_isEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[CategoryTheory.IsEquivalence F]
:
instance
CategoryTheory.Functor.rightAdjointOfEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[CategoryTheory.IsEquivalence F]
:
If F is an equivalence, it's a right adjoint.
Equations
- CategoryTheory.Functor.rightAdjointOfEquivalence = { left := CategoryTheory.Functor.inv F, adj := CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv F) }
@[simp]
theorem
CategoryTheory.Functor.leftAdjoint_of_isEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[CategoryTheory.IsEquivalence F]
: