mathlib3 documentation

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

@[simp]
theorem homological_complex.op_X {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c) (i : ι) :
X.op.X i = opposite.op (X.X i)
@[simp]
theorem homological_complex.op_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c) (i j : ι) :
X.op.d i j = (X.d j i).op
@[protected]

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

Equations
@[protected]

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} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c.symm) (i j : ι) :
X.op_symm.d i j = (X.d j i).op
@[simp]
@[simp]
theorem homological_complex.unop_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c) (i j : ι) :
X.unop.d i j = (X.d j i).unop
@[protected]

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

Equations
@[simp]
@[protected]

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

Equations
@[simp]
@[simp]

Auxilliary definition for op_equivalence.

Equations
Instances for homological_complex.op_functor

Auxilliary definition for op_equivalence.

Equations

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

Auxilliary definition for unop_equivalence.

Equations
Instances for homological_complex.unop_functor
@[simp]

Auxilliary definition for unop_equivalence.

Equations

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
noncomputable def homological_complex.homology_op_def {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (C : homological_complex V 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} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (C : homological_complex V 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

Auxilliary tautological definition for homology_unop.

Equations

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