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.

Equations

• ComplexShape.embeddingUpIntDownInt = { f := fun (n : ℤ) => -n, injective_f := ComplexShape.embeddingUpIntDownInt._proof_2, rel := ComplexShape.embeddingUpIntDownInt._proof_3 }

@[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.

Equations

• ComplexShape.embeddingDownIntUpInt = { f := fun (n : ℤ) => -n, injective_f := ComplexShape.embeddingUpIntDownInt._proof_2, rel := @ComplexShape.embeddingDownIntUpInt._proof_2 }

@[simp]

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

instance ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt : embeddingDownIntUpInt.IsRelIff

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CochainComplex.opEquivalence C = (HomologicalComplex.opEquivalence C (ComplexShape.up ℤ)).trans (ChainComplex.cochainComplexEquivalence Cᵒᵖ)

def CochainComplex.homotopyOp {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• CochainComplex.homotopyOp h = { hom := fun (p q : ℤ) => (h.hom (-q) (-p)).op, zero := ⋯, comm := ⋯ }

theorem CochainComplex.homotopyOp_hom_eq {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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.

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.homotopyUnop_hom_eq {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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ᵒᵖ ℤ.

Equations

• One or more equations did not get rendered due to their size.