Adjunctions between functors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
F ⊣ G represents the data of an adjunction between two functors
F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.
We provide various useful constructors:
mk_of_hom_equivmk_of_unit_counitleft_adjoint_of_equiv/right_adjoint_of equivconstruct a left/right adjoint of a given functor given the action on objects and the relevant equivalence of morphism spaces.adjunction_of_equiv_left/adjunction_of_equiv_rightwitness that these constructions give adjunctions.
There are also typeclasses is_left_adjoint / is_right_adjoint, carrying data witnessing
that a given functor is a left or right adjoint.
Given [is_left_adjoint F], a right adjoint of F can be constructed as right_adjoint F.
adjunction.comp composes adjunctions.
to_equivalence upgrades an adjunction to an equivalence,
given witnesses that the unit and counit are pointwise isomorphisms.
Conversely equivalence.to_adjunction recovers the underlying adjunction from an equivalence.
structure
category_theory.adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C) :
Type (max u₁ u₂ v₁ v₂)
- hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
- unit : 𝟭 C ⟶ F ⋙ G
- counit : G ⋙ F ⟶ 𝟭 D
- hom_equiv_unit' : (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y}, ⇑(self.hom_equiv X Y) f = self.unit.app X ≫ G.map f) . "obviously"
- hom_equiv_counit' : (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, ⇑((self.hom_equiv X Y).symm) g = F.map g ≫ self.counit.app Y) . "obviously"
F ⊣ G represents the data of an adjunction between two functors
F : C ⥤ D and G : D ⥤ C. F is the left adjoint and G is the right adjoint.
To construct an adjunction between two functors, it's often easier to instead use the
constructors mk_of_hom_equiv or mk_of_unit_counit. To construct a left adjoint,
there are also constructors left_adjoint_of_equiv and adjunction_of_equiv_left (as
well as their duals) which can be simpler in practice.
Uniqueness of adjoints is shown in category_theory.adjunction.opposites.
See https://stacks.math.columbia.edu/tag/0037.
Instances for category_theory.adjunction
- category_theory.adjunction.has_sizeof_inst
- category_theory.adjunction.inhabited
@[class]
structure
category_theory.is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(left : C ⥤ D) :
Type (max u₁ u₂ v₁ v₂)
- right : D ⥤ C
- adj : left ⊣ category_theory.is_left_adjoint.right left
A class giving a chosen right adjoint to the functor left.
Instances of this typeclass
Instances of other typeclasses for category_theory.is_left_adjoint
- category_theory.is_left_adjoint.has_sizeof_inst
@[class]
structure
category_theory.is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(right : D ⥤ C) :
Type (max u₁ u₂ v₁ v₂)
- left : C ⥤ D
- adj : category_theory.is_right_adjoint.left right ⊣ right
A class giving a chosen left adjoint to the functor right.
Instances of this typeclass
Instances of other typeclasses for category_theory.is_right_adjoint
- category_theory.is_right_adjoint.has_sizeof_inst
def
category_theory.left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R] :
C ⥤ D
Extract the left adjoint from the instance giving the chosen adjoint.
def
category_theory.right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(L : C ⥤ D)
[category_theory.is_left_adjoint L] :
D ⥤ C
Extract the right adjoint from the instance giving the chosen adjoint.
def
category_theory.adjunction.of_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(left : C ⥤ D)
[category_theory.is_left_adjoint left] :
left ⊣ category_theory.right_adjoint left
The adjunction associated to a functor known to be a left adjoint.
def
category_theory.adjunction.of_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(right : C ⥤ D)
[category_theory.is_right_adjoint right] :
category_theory.left_adjoint right ⊣ right
The adjunction associated to a functor known to be a right adjoint.
@[simp]
theorem
category_theory.adjunction.hom_equiv_naturality_left_symm
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X' X : C}
{Y : D}
(f : X' ⟶ X)
(g : X ⟶ G.obj Y) :
@[simp]
theorem
category_theory.adjunction.hom_equiv_naturality_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X' X : C}
{Y : D}
(f : X' ⟶ X)
(g : F.obj X ⟶ Y) :
@[simp]
theorem
category_theory.adjunction.hom_equiv_naturality_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X : C}
{Y Y' : D}
(f : F.obj X ⟶ Y)
(g : Y ⟶ Y') :
@[simp]
theorem
category_theory.adjunction.hom_equiv_naturality_right_symm
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X : C}
{Y Y' : D}
(f : X ⟶ G.obj Y)
(g : Y ⟶ Y') :
@[simp]
theorem
category_theory.adjunction.left_triangle
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
category_theory.whisker_right adj.unit F ≫ category_theory.whisker_left F adj.counit = category_theory.nat_trans.id (𝟭 C ⋙ F)
@[simp]
theorem
category_theory.adjunction.right_triangle
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
category_theory.whisker_left G adj.unit ≫ category_theory.whisker_right adj.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C)
@[simp]
theorem
category_theory.adjunction.left_triangle_components_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X : C}
{X' : D}
(f' : (𝟭 D).obj (F.obj X) ⟶ X') :
@[simp]
theorem
category_theory.adjunction.right_triangle_components_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{Y : D}
{X' : C}
(f' : G.obj ((𝟭 D).obj Y) ⟶ X') :
@[simp]
theorem
category_theory.adjunction.counit_naturality_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X Y : D}
(f : X ⟶ Y)
{X' : D}
(f' : (𝟭 D).obj Y ⟶ X') :
@[simp]
theorem
category_theory.adjunction.unit_naturality_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : G.obj (F.obj Y) ⟶ X') :
@[nolint]
structure
category_theory.adjunction.core_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C) :
Type (max u₁ u₂ v₁ v₂)
- hom_equiv : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
- hom_equiv_naturality_left_symm' : (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y), ⇑((self.hom_equiv X' Y).symm) (f ≫ g) = F.map f ≫ ⇑((self.hom_equiv X Y).symm) g) . "obviously"
- hom_equiv_naturality_right' : (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ⇑(self.hom_equiv X Y') (f ≫ g) = ⇑(self.hom_equiv X Y) f ≫ G.map g) . "obviously"
This is an auxiliary data structure useful for constructing adjunctions.
See adjunction.mk_of_hom_equiv.
This structure won't typically be used anywhere else.
Instances for category_theory.adjunction.core_hom_equiv
- category_theory.adjunction.core_hom_equiv.has_sizeof_inst
@[simp]
theorem
category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(self : category_theory.adjunction.core_hom_equiv F G)
{X' X : C}
{Y : D}
(f : X' ⟶ X)
(g : X ⟶ G.obj Y) :
@[simp]
theorem
category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(self : category_theory.adjunction.core_hom_equiv F G)
{X : C}
{Y Y' : D}
(f : F.obj X ⟶ Y)
(g : Y ⟶ Y') :
@[simp]
theorem
category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G)
{X' X : C}
{Y : D}
(f : X' ⟶ X)
(g : F.obj X ⟶ Y) :
@[simp]
theorem
category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right_symm
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G)
{X : C}
{Y Y' : D}
(f : X ⟶ G.obj Y)
(g : Y ⟶ Y') :
@[nolint]
structure
category_theory.adjunction.core_unit_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C) :
Type (max u₁ u₂ v₁ v₂)
- unit : 𝟭 C ⟶ F ⋙ G
- counit : G ⋙ F ⟶ 𝟭 D
- left_triangle' : category_theory.whisker_right self.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F self.counit = category_theory.nat_trans.id (𝟭 C ⋙ F) . "obviously"
- right_triangle' : category_theory.whisker_left G self.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right self.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C) . "obviously"
This is an auxiliary data structure useful for constructing adjunctions.
See adjunction.mk_of_unit_counit.
This structure won't typically be used anywhere else.
Instances for category_theory.adjunction.core_unit_counit
- category_theory.adjunction.core_unit_counit.has_sizeof_inst
@[simp]
theorem
category_theory.adjunction.core_unit_counit.left_triangle
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(self : category_theory.adjunction.core_unit_counit F G) :
category_theory.whisker_right self.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F self.counit = category_theory.nat_trans.id (𝟭 C ⋙ F)
@[simp]
theorem
category_theory.adjunction.core_unit_counit.right_triangle
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(self : category_theory.adjunction.core_unit_counit F G) :
category_theory.whisker_left G self.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right self.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C)
@[simp]
theorem
category_theory.adjunction.mk_of_hom_equiv_unit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G)
(X : C) :
def
category_theory.adjunction.mk_of_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G) :
F ⊣ G
Construct an adjunction between F and G out of a natural bijection between each
F.obj X ⟶ Y and X ⟶ G.obj Y.
Equations
- category_theory.adjunction.mk_of_hom_equiv adj = {hom_equiv := adj.hom_equiv, unit := {app := λ (X : C), ⇑(adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X)), naturality' := _}, counit := {app := λ (Y : D), (adj.hom_equiv (G.obj Y) ((𝟭 D).obj Y)).inv_fun (𝟙 (G.obj Y)), naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[simp]
theorem
category_theory.adjunction.mk_of_hom_equiv_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G)
(X : C)
(Y : D) :
(category_theory.adjunction.mk_of_hom_equiv adj).hom_equiv X Y = adj.hom_equiv X Y
@[simp]
theorem
category_theory.adjunction.mk_of_hom_equiv_counit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_hom_equiv F G)
(Y : D) :
def
category_theory.adjunction.mk_of_unit_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_unit_counit F G) :
F ⊣ G
Construct an adjunction between functors F and G given a unit and counit for the adjunction
satisfying the triangle identities.
Equations
- category_theory.adjunction.mk_of_unit_counit adj = {hom_equiv := λ (X : C) (Y : D), {to_fun := λ (f : F.obj X ⟶ Y), adj.unit.app X ≫ G.map f, inv_fun := λ (g : X ⟶ G.obj Y), F.map g ≫ adj.counit.app Y, left_inv := _, right_inv := _}, unit := adj.unit, counit := adj.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[simp]
theorem
category_theory.adjunction.mk_of_unit_counit_hom_equiv_symm_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_unit_counit F G)
(X : C)
(Y : D)
(g : X ⟶ G.obj Y) :
@[simp]
theorem
category_theory.adjunction.mk_of_unit_counit_unit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_unit_counit F G) :
@[simp]
theorem
category_theory.adjunction.mk_of_unit_counit_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_unit_counit F G) :
@[simp]
theorem
category_theory.adjunction.mk_of_unit_counit_hom_equiv_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : category_theory.adjunction.core_unit_counit F G)
(X : C)
(Y : D)
(f : F.obj X ⟶ Y) :
The adjunction between the identity functor on a category and itself.
Equations
- category_theory.adjunction.id = {hom_equiv := λ (X Y : C), equiv.refl ((𝟭 C).obj X ⟶ Y), unit := 𝟙 (𝟭 C), counit := 𝟙 (𝟭 C ⋙ 𝟭 C), hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
Equations
@[simp]
theorem
category_theory.adjunction.equiv_homset_left_of_nat_iso_symm_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F F' : C ⥤ D}
(iso : F ≅ F')
{X : C}
{Y : D}
(g : F'.obj X ⟶ Y) :
def
category_theory.adjunction.equiv_homset_left_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F F' : C ⥤ D}
(iso : F ≅ F')
{X : C}
{Y : D} :
If F and G are naturally isomorphic functors, establish an equivalence of hom-sets.
@[simp]
theorem
category_theory.adjunction.equiv_homset_left_of_nat_iso_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F F' : C ⥤ D}
(iso : F ≅ F')
{X : C}
{Y : D}
(f : F.obj X ⟶ Y) :
@[simp]
theorem
category_theory.adjunction.equiv_homset_right_of_nat_iso_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G G' : D ⥤ C}
(iso : G ≅ G')
{X : C}
{Y : D}
(f : X ⟶ G.obj Y) :
def
category_theory.adjunction.equiv_homset_right_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G G' : D ⥤ C}
(iso : G ≅ G')
{X : C}
{Y : D} :
If G and H are naturally isomorphic functors, establish an equivalence of hom-sets.
@[simp]
theorem
category_theory.adjunction.equiv_homset_right_of_nat_iso_symm_apply
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G G' : D ⥤ C}
(iso : G ≅ G')
{X : C}
{Y : D}
(g : X ⟶ G'.obj Y) :
def
category_theory.adjunction.of_nat_iso_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
{H : D ⥤ C}
(adj : F ⊣ H)
(iso : F ≅ G) :
G ⊣ H
Transport an adjunction along an natural isomorphism on the left.
Equations
- adj.of_nat_iso_left iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (category_theory.adjunction.equiv_homset_left_of_nat_iso iso.symm).trans (adj.hom_equiv X Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
def
category_theory.adjunction.of_nat_iso_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G H : D ⥤ C}
(adj : F ⊣ G)
(iso : G ≅ H) :
F ⊣ H
Transport an adjunction along an natural isomorphism on the right.
Equations
- adj.of_nat_iso_right iso = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), (adj.hom_equiv X Y).trans (category_theory.adjunction.equiv_homset_right_of_nat_iso iso), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
def
category_theory.adjunction.right_adjoint_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[r : category_theory.is_right_adjoint F] :
Transport being a right adjoint along a natural isomorphism.
def
category_theory.adjunction.left_adjoint_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[r : category_theory.is_left_adjoint F] :
Transport being a left adjoint along a natural isomorphism.
def
category_theory.adjunction.comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
{H : D ⥤ E}
{I : E ⥤ D}
(adj₁ : F ⊣ G)
(adj₂ : H ⊣ I) :
Composition of adjunctions.
See https://stacks.math.columbia.edu/tag/0DV0.
Equations
- adj₁.comp adj₂ = {hom_equiv := λ (X : C) (Z : E), (adj₂.hom_equiv (F.obj X) Z).trans (adj₁.hom_equiv X (I.obj Z)), unit := adj₁.unit ≫ category_theory.whisker_left F (category_theory.whisker_right adj₂.unit G) ≫ (F.associator (H ⋙ I) G).inv, counit := (I.associator G (F ⋙ H)).hom ≫ category_theory.whisker_left I (category_theory.whisker_right adj₁.counit H) ≫ adj₂.counit, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
def
category_theory.adjunction.left_adjoint_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[Fl : category_theory.is_left_adjoint F]
[Gl : category_theory.is_left_adjoint G] :
If F and G are left adjoints then F ⋙ G is a left adjoint too.
@[protected, instance]
def
category_theory.adjunction.right_adjoint_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
{F : C ⥤ D}
{G : D ⥤ E}
[Fr : category_theory.is_right_adjoint F]
[Gr : category_theory.is_right_adjoint G] :
If F and G are right adjoints then F ⋙ G is a right adjoint too.
@[simp]
theorem
category_theory.adjunction.left_adjoint_of_equiv_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g)
(ᾰ : C) :
(category_theory.adjunction.left_adjoint_of_equiv e he).obj ᾰ = F_obj ᾰ
@[simp]
theorem
category_theory.adjunction.left_adjoint_of_equiv_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g)
(X X' : C)
(f : X ⟶ X') :
def
category_theory.adjunction.left_adjoint_of_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g) :
C ⥤ D
Construct a left adjoint functor to G, given the functor's value on objects F_obj and
a bijection e between F_obj X ⟶ Y and X ⟶ G.obj Y satisfying a naturality law
he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g.
Dual to right_adjoint_of_equiv.
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_left_unit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g)
(X : C) :
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_left_counit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g)
(Y : D) :
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_left_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g)
(X : C)
(Y : D) :
(category_theory.adjunction.adjunction_of_equiv_left e he).hom_equiv X Y = e X Y
def
category_theory.adjunction.adjunction_of_equiv_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
{F_obj : C → D}
(e : Π (X : C) (Y : D), (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
(he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ⇑(e X Y') (h ≫ g) = ⇑(e X Y) h ≫ G.map g) :
Show that the functor given by left_adjoint_of_equiv is indeed left adjoint to G. Dual
to adjunction_of_equiv_right.
def
category_theory.adjunction.right_adjoint_of_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g) :
D ⥤ C
Construct a right adjoint functor to F, given the functor's value on objects G_obj and
a bijection e between F.obj X ⟶ Y and X ⟶ G_obj Y satisfying a naturality law
he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g.
Dual to left_adjoint_of_equiv.
@[simp]
theorem
category_theory.adjunction.right_adjoint_of_equiv_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g)
(ᾰ : D) :
(category_theory.adjunction.right_adjoint_of_equiv e he).obj ᾰ = G_obj ᾰ
@[simp]
theorem
category_theory.adjunction.right_adjoint_of_equiv_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g)
(Y Y' : D)
(g : Y ⟶ Y') :
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_right_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g)
(X : C)
(Y : D) :
(category_theory.adjunction.adjunction_of_equiv_right e he).hom_equiv X Y = e X Y
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_right_counit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g)
(Y : D) :
def
category_theory.adjunction.adjunction_of_equiv_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g) :
Show that the functor given by right_adjoint_of_equiv is indeed right adjoint to F. Dual
to adjunction_of_equiv_left.
@[simp]
theorem
category_theory.adjunction.adjunction_of_equiv_right_unit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G_obj : D → C}
(e : Π (X : C) (Y : D), (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
(he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ⇑(e X' Y) (F.map f ≫ g) = f ≫ ⇑(e X Y) g)
(X : C) :
@[simp]
theorem
category_theory.adjunction.to_equivalence_inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
[∀ (X : C), category_theory.is_iso (adj.unit.app X)]
[∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
adj.to_equivalence.inverse = G
@[simp]
theorem
category_theory.adjunction.to_equivalence_functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
[∀ (X : C), category_theory.is_iso (adj.unit.app X)]
[∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
adj.to_equivalence.functor = F
@[simp]
theorem
category_theory.adjunction.to_equivalence_unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
[∀ (X : C), category_theory.is_iso (adj.unit.app X)]
[∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
adj.to_equivalence.unit_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (adj.unit.app X)) _
@[simp]
theorem
category_theory.adjunction.to_equivalence_counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
[∀ (X : C), category_theory.is_iso (adj.unit.app X)]
[∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
adj.to_equivalence.counit_iso = category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (adj.counit.app Y)) _
noncomputable
def
category_theory.adjunction.to_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
[∀ (X : C), category_theory.is_iso (adj.unit.app X)]
[∀ (Y : D), category_theory.is_iso (adj.counit.app Y)] :
C ≌ D
If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the adjunction to an equivalence.
Equations
- adj.to_equivalence = {functor := F, inverse := G, unit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (adj.unit.app X)) _, counit_iso := category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (adj.counit.app Y)) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.adjunction.is_right_adjoint_to_is_equivalence_inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] :
@[simp]
theorem
category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)]
(X : C) :
@[simp]
theorem
category_theory.adjunction.is_right_adjoint_to_is_equivalence_counit_iso_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)]
(X : C) :
noncomputable
def
category_theory.adjunction.is_right_adjoint_to_is_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)] :
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.
@[simp]
theorem
category_theory.adjunction.is_right_adjoint_to_is_equivalence_unit_iso_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)]
(X : D) :
@[simp]
theorem
category_theory.adjunction.is_right_adjoint_to_is_equivalence_unit_iso_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : D ⥤ C}
[category_theory.is_right_adjoint G]
[∀ (X : C), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).unit.app X)]
[∀ (Y : D), category_theory.is_iso ((category_theory.adjunction.of_right_adjoint G).counit.app Y)]
(X : D) :
def
category_theory.equivalence.to_adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
simply use e.symm.to_adjunction.
Equations
- e.to_adjunction = category_theory.adjunction.mk_of_unit_counit {unit := e.unit, counit := e.counit, left_triangle' := _, right_triangle' := _}
@[simp]
theorem
category_theory.equivalence.as_equivalence_to_adjunction_unit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{e : C ≌ D} :
@[simp]
theorem
category_theory.equivalence.as_equivalence_to_adjunction_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{e : C ≌ D} :
def
category_theory.functor.adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : C ⥤ D)
[category_theory.is_equivalence E] :
An equivalence E is left adjoint to its inverse.
Equations
@[protected, instance]
def
category_theory.functor.left_adjoint_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_equivalence F] :
If F is an equivalence, it's a left adjoint.
Equations
- category_theory.functor.left_adjoint_of_equivalence = {right := F.inv _inst_3, adj := F.adjunction _inst_3}
@[simp]
theorem
category_theory.functor.right_adjoint_of_is_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_equivalence F] :
@[protected, instance]
def
category_theory.functor.right_adjoint_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_equivalence F] :
If F is an equivalence, it's a right adjoint.
Equations
- category_theory.functor.right_adjoint_of_equivalence = {left := F.inv _inst_3, adj := F.inv.adjunction F.is_equivalence_inv}
@[simp]
theorem
category_theory.functor.left_adjoint_of_is_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[category_theory.is_equivalence F] :