structure
category_theory.adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
- 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}, ⇑(c.hom_equiv X Y) f = c.unit.app X ≫ G.map f) . "obviously"
- hom_equiv_counit' : (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y}, ⇑((c.hom_equiv X Y).symm) g = F.map g ≫ c.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.
@[class]
structure
category_theory.is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
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.
@[class]
structure
category_theory.is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
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.
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') :
structure
category_theory.adjunction.core_hom_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
- 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), ⇑((c.hom_equiv X' Y).symm) (f ≫ g) = F.map f ≫ ⇑((c.hom_equiv X Y).symm) g) . "obviously"
- hom_equiv_naturality_right' : (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ⇑(c.hom_equiv X Y') (f ≫ g) = ⇑(c.hom_equiv X Y) f ≫ G.map g) . "obviously"
@[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') :
structure
category_theory.adjunction.core_unit_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
- unit : 𝟭 C ⟶ F ⋙ G
- counit : G ⋙ F ⟶ 𝟭 D
- left_triangle' : category_theory.whisker_right c.unit F ≫ (F.associator G F).hom ≫ category_theory.whisker_left F c.counit = category_theory.nat_trans.id (𝟭 C ⋙ F) . "obviously"
- right_triangle' : category_theory.whisker_left G c.unit ≫ (G.associator F G).inv ≫ category_theory.whisker_right c.counit G = category_theory.nat_trans.id (G ⋙ 𝟭 C) . "obviously"
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} :
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' := _}
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} :
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' := _}
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' := _}
@[instance]
Equations
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_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_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_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) :
@[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} :
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} :
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) :
Show that adjunctions can be composed.
Equations
- category_theory.adjunction.comp H I adj₁ 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' := _}
@[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.
Equations
- category_theory.adjunction.left_adjoint_of_comp F G = {right := category_theory.is_left_adjoint.right G ⋙ category_theory.is_left_adjoint.right F, adj := category_theory.adjunction.comp G (category_theory.is_left_adjoint.right G) category_theory.is_left_adjoint.adj category_theory.is_left_adjoint.adj}
@[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.
Equations
- category_theory.adjunction.right_adjoint_of_comp = {left := category_theory.is_right_adjoint.left G ⋙ category_theory.is_right_adjoint.left F, adj := category_theory.adjunction.comp (category_theory.is_right_adjoint.left F) F category_theory.is_right_adjoint.adj category_theory.is_right_adjoint.adj}
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)) :
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.
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)) :
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.
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.
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' := _}
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
@[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] :
@[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] :