Opposite categories of cochain complexes

We construct an equivalence of categories CochainComplex.opEquivalence C between (CochainComplex C ℤ)ᵒᵖ and CochainComplex Cᵒᵖ ℤ, and we show that two morphisms in CochainComplex C ℤ are homotopic iff they are homotopic as morphisms in CochainComplex Cᵒᵖ ℤ.

def ComplexShape.embeddingUpIntDownInt : (up ℤ).Embedding (down ℤ)

The embedding of the complex shape up ℤ in down ℤ given by n ↦ -n.

@[simp]

theorem ComplexShape.embeddingUpIntDownInt_f (n : ℤ) : embeddingUpIntDownInt.f n = -n

instance ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt : embeddingUpIntDownInt.IsRelIff

def ComplexShape.embeddingDownIntUpInt : (down ℤ).Embedding (up ℤ)

The embedding of the complex shape down ℤ in up ℤ given by n ↦ -n.

@[simp]

theorem ComplexShape.embeddingDownIntUpInt_f (n : ℤ) : embeddingDownIntUpInt.f n = -n

instance ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt : embeddingDownIntUpInt.IsRelIff

def ChainComplex.cochainComplexEquivalence (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ChainComplex C ℤ ≌ CochainComplex C ℤ

The equivalence of categories ChainComplex C ℤ ≌ CochainComplex C ℤ.

def CochainComplex.opEquivalence (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CochainComplex C ℤ)ᵒᵖ ≌ CochainComplex Cᵒᵖ ℤ

The equivalence of categories (CochainComplex C ℤ)ᵒᵖ ≌ CochainComplex Cᵒᵖ ℤ.

def CochainComplex.homotopyOp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g) : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)

Given an homotopy between morphisms of cochain complexes indexed by ℤ, this is the corresponding homotopy between morphisms of cochain complexes in the opposite category.

theorem CochainComplex.homotopyOp_hom_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g) (p q p' q' : ℤ) (hp : p + p' = 0 := by lia) (hq : q + q' = 0 := by lia) : (homotopyOp h).hom p q = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq L ⋯).hom.op (CategoryTheory.CategoryStruct.comp (h.hom q' p').op (HomologicalComplex.XIsoOfEq K ⋯).hom.op)

def CochainComplex.homotopyUnop {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)) : Homotopy f g

The homotopy between two morphisms of cochain complexes indexed by ℤ which correspond to an homotopy between morphisms of cochain complexes in the opposite category.

theorem CochainComplex.homotopyUnop_hom_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)) (p q p' q' : ℤ) (hp : p + p' = 0 := by lia) (hq : q + q' = 0 := by lia) : (homotopyUnop h).hom p q = CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq K ⋯).hom (CategoryTheory.CategoryStruct.comp (h.hom q' p').unop (HomologicalComplex.XIsoOfEq L ⋯).hom)

def CochainComplex.homotopyOpEquiv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} : Homotopy f g ≃ Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)

Two morphisms of cochain complexes indexed by ℤ are homotopic iff they are homotopic after the application of the functor (opEquivalence C).functor : (CochainComplex C ℤ)ᵒᵖ ⥤ CochainComplex Cᵒᵖ ℤ.

theorem CochainComplex.exactAt_op {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {n : ℤ} (hK : HomologicalComplex.ExactAt K n) (m : ℤ) (hm : n + m = 0 := by lia) : HomologicalComplex.ExactAt ((opEquivalence C).functor.obj (Opposite.op K)) m

theorem CochainComplex.acyclic_op {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} (hK : HomologicalComplex.Acyclic K) : HomologicalComplex.Acyclic ((opEquivalence C).functor.obj (Opposite.op K))