Opposite categories #
We provide a category instance on Cᵒᵖ
.
The morphisms X ⟶ Y
are defined to be the morphisms unop Y ⟶ unop X
in C
.
Here Cᵒᵖ
is an irreducible typeclass synonym for C
(it is the same one used in the algebra library).
We also provide various mechanisms for constructing opposite morphisms, functors, and natural transformations.
Unfortunately, because we do not have a definitional equality op (op X) = X
,
there are quite a few variations that are needed in practice.
The opposite category.
See https://stacks.math.columbia.edu/tag/001M.
Equations
- category_theory.category.opposite = {to_category_struct := {to_quiver := quiver.opposite category_theory.category_struct.to_quiver, id := λ (X : Cᵒᵖ), (𝟙 (opposite.unop X)).op, comp := λ (_x _x_1 _x_2 : Cᵒᵖ) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), (g.unop ≫ f.unop).op}, id_comp' := _, comp_id' := _, assoc' := _}
The functor from the double-opposite of a category to the underlying category.
The functor from a category to its double-opposite.
Equations
- category_theory.unop_unop C = {obj := λ (X : C), opposite.op (opposite.op X), map := λ (X Y : C) (f : X ⟶ Y), f.op.op, map_id' := _, map_comp' := _}
The double opposite category is equivalent to the original.
Equations
- category_theory.op_op_equivalence C = {functor := category_theory.op_op C _inst_1, inverse := category_theory.unop_unop C _inst_1, unit_iso := category_theory.iso.refl (𝟭 Cᵒᵖᵒᵖ), counit_iso := category_theory.iso.refl (category_theory.unop_unop C ⋙ category_theory.op_op C), functor_unit_iso_comp' := _}
If f
is an isomorphism, so is f.op
If f.op
is an isomorphism f
must be too.
(This cannot be an instance as it would immediately loop!)
The opposite of a functor, i.e. considering a functor F : C ⥤ D
as a functor Cᵒᵖ ⥤ Dᵒᵖ
.
In informal mathematics no distinction is made between these.
Equations
Given a functor F : Cᵒᵖ ⥤ Dᵒᵖ
we can take the "unopposite" functor F : C ⥤ D
.
In informal mathematics no distinction is made between these.
Equations
Instances for category_theory.functor.unop
The isomorphism between F.op.unop
and F
.
Equations
- F.op_unop_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl (F.op.unop.obj X)) _
The isomorphism between F.unop.op
and F
.
Equations
- F.unop_op_iso = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.iso.refl (F.unop.op.obj X)) _
Taking the opposite of a functor is functorial.
Take the "unopposite" of a functor is functorial.
Equations
- category_theory.functor.op_inv C D = {obj := λ (F : Cᵒᵖ ⥤ Dᵒᵖ), opposite.op F.unop, map := λ (F G : Cᵒᵖ ⥤ Dᵒᵖ) (α : F ⟶ G), quiver.hom.op {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}, map_id' := _, map_comp' := _}
Another variant of the opposite of functor, turning a functor C ⥤ Dᵒᵖ
into a functor Cᵒᵖ ⥤ D
.
In informal mathematics no distinction is made.
Equations
Instances for category_theory.functor.left_op
Another variant of the opposite of functor, turning a functor Cᵒᵖ ⥤ D
into a functor C ⥤ Dᵒᵖ
.
In informal mathematics no distinction is made.
Equations
Instances for category_theory.functor.right_op
If F is faithful then the right_op of F is also faithful.
If F is faithful then the left_op of F is also faithful.
The isomorphism between F.left_op.right_op
and F
.
Equations
- F.left_op_right_op_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl (F.left_op.right_op.obj X)) _
The isomorphism between F.right_op.left_op
and F
.
Equations
- F.right_op_left_op_iso = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.iso.refl (F.right_op.left_op.obj X)) _
The opposite of a natural transformation.
Equations
- category_theory.nat_trans.op α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).op, naturality' := _}
The "unopposite" of a natural transformation.
Equations
- category_theory.nat_trans.unop α = {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}
Given a natural transformation α : F.op ⟶ G.op
,
we can take the "unopposite" of each component obtaining a natural transformation G ⟶ F
.
Equations
- category_theory.nat_trans.remove_op α = {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}
Given a natural transformation α : F.unop ⟶ G.unop
, we can take the opposite of each
component obtaining a natural transformation G ⟶ F
.
Equations
- category_theory.nat_trans.remove_unop α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).op, naturality' := _}
Given a natural transformation α : F ⟶ G
, for F G : C ⥤ Dᵒᵖ
,
taking unop
of each component gives a natural transformation G.left_op ⟶ F.left_op
.
Equations
- category_theory.nat_trans.left_op α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).unop, naturality' := _}
Given a natural transformation α : F.left_op ⟶ G.left_op
, for F G : C ⥤ Dᵒᵖ
,
taking op
of each component gives a natural transformation G ⟶ F
.
Equations
- category_theory.nat_trans.remove_left_op α = {app := λ (X : C), (α.app (opposite.op X)).op, naturality' := _}
Given a natural transformation α : F ⟶ G
, for F G : Cᵒᵖ ⥤ D
,
taking op
of each component gives a natural transformation G.right_op ⟶ F.right_op
.
Equations
- category_theory.nat_trans.right_op α = {app := λ (X : C), (α.app (opposite.op X)).op, naturality' := _}
Given a natural transformation α : F.right_op ⟶ G.right_op
, for F G : Cᵒᵖ ⥤ D
,
taking unop
of each component gives a natural transformation G ⟶ F
.
Equations
- category_theory.nat_trans.remove_right_op α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).unop, naturality' := _}
The opposite isomorphism.
The isomorphism obtained from an isomorphism in the opposite category.
The natural isomorphism between opposite functors G.op ≅ F.op
induced by a natural
isomorphism between the original functors F ≅ G
.
Equations
- category_theory.nat_iso.op α = {hom := category_theory.nat_trans.op α.hom, inv := category_theory.nat_trans.op α.inv, hom_inv_id' := _, inv_hom_id' := _}
The natural isomorphism between functors G ≅ F
induced by a natural isomorphism
between the opposite functors F.op ≅ G.op
.
Equations
- category_theory.nat_iso.remove_op α = {hom := category_theory.nat_trans.remove_op α.hom, inv := category_theory.nat_trans.remove_op α.inv, hom_inv_id' := _, inv_hom_id' := _}
The natural isomorphism between functors G.unop ≅ F.unop
induced by a natural isomorphism
between the original functors F ≅ G
.
Equations
- category_theory.nat_iso.unop α = {hom := category_theory.nat_trans.unop α.hom, inv := category_theory.nat_trans.unop α.inv, hom_inv_id' := _, inv_hom_id' := _}
An equivalence between categories gives an equivalence between the opposite categories.
Equations
- e.op = {functor := e.functor.op, inverse := e.inverse.op, unit_iso := (category_theory.nat_iso.op e.unit_iso).symm, counit_iso := (category_theory.nat_iso.op e.counit_iso).symm, functor_unit_iso_comp' := _}
An equivalence between opposite categories gives an equivalence between the original categories.
Equations
- e.unop = {functor := e.functor.unop, inverse := e.inverse.unop, unit_iso := (category_theory.nat_iso.unop e.unit_iso).symm, counit_iso := (category_theory.nat_iso.unop e.counit_iso).symm, functor_unit_iso_comp' := _}
The equivalence between arrows of the form A ⟶ B
and B.unop ⟶ A.unop
. Useful for building
adjunctions.
Note that this (definitionally) gives variants
def op_equiv' (A : C) (B : Cᵒᵖ) : (opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
op_equiv _ _
def op_equiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ opposite.op B) ≃ (B ⟶ A.unop) :=
op_equiv _ _
def op_equiv''' (A B : C) : (opposite.op A ⟶ opposite.op B) ≃ (B ⟶ A) :=
op_equiv _ _
```
Equations
- category_theory.op_equiv A B = {to_fun := λ (f : A ⟶ B), f.unop, inv_fun := λ (g : opposite.unop B ⟶ opposite.unop A), g.op, left_inv := _, right_inv := _}
Equations
The equivalence between isomorphisms of the form A ≅ B
and B.unop ≅ A.unop
.
Note this is definitionally the same as the other three variants:
(opposite.op A ≅ B) ≃ (B.unop ≅ A)
(A ≅ opposite.op B) ≃ (B ≅ A.unop)
(opposite.op A ≅ opposite.op B) ≃ (B ≅ A)
Equations
- category_theory.iso_op_equiv A B = {to_fun := λ (f : A ≅ B), f.unop, inv_fun := λ (g : opposite.unop B ≅ opposite.unop A), g.op, left_inv := _, right_inv := _}
The equivalence of functor categories induced by op
and unop
.
Equations
- category_theory.functor.op_unop_equiv C D = {functor := category_theory.functor.op_hom C D _inst_2, inverse := category_theory.functor.op_inv C D _inst_2, unit_iso := category_theory.nat_iso.of_components (λ (F : (C ⥤ D)ᵒᵖ), (opposite.unop F).op_unop_iso.op) _, counit_iso := category_theory.nat_iso.of_components (λ (F : Cᵒᵖ ⥤ Dᵒᵖ), F.unop_op_iso) _, functor_unit_iso_comp' := _}
The equivalence of functor categories induced by left_op
and right_op
.
Equations
- category_theory.functor.left_op_right_op_equiv C D = {functor := {obj := λ (F : (Cᵒᵖ ⥤ D)ᵒᵖ), (opposite.unop F).right_op, map := λ (F G : (Cᵒᵖ ⥤ D)ᵒᵖ) (η : F ⟶ G), category_theory.nat_trans.right_op η.unop, map_id' := _, map_comp' := _}, inverse := {obj := λ (F : C ⥤ Dᵒᵖ), opposite.op F.left_op, map := λ (F G : C ⥤ Dᵒᵖ) (η : F ⟶ G), (category_theory.nat_trans.left_op η).op, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (F : (Cᵒᵖ ⥤ D)ᵒᵖ), (opposite.unop F).right_op_left_op_iso.op) _, counit_iso := category_theory.nat_iso.of_components (λ (F : C ⥤ Dᵒᵖ), F.left_op_right_op_iso) _, functor_unit_iso_comp' := _}