# mathlib3documentation

algebra.homology.opposite

# Opposite categories of complexes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 analagous 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 analagous result for unop).

## Implementation notes #

It is convenient to define both op and op_symm; 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 image_to_kernel_op {V : Type u_1} {X Y Z : V} (f : X Y) (g : Y Z) (w : f g = 0) :
theorem image_to_kernel_unop {V : Type u_1} {X Y Z : Vᵒᵖ} (f : X Y) (g : Y Z) (w : f g = 0) :
noncomputable def homology_op {V : Type u_1} {X Y Z : V} (f : X Y) (g : Y Z) (w : f g = 0) :
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
noncomputable def homology_unop {V : Type u_1} {X Y Z : Vᵒᵖ} (f : X Y) (g : Y Z) (w : f g = 0) :

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
@[simp]
theorem homological_complex.op_X {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) (i : ι) :
X.op.X i = opposite.op (X.X i)
@[simp]
theorem homological_complex.op_d {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) (i j : ι) :
X.op.d i j = (X.d j i).op
@[protected]
def homological_complex.op {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) :

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

Equations
@[protected]
def homological_complex.op_symm {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) :

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

Equations
@[simp]
theorem homological_complex.op_symm_d {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) (i j : ι) :
X.op_symm.d i j = (X.d j i).op
@[simp]
theorem homological_complex.op_symm_X {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) (i : ι) :
X.op_symm.X i = opposite.op (X.X i)
@[simp]
theorem homological_complex.unop_d {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) (i j : ι) :
X.unop.d i j = (X.d j i).unop
@[protected]
def homological_complex.unop {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) :

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

Equations
@[simp]
theorem homological_complex.unop_X {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c) (i : ι) :
X.unop.X i = opposite.unop (X.X i)
@[protected]
def homological_complex.unop_symm {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) :

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

Equations
@[simp]
theorem homological_complex.unop_symm_X {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) (i : ι) :
@[simp]
theorem homological_complex.unop_symm_d {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (X : c.symm) (i j : ι) :
X.unop_symm.d i j = (X.d j i).unop
@[simp]
theorem homological_complex.op_functor_map_f {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X Y : c)ᵒᵖ) (f : X Y) (i : ι) :
f).f i = (f.unop.f i).op
def homological_complex.op_functor {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for op_equivalence.

Equations
Instances for homological_complex.op_functor
@[simp]
theorem homological_complex.op_functor_obj {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X : c)ᵒᵖ) :
= .op
@[simp]
theorem homological_complex.op_inverse_obj {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X : c.symm) :
def homological_complex.op_inverse {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for op_equivalence.

Equations
@[simp]
theorem homological_complex.op_inverse_map {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X Y : c.symm) (f : X Y) :
= quiver.hom.op {f := λ (i : ι), (f.f i).unop, comm' := _}
def homological_complex.op_unit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for op_equivalence.

Equations
def homological_complex.op_counit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for op_equivalence.

Equations
@[simp]
theorem homological_complex.op_equivalence_counit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
@[simp]
theorem homological_complex.op_equivalence_unit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
def homological_complex.op_equivalence {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

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
@[simp]
theorem homological_complex.op_equivalence_functor {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
@[simp]
theorem homological_complex.op_equivalence_inverse {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
def homological_complex.unop_functor {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for unop_equivalence.

Equations
Instances for homological_complex.unop_functor
@[simp]
theorem homological_complex.unop_functor_obj {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X : ᵒᵖ) :
@[simp]
theorem homological_complex.unop_functor_map_f {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X Y : ᵒᵖ) (f : X Y) (i : ι) :
f).f i = (f.unop.f i).unop
@[simp]
theorem homological_complex.unop_inverse_map {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X Y : c.symm) (f : X Y) :
= quiver.hom.op {f := λ (i : ι), (f.f i).op, comm' := _}
@[simp]
theorem homological_complex.unop_inverse_obj {ι : Type u_1} (V : Type u_2) (c : complex_shape ι) (X : c.symm) :
def homological_complex.unop_inverse {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for unop_equivalence.

Equations
def homological_complex.unop_unit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for unop_equivalence.

Equations
def homological_complex.unop_counit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

Auxilliary definition for unop_equivalence.

Equations
@[simp]
theorem homological_complex.unop_equivalence_counit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
def homological_complex.unop_equivalence {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :

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
@[simp]
theorem homological_complex.unop_equivalence_unit_iso {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
@[simp]
theorem homological_complex.unop_equivalence_inverse {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
@[simp]
theorem homological_complex.unop_equivalence_functor {ι : Type u_1} (V : Type u_2) (c : complex_shape ι)  :
@[protected, instance]
def homological_complex.op_functor_additive {ι : Type u_1} {V : Type u_2} {c : complex_shape ι}  :
@[protected, instance]
def homological_complex.unop_functor_additive {ι : Type u_1} {V : Type u_2} {c : complex_shape ι}  :
noncomputable def homological_complex.homology_op_def {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (C : c) (i : ι) :
C.op.homology i homology (C.d_from i).op (C.d_to i).op _

Auxilliary tautological definition for homology_op.

Equations
noncomputable def homological_complex.homology_op {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (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
noncomputable def homological_complex.homology_unop_def {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (i : ι) (C : c) :

Auxilliary tautological definition for homology_unop.

Equations
noncomputable def homological_complex.homology_unop {ι : Type u_1} {V : Type u_2} {c : complex_shape ι} (i : ι) (C : 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