# Opposite categories of complexes #

Given a preadditive category V, the opposite of its category of chain complexes is equivalent to the category of cochain complexes of objects in Vᵒᵖ. We define this equivalence, and another analogous equivalence (for a general category of homological complexes with a general complex shape).

We then show that when V is abelian, if C is a homological complex, then the homology of op(C) is isomorphic to op of the homology of C (and the analogous result for unop).

## Implementation notes #

It is convenient to define both op and opSymm; this is because given a complex shape c, c.symm.symm is not defeq to c.

## Tags #

opposite, chain complex, cochain complex, homology, cohomology, homological complex

theorem imageToKernel_op {V : Type u_1} [] {X : V} {Y : V} {Z : V} (f : X Y) (g : Y Z) (w : ) :
imageToKernel g.op f.op =
theorem imageToKernel_unop {V : Type u_1} [] {X : Vᵒᵖ} {Y : Vᵒᵖ} {Z : Vᵒᵖ} (f : X Y) (g : Y Z) (w : ) :
def homology'Op {V : Type u_1} [] {X : V} {Y : V} {Z : V} (f : X Y) (g : Y Z) (w : ) :
homology' g.op f.op Opposite.op (homology' f g w)

Given f, g with f ≫ g = 0, the homology of g.op, f.op is the opposite of the homology of f, g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def homology'Unop {V : Type u_1} [] {X : Vᵒᵖ} {Y : Vᵒᵖ} {Z : Vᵒᵖ} (f : X Y) (g : Y Z) (w : ) :
homology' g.unop f.unop (homology' f g w).unop

Given morphisms f, g in Vᵒᵖ with f ≫ g = 0, the homology of g.unop, f.unop is the opposite of the homology of f, g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.op_d {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) (j : ι) :
.d i j = (X.d j i).op
@[simp]
theorem HomologicalComplex.op_X {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) :
.X i = Opposite.op (X.X i)
def HomologicalComplex.op {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) :

Sends a complex X with objects in V to the corresponding complex with objects in Vᵒᵖ.

Equations
• = { X := fun (i : ι) => Opposite.op (X.X i), d := fun (i j : ι) => (X.d j i).op, shape := , d_comp_d' := }
Instances For
@[simp]
theorem HomologicalComplex.opSymm_X {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) :
i = Opposite.op (X.X i)
@[simp]
theorem HomologicalComplex.opSymm_d {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) (j : ι) :
i j = (X.d j i).op
def HomologicalComplex.opSymm {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) :

Sends a complex X with objects in V to the corresponding complex with objects in Vᵒᵖ.

Equations
• = { X := fun (i : ι) => Opposite.op (X.X i), d := fun (i j : ι) => (X.d j i).op, shape := , d_comp_d' := }
Instances For
@[simp]
theorem HomologicalComplex.unop_d {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) (j : ι) :
.d i j = (X.d j i).unop
@[simp]
theorem HomologicalComplex.unop_X {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) :
.X i = (X.X i).unop
def HomologicalComplex.unop {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) :

Sends a complex X with objects in Vᵒᵖ to the corresponding complex with objects in V.

Equations
• = { X := fun (i : ι) => (X.X i).unop, d := fun (i j : ι) => (X.d j i).unop, shape := , d_comp_d' := }
Instances For
@[simp]
theorem HomologicalComplex.unopSymm_d {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) (j : ι) :
i j = (X.d j i).unop
@[simp]
theorem HomologicalComplex.unopSymm_X {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) (i : ι) :
i = (X.X i).unop
def HomologicalComplex.unopSymm {ι : Type u_1} {V : Type u_2} [] {c : } (X : ) :

Sends a complex X with objects in Vᵒᵖ to the corresponding complex with objects in V.

Equations
• = { X := fun (i : ι) => (X.X i).unop, d := fun (i j : ι) => (X.d j i).unop, shape := , d_comp_d' := }
Instances For
@[simp]
theorem HomologicalComplex.opFunctor_obj {ι : Type u_1} (V : Type u_2) [] (c : ) (X : ()ᵒᵖ) :
.obj X = HomologicalComplex.op X.unop
@[simp]
theorem HomologicalComplex.opFunctor_map_f {ι : Type u_1} (V : Type u_2) [] (c : ) :
∀ {X Y : ()ᵒᵖ} (f : X Y) (i : ι), (.map f).f i = (f.unop.f i).op
def HomologicalComplex.opFunctor {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for opEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.opInverse_map {ι : Type u_1} (V : Type u_2) [] (c : ) :
∀ {X Y : } (f : X Y), .map f = { f := fun (i : ι) => (f.f i).unop, comm' := }.op
@[simp]
theorem HomologicalComplex.opInverse_obj {ι : Type u_1} (V : Type u_2) [] (c : ) (X : ) :
.obj X =
def HomologicalComplex.opInverse {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for opEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HomologicalComplex.opUnitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for opEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HomologicalComplex.opCounitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for opEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.opEquivalence_inverse {ι : Type u_1} (V : Type u_2) [] (c : ) :
.inverse =
@[simp]
theorem HomologicalComplex.opEquivalence_counitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :
.counitIso =
@[simp]
theorem HomologicalComplex.opEquivalence_functor {ι : Type u_1} (V : Type u_2) [] (c : ) :
.functor =
@[simp]
theorem HomologicalComplex.opEquivalence_unitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :
.unitIso =
def HomologicalComplex.opEquivalence {ι : Type u_1} (V : Type u_2) [] (c : ) :

Given a category of complexes with objects in V, there is a natural equivalence between its opposite category and a category of complexes with objects in Vᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.unopFunctor_map_f {ι : Type u_1} (V : Type u_2) [] (c : ) :
∀ {X Y : ()ᵒᵖ} (f : X Y) (i : ι), (.map f).f i = (f.unop.f i).unop
@[simp]
theorem HomologicalComplex.unopFunctor_obj {ι : Type u_1} (V : Type u_2) [] (c : ) (X : ()ᵒᵖ) :
def HomologicalComplex.unopFunctor {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for unopEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.unopInverse_obj {ι : Type u_1} (V : Type u_2) [] (c : ) (X : ) :
.obj X =
@[simp]
theorem HomologicalComplex.unopInverse_map {ι : Type u_1} (V : Type u_2) [] (c : ) :
∀ {X Y : } (f : X Y), .map f = { f := fun (i : ι) => (f.f i).op, comm' := }.op
def HomologicalComplex.unopInverse {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for unopEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HomologicalComplex.unopUnitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for unopEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HomologicalComplex.unopCounitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :

Auxiliary definition for unopEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.unopEquivalence_unitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :
.unitIso =
@[simp]
theorem HomologicalComplex.unopEquivalence_functor {ι : Type u_1} (V : Type u_2) [] (c : ) :
.functor =
@[simp]
theorem HomologicalComplex.unopEquivalence_counitIso {ι : Type u_1} (V : Type u_2) [] (c : ) :
.counitIso =
@[simp]
theorem HomologicalComplex.unopEquivalence_inverse {ι : Type u_1} (V : Type u_2) [] (c : ) :
.inverse =
def HomologicalComplex.unopEquivalence {ι : Type u_1} (V : Type u_2) [] (c : ) :

Given a category of complexes with objects in Vᵒᵖ, there is a natural equivalence between its opposite category and a category of complexes with objects in V.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance HomologicalComplex.opFunctor_additive {ι : Type u_1} {V : Type u_2} [] {c : } :
Equations
• =
instance HomologicalComplex.unopFunctor_additive {ι : Type u_1} {V : Type u_2} [] {c : } :
Equations
• =
instance HomologicalComplex.instHasHomologyPreadditiveHasZeroMorphismsSymmUnop {ι : Type u_1} {V : Type u_2} [] {c : } (K : ) (i : ι) :
Equations
• =
def HomologicalComplex.homologyOp {ι : Type u_1} {V : Type u_2} [] {c : } (K : ) (i : ι) :

If K is a homological complex, then the homology of K.op identifies to the opposite of the homology of K.

Equations
Instances For
def HomologicalComplex.homologyUnop {ι : Type u_1} {V : Type u_2} [] {c : } (K : ) (i : ι) :

If K is a homological complex in the opposite category, then the homology of K.unop identifies to the opposite of the homology of K.

Equations
Instances For
def HomologicalComplex.homology'OpDef {ι : Type u_1} {V : Type u_2} [] {c : } (C : ) (i : ι) :
homology' ().op ().op

Auxiliary tautological definition for homologyOp.

Equations
Instances For
def HomologicalComplex.homology'Op {ι : Type u_1} {V : Type u_2} [] {c : } (C : ) (i : ι) :

Given a complex C of objects in V, the ith homology of its 'opposite' complex (with objects in Vᵒᵖ) is the opposite of the ith homology of C.

Equations
Instances For
def HomologicalComplex.homology'UnopDef {ι : Type u_1} {V : Type u_2} [] {c : } (i : ι) (C : ) :
homology' ().unop ().unop

Auxiliary tautological definition for homologyUnop.

Equations
Instances For
def HomologicalComplex.homology'Unop {ι : Type u_1} {V : Type u_2} [] {c : } (i : ι) (C : ) :

Given a complex C of objects in Vᵒᵖ, the ith homology of its 'opposite' complex (with objects in V) is the opposite of the ith homology of C.

Equations
Instances For