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

theorem imageToKernel_op {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.op f.op ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv)

theorem imageToKernel_unop {V : Type u_1} [CategoryTheory.Category.{u_2, u_1} V] [CategoryTheory.Abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.unop f.unop ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv)

def HomologicalComplex.op {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c) : HomologicalComplex Vᵒᵖ c.symm

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

@[simp]

theorem HomologicalComplex.op_d {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c) (i j : ι) : X.op.d i j = (X.d j i).op

@[simp]

theorem HomologicalComplex.op_X {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c) (i : ι) : X.op.X i = Opposite.op (X.X i)

def HomologicalComplex.opSymm {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) : HomologicalComplex Vᵒᵖ c

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

@[simp]

theorem HomologicalComplex.opSymm_d {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) (i j : ι) : X.opSymm.d i j = (X.d j i).op

@[simp]

theorem HomologicalComplex.opSymm_X {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) (i : ι) : X.opSymm.X i = Opposite.op (X.X i)

def HomologicalComplex.unop {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c) : HomologicalComplex V c.symm

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

@[simp]

theorem HomologicalComplex.unop_d {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c) (i j : ι) : X.unop.d i j = (X.d j i).unop

@[simp]

theorem HomologicalComplex.unop_X {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c) (i : ι) : X.unop.X i = Opposite.unop (X.X i)

def HomologicalComplex.unopSymm {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) : HomologicalComplex V c

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

@[simp]

theorem HomologicalComplex.unopSymm_X {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) (i : ι) : X.unopSymm.X i = Opposite.unop (X.X i)

@[simp]

theorem HomologicalComplex.unopSymm_d {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) (i j : ι) : X.unopSymm.d i j = (X.d j i).unop

def HomologicalComplex.opFunctor {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex V c)ᵒᵖ (HomologicalComplex Vᵒᵖ c.symm)

Auxiliary definition for opEquivalence.

@[simp]

theorem HomologicalComplex.opFunctor_obj {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (X : (HomologicalComplex V c)ᵒᵖ) : (opFunctor V c).obj X = (Opposite.unop X).op

@[simp]

theorem HomologicalComplex.opFunctor_map_f {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] {X✝ Y✝ : (HomologicalComplex V c)ᵒᵖ} (f : X✝ ⟶ Y✝) (i : ι) : ((opFunctor V c).map f).f i = (f.unop.f i).op

def HomologicalComplex.opInverse {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex Vᵒᵖ c.symm) (HomologicalComplex V c)ᵒᵖ

Auxiliary definition for opEquivalence.

@[simp]

theorem HomologicalComplex.opInverse_obj {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) : (opInverse V c).obj X = Opposite.op X.unopSymm

@[simp]

theorem HomologicalComplex.opInverse_map {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] {X✝ Y✝ : HomologicalComplex Vᵒᵖ c.symm} (f : X✝ ⟶ Y✝) : (opInverse V c).map f = Quiver.Hom.op { f := fun (i : ι) => (f.f i).unop, comm' := ⋯ }

def HomologicalComplex.opUnitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.id (HomologicalComplex V c)ᵒᵖ ≅ (opFunctor V c).comp (opInverse V c)

Auxiliary definition for opEquivalence.

def HomologicalComplex.opCounitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (opInverse V c).comp (opFunctor V c) ≅ CategoryTheory.Functor.id (HomologicalComplex Vᵒᵖ c.symm)

Auxiliary definition for opEquivalence.

def HomologicalComplex.opEquivalence {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex V c)ᵒᵖ ≌ HomologicalComplex Vᵒᵖ c.symm

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

@[simp]

theorem HomologicalComplex.opEquivalence_inverse {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (opEquivalence V c).inverse = opInverse V c

@[simp]

theorem HomologicalComplex.opEquivalence_unitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (opEquivalence V c).unitIso = opUnitIso V c

@[simp]

theorem HomologicalComplex.opEquivalence_functor {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (opEquivalence V c).functor = opFunctor V c

@[simp]

theorem HomologicalComplex.opEquivalence_counitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (opEquivalence V c).counitIso = opCounitIso V c

def HomologicalComplex.unopFunctor {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex Vᵒᵖ c)ᵒᵖ (HomologicalComplex V c.symm)

Auxiliary definition for unopEquivalence.

@[simp]

theorem HomologicalComplex.unopFunctor_map_f {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] {X✝ Y✝ : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X✝ ⟶ Y✝) (i : ι) : ((unopFunctor V c).map f).f i = (f.unop.f i).unop

@[simp]

theorem HomologicalComplex.unopFunctor_obj {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ) : (unopFunctor V c).obj X = (Opposite.unop X).unop

def HomologicalComplex.unopInverse {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex V c.symm) (HomologicalComplex Vᵒᵖ c)ᵒᵖ

Auxiliary definition for unopEquivalence.

@[simp]

theorem HomologicalComplex.unopInverse_map {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] {X✝ Y✝ : HomologicalComplex V c.symm} (f : X✝ ⟶ Y✝) : (unopInverse V c).map f = Quiver.Hom.op { f := fun (i : ι) => (f.f i).op, comm' := ⋯ }

@[simp]

theorem HomologicalComplex.unopInverse_obj {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) : (unopInverse V c).obj X = Opposite.op X.opSymm

def HomologicalComplex.unopUnitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.id (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≅ (unopFunctor V c).comp (unopInverse V c)

Auxiliary definition for unopEquivalence.

def HomologicalComplex.unopCounitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (unopInverse V c).comp (unopFunctor V c) ≅ CategoryTheory.Functor.id (HomologicalComplex V c.symm)

Auxiliary definition for unopEquivalence.

def HomologicalComplex.unopEquivalence {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≌ HomologicalComplex V c.symm

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.

@[simp]

theorem HomologicalComplex.unopEquivalence_functor {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (unopEquivalence V c).functor = unopFunctor V c

@[simp]

theorem HomologicalComplex.unopEquivalence_unitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (unopEquivalence V c).unitIso = unopUnitIso V c

@[simp]

theorem HomologicalComplex.unopEquivalence_inverse {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (unopEquivalence V c).inverse = unopInverse V c

@[simp]

theorem HomologicalComplex.unopEquivalence_counitIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] : (unopEquivalence V c).counitIso = unopCounitIso V c

instance HomologicalComplex.instHasHomologyOppositeOp {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.HasHomology i

instance HomologicalComplex.instHasHomologyUnopOfOpposite {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : K.unop.HasHomology i

instance HomologicalComplex.instHasHomologyOppositeObjSymmOpFunctorOp {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : ((opFunctor V c).obj (Opposite.op K)).HasHomology i

instance HomologicalComplex.instHasHomologyObjOppositeSymmUnopFunctorOp {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : ((unopFunctor V c).obj (Opposite.op K)).HasHomology i

@[simp]

theorem HomologicalComplex.quasiIsoAt_opFunctor_map_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : QuasiIsoAt ((opFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

@[simp]

theorem HomologicalComplex.quasiIsoAt_unopFunctor_map_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : QuasiIsoAt ((unopFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

instance HomologicalComplex.instQuasiIsoAtOppositeMapSymmOpFunctorOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt φ i] : QuasiIsoAt ((opFunctor V c).map φ.op) i

instance HomologicalComplex.instQuasiIsoAtMapOppositeSymmUnopFunctorOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt φ i] : QuasiIsoAt ((unopFunctor V c).map φ.op) i

@[simp]

theorem HomologicalComplex.quasiIso_opFunctor_map_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] : QuasiIso ((opFunctor V c).map φ.op) ↔ QuasiIso φ

@[simp]

theorem HomologicalComplex.quasiIso_unopFunctor_map_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] : QuasiIso ((unopFunctor V c).map φ.op) ↔ QuasiIso φ

instance HomologicalComplex.instQuasiIsoOppositeMapSymmOpFunctorOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [QuasiIso φ] : QuasiIso ((opFunctor V c).map φ.op)

instance HomologicalComplex.instQuasiIsoMapOppositeSymmUnopFunctorOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [QuasiIso φ] : QuasiIso ((unopFunctor V c).map φ.op)

theorem HomologicalComplex.ExactAt.op {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex V c} {i : ι} (h : K.ExactAt i) : K.op.ExactAt i

theorem HomologicalComplex.ExactAt.unop {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex Vᵒᵖ c} {i : ι} (h : K.ExactAt i) : K.unop.ExactAt i

@[simp]

theorem HomologicalComplex.exactAt_op_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) {i : ι} : K.op.ExactAt i ↔ K.ExactAt i

theorem HomologicalComplex.Acyclic.op {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex V c} (h : K.Acyclic) : K.op.Acyclic

theorem HomologicalComplex.Acyclic.unop {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex Vᵒᵖ c} (h : K.Acyclic) : K.unop.Acyclic

@[simp]

theorem HomologicalComplex.acyclic_op_iff {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) : K.op.Acyclic ↔ K.Acyclic

def HomologicalComplex.homologyOp {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.homology i ≅ Opposite.op (K.homology i)

If K is a homological complex, then the homology of K.op identifies to the opposite of the homology of K.

def HomologicalComplex.homologyUnop {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i] : K.unop.homology i ≅ Opposite.unop (K.homology i)

If K is a homological complex in the opposite category, then the homology of K.unop identifies to the opposite of the homology of K.

def HomologicalComplex.cyclesOpIso {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.cycles i ≅ Opposite.op (K.opcycles i)

The canonical isomorphism K.op.cycles i ≅ op (K.opcycles i).

def HomologicalComplex.opcyclesOpIso {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.opcycles i ≅ Opposite.op (K.cycles i)

The canonical isomorphism K.op.opcycles i ≅ op (K.cycles i).

@[simp]

theorem HomologicalComplex.opcyclesOpIso_hom_toCycles_op {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] (j : ι) : CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom (K.toCycles j i).op = K.op.fromOpcycles i j

@[simp]

theorem HomologicalComplex.opcyclesOpIso_hom_toCycles_op_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] (j : ι) {Z : Vᵒᵖ} (h : Opposite.op (K.X j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom (CategoryTheory.CategoryStruct.comp (K.toCycles j i).op h) = CategoryTheory.CategoryStruct.comp (K.op.fromOpcycles i j) h

@[simp]

theorem HomologicalComplex.fromOpcycles_op_cyclesOpIso_inv {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] (j : ι) : CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j).op (K.cyclesOpIso i).inv = K.op.toCycles j i

@[simp]

theorem HomologicalComplex.fromOpcycles_op_cyclesOpIso_inv_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] (j : ι) {Z : Vᵒᵖ} (h : K.op.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j).op (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).inv h) = CategoryTheory.CategoryStruct.comp (K.op.toCycles j i) h

theorem HomologicalComplex.homologyOp_hom_naturality {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (homologyMap ((opFunctor V c).map φ.op) i) (K.homologyOp i).hom = CategoryTheory.CategoryStruct.comp (L.homologyOp i).hom (homologyMap φ i).op

theorem HomologicalComplex.homologyOp_hom_naturality_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.homology i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (homologyMap ((opFunctor V c).map φ.op) i) (CategoryTheory.CategoryStruct.comp (K.homologyOp i).hom h) = CategoryTheory.CategoryStruct.comp (L.homologyOp i).hom (CategoryTheory.CategoryStruct.comp (homologyMap φ i).op h)

theorem HomologicalComplex.opcyclesOpIso_hom_naturality {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (opcyclesMap ((opFunctor V c).map φ.op) i) (K.opcyclesOpIso i).hom = CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).hom (cyclesMap φ i).op

theorem HomologicalComplex.opcyclesOpIso_hom_naturality_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.cycles i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (opcyclesMap ((opFunctor V c).map φ.op) i) (CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom h) = CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).hom (CategoryTheory.CategoryStruct.comp (cyclesMap φ i).op h)

theorem HomologicalComplex.opcyclesOpIso_inv_naturality {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (cyclesMap φ i).op (K.opcyclesOpIso i).inv = CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).inv (opcyclesMap ((opFunctor V c).map φ.op) i)

theorem HomologicalComplex.opcyclesOpIso_inv_naturality_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : Vᵒᵖ} (h : K.op.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap φ i).op (CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).inv h) = CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).inv (CategoryTheory.CategoryStruct.comp (opcyclesMap ((opFunctor V c).map φ.op) i) h)

theorem HomologicalComplex.cyclesOpIso_hom_naturality {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (cyclesMap ((opFunctor V c).map φ.op) i) (K.cyclesOpIso i).hom = CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).hom (opcyclesMap φ i).op

theorem HomologicalComplex.cyclesOpIso_hom_naturality_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.opcycles i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap ((opFunctor V c).map φ.op) i) (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).hom h) = CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).hom (CategoryTheory.CategoryStruct.comp (opcyclesMap φ i).op h)

theorem HomologicalComplex.cyclesOpIso_inv_naturality {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (opcyclesMap φ i).op (K.cyclesOpIso i).inv = CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).inv (cyclesMap ((opFunctor V c).map φ.op) i)

theorem HomologicalComplex.cyclesOpIso_inv_naturality_assoc {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : Vᵒᵖ} (h : K.op.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (opcyclesMap φ i).op (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).inv h) = CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).inv (CategoryTheory.CategoryStruct.comp (cyclesMap ((opFunctor V c).map φ.op) i) h)

def HomologicalComplex.cyclesOpNatIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.CategoryWithHomology V] (i : ι) : (opFunctor V c).comp (cyclesFunctor Vᵒᵖ c.symm i) ≅ (opcyclesFunctor V c i).op

The natural isomorphism K.op.cycles i ≅ op (K.opcycles i).

@[simp]

theorem HomologicalComplex.cyclesOpNatIso_inv_app {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.CategoryWithHomology V] (i : ι) (X : (HomologicalComplex V c)ᵒᵖ) : (cyclesOpNatIso V c i).inv.app X = ((Opposite.unop X).cyclesOpIso i).inv

@[simp]

theorem HomologicalComplex.cyclesOpNatIso_hom_app {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.CategoryWithHomology V] (i : ι) (X : (HomologicalComplex V c)ᵒᵖ) : (cyclesOpNatIso V c i).hom.app X = ((Opposite.unop X).cyclesOpIso i).hom

def HomologicalComplex.opcyclesOpNatIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.CategoryWithHomology V] (i : ι) : (opFunctor V c).comp (opcyclesFunctor Vᵒᵖ c.symm i) ≅ (cyclesFunctor V c i).op

The natural isomorphism K.op.opcycles i ≅ op (K.cycles i).

def HomologicalComplex.homologyOpNatIso {ι : Type u_1} (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.CategoryWithHomology V] (i : ι) : (opFunctor V c).comp (homologyFunctor Vᵒᵖ c.symm i) ≅ (homologyFunctor V c i).op

The natural isomorphism K.op.homology i ≅ op (K.homology i).

instance HomologicalComplex.opFunctor_additive {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Preadditive V] : (opFunctor V c).Additive

instance HomologicalComplex.unopFunctor_additive {ι : Type u_1} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] {c : ComplexShape ι} [CategoryTheory.Preadditive V] : (unopFunctor V c).Additive