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 : V}
{Y : V}
{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 : Vᵒᵖ}
{Y : Vᵒᵖ}
{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ᵒᵖ.
Equations
- X.op = { X := fun (i : ι) => Opposite.op (X.X i), d := fun (i j : ι) => (X.d j i).op, shape := ⋯, d_comp_d' := ⋯ }
Instances For
@[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)
:
Sends a complex X with objects in V to the corresponding complex with objects in Vᵒᵖ.
Equations
- X.opSymm = { X := fun (i : ι) => Opposite.op (X.X i), d := fun (i j : ι) => (X.d j i).op, shape := ⋯, d_comp_d' := ⋯ }
Instances For
@[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.
Equations
- X.unop = { X := fun (i : ι) => Opposite.unop (X.X i), d := fun (i j : ι) => (X.d j i).unop, shape := ⋯, d_comp_d' := ⋯ }
Instances For
@[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)
:
Sends a complex X with objects in Vᵒᵖ to the corresponding complex with objects in V.
Equations
- X.unopSymm = { X := fun (i : ι) => Opposite.unop (X.X i), d := fun (i j : ι) => (X.d j i).unop, shape := ⋯, d_comp_d' := ⋯ }
Instances For
@[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)ᵒᵖ)
:
(HomologicalComplex.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 : ι),
((HomologicalComplex.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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),
(HomologicalComplex.opInverse V c).map f = Quiver.Hom.op { f := fun (i : ι) => (f.f i).unop, comm' := ⋯ }
@[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)
:
(HomologicalComplex.opInverse V c).obj X = Opposite.op X.unopSymm
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)ᵒᵖ ≅ (HomologicalComplex.opFunctor V c).comp (HomologicalComplex.opInverse V c)
Auxiliary definition for opEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HomologicalComplex.opCounitIso
{ι : Type u_1}
(V : Type u_2)
[CategoryTheory.Category.{u_3, u_2} V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroMorphisms V]
:
(HomologicalComplex.opInverse V c).comp (HomologicalComplex.opFunctor V c) ≅ CategoryTheory.Functor.id (HomologicalComplex Vᵒᵖ c.symm)
Auxiliary definition for opEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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ᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
(HomologicalComplex.opEquivalence V c).unitIso = HomologicalComplex.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]
:
(HomologicalComplex.opEquivalence V c).functor = HomologicalComplex.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]
:
(HomologicalComplex.opEquivalence V c).counitIso = HomologicalComplex.opCounitIso V c
@[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]
:
(HomologicalComplex.opEquivalence V c).inverse = HomologicalComplex.opInverse 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 : ι),
((HomologicalComplex.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)ᵒᵖ)
:
(HomologicalComplex.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
(HomologicalComplex.unopInverse V c).obj X = Opposite.op X.opSymm
@[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),
(HomologicalComplex.unopInverse V c).map f = Quiver.Hom.op { f := fun (i : ι) => (f.f i).op, comm' := ⋯ }
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)ᵒᵖ ≅ (HomologicalComplex.unopFunctor V c).comp (HomologicalComplex.unopInverse V c)
Auxiliary definition for unopEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HomologicalComplex.unopCounitIso
{ι : Type u_1}
(V : Type u_2)
[CategoryTheory.Category.{u_3, u_2} V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasZeroMorphisms V]
:
(HomologicalComplex.unopInverse V c).comp (HomologicalComplex.unopFunctor V c) ≅ CategoryTheory.Functor.id (HomologicalComplex V c.symm)
Auxiliary definition for unopEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
(HomologicalComplex.unopEquivalence V c).counitIso = HomologicalComplex.unopCounitIso 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]
:
(HomologicalComplex.unopEquivalence V c).unitIso = HomologicalComplex.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]
:
(HomologicalComplex.unopEquivalence V c).inverse = HomologicalComplex.unopInverse V c
@[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]
:
(HomologicalComplex.unopEquivalence V c).functor = HomologicalComplex.unopFunctor 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
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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.
Equations
- K.homologyOp i = (K.sc i).homologyOpIso
Instances For
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.
Equations
- K.homologyUnop i = (K.unop.homologyOp i).unop
Instances For
instance
HomologicalComplex.opFunctor_additive
{ι : Type u_1}
{V : Type u_2}
[CategoryTheory.Category.{u_3, u_2} V]
{c : ComplexShape ι}
[CategoryTheory.Preadditive V]
:
(HomologicalComplex.opFunctor V c).Additive
Equations
- ⋯ = ⋯
instance
HomologicalComplex.unopFunctor_additive
{ι : Type u_1}
{V : Type u_2}
[CategoryTheory.Category.{u_3, u_2} V]
{c : ComplexShape ι}
[CategoryTheory.Preadditive V]
:
(HomologicalComplex.unopFunctor V c).Additive
Equations
- ⋯ = ⋯