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.
The functor from the double-opposite of a category to the underlying category.
Instances For
The functor from a category to its double-opposite.
Instances For
The double opposite category is equivalent to the original.
Instances For
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.
Instances For
Given a functor F : Cᵒᵖ ⥤ Dᵒᵖ
we can take the "unopposite" functor F : C ⥤ D
.
In informal mathematics no distinction is made between these.
Instances For
The isomorphism between F.op.unop
and F
.
Instances For
The isomorphism between F.unop.op
and F
.
Instances For
Taking the opposite of a functor is functorial.
Instances For
Take the "unopposite" of a functor is functorial.
Instances For
Another variant of the opposite of functor, turning a functor C ⥤ Dᵒᵖ
into a functor Cᵒᵖ ⥤ D
.
In informal mathematics no distinction is made.
Instances For
Another variant of the opposite of functor, turning a functor Cᵒᵖ ⥤ D
into a functor C ⥤ Dᵒᵖ
.
In informal mathematics no distinction is made.
Instances For
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.leftOp.rightOp
and F
.
Instances For
The isomorphism between F.rightOp.leftOp
and F
.
Instances For
Whenever possible, it is advisable to use the isomorphism rightOpLeftOpIso
instead of this equality of functors.
The opposite of a natural transformation.
Instances For
The "unopposite" of a natural transformation.
Instances For
Given a natural transformation α : F.op ⟶ G.op
,
we can take the "unopposite" of each component obtaining a natural transformation G ⟶ F
.
Instances For
Given a natural transformation α : F.unop ⟶ G.unop
, we can take the opposite of each
component obtaining a natural transformation G ⟶ F
.
Instances For
Given a natural transformation α : F ⟶ G
, for F G : C ⥤ Dᵒᵖ
,
taking unop
of each component gives a natural transformation G.leftOp ⟶ F.leftOp
.
Instances For
Given a natural transformation α : F.leftOp ⟶ G.leftOp
, for F G : C ⥤ Dᵒᵖ
,
taking op
of each component gives a natural transformation G ⟶ F
.
Instances For
Given a natural transformation α : F ⟶ G
, for F G : Cᵒᵖ ⥤ D
,
taking op
of each component gives a natural transformation G.rightOp ⟶ F.rightOp
.
Instances For
Given a natural transformation α : F.rightOp ⟶ G.rightOp
, for F G : Cᵒᵖ ⥤ D
,
taking unop
of each component gives a natural transformation G ⟶ F
.
Instances For
The opposite isomorphism.
Instances For
The isomorphism obtained from an isomorphism in the opposite category.
Instances For
The natural isomorphism between opposite functors G.op ≅ F.op
induced by a natural
isomorphism between the original functors F ≅ G
.
Instances For
The natural isomorphism between functors G ≅ F
induced by a natural isomorphism
between the opposite functors F.op ≅ G.op
.
Instances For
The natural isomorphism between functors G.unop ≅ F.unop
induced by a natural isomorphism
between the original functors F ≅ G
.
Instances For
An equivalence between categories gives an equivalence between the opposite categories.
Instances For
An equivalence between opposite categories gives an equivalence between the original categories.
Instances For
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 opEquiv' (A : C) (B : Cᵒᵖ) : (Opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
opEquiv _ _
def opEquiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ Opposite.op B) ≃ (B ⟶ A.unop) :=
opEquiv _ _
def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
opEquiv _ _
Instances For
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)
Instances For
The equivalence of functor categories induced by op
and unop
.
Instances For
The equivalence of functor categories induced by leftOp
and rightOp
.