Documentation

Mathlib.Algebra.Homology.Opposite

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

def homologyOp {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Abelian V] {X : V} {Y : V} {Z : V} (f : X Y) (g : Y Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) :

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

Instances For
    def homologyUnop {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Abelian V] {X : Vᵒᵖ} {Y : Vᵒᵖ} {Z : Vᵒᵖ} (f : X Y) (g : Y Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) :
    homology g.unop f.unop (_ : CategoryTheory.CategoryStruct.comp g.unop f.unop = 0) (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.

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

              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ᵒᵖ.

              Instances For

                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.

                Instances For

                  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.

                  Instances For

                    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.

                    Instances For