mathlib3 documentation

algebra.homology.opposite

Opposite categories of complexes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 analagous 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 analagous result for unop).

Implementation notes #

It is convenient to define both op and op_symm; 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

source
theorem image_to_kernel_op {V : Type u_1} [category_theory.category V] [category_theory.abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
image_to_kernel g.op f.op _ = (category_theory.limits.image_subobject_iso g.op ≪≫ (category_theory.image_op_op g).symm).hom ≫ (category_theory.limits.cokernel.desc f (category_theory.limits.factor_thru_image g) _).op ≫ (category_theory.limits.kernel_subobject_iso f.op ≪≫ category_theory.kernel_op_op f).inv
source
theorem image_to_kernel_unop {V : Type u_1} [category_theory.category V] [category_theory.abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
image_to_kernel g.unop f.unop _ = (category_theory.limits.image_subobject_iso g.unop ≪≫ (category_theory.image_unop_unop g).symm).hom ≫ (category_theory.limits.cokernel.desc f (category_theory.limits.factor_thru_image g) _).unop ≫ (category_theory.limits.kernel_subobject_iso f.unop ≪≫ category_theory.kernel_unop_unop f).inv
source
noncomputable def homology_op {V : Type u_1} [category_theory.category V] [category_theory.abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
homology g.op f.op _ ≅ opposite.op (homology f g w)

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

Equations
source
noncomputable def homology_unop {V : Type u_1} [category_theory.category V] [category_theory.abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
homology g.unop f.unop _ ≅ opposite.unop (homology f g w)

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.

Equations
source
@[simp]
theorem homological_complex.op_X {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c) (i : ι) :
X.op.X i = opposite.op (X.X i)
source
@[simp]
theorem homological_complex.op_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c) (i j : ι) :
X.op.d i j = (X.d j i).op
source
@[protected]
def homological_complex.op {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c) :
homological_complex Vᵒᵖ c.symm

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

Equations
source
@[protected]
def homological_complex.op_symm {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c.symm) :
homological_complex Vᵒᵖ c

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

Equations
source
@[simp]
theorem homological_complex.op_symm_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c.symm) (i j : ι) :
X.op_symm.d i j = (X.d j i).op
source
@[simp]
theorem homological_complex.op_symm_X {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex V c.symm) (i : ι) :
X.op_symm.X i = opposite.op (X.X i)
source
@[simp]
theorem homological_complex.unop_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c) (i j : ι) :
X.unop.d i j = (X.d j i).unop
source
@[protected]
def homological_complex.unop {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c) :
homological_complex V c.symm

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

Equations
source
@[simp]
theorem homological_complex.unop_X {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c) (i : ι) :
X.unop.X i = opposite.unop (X.X i)
source
@[protected]
def homological_complex.unop_symm {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c.symm) :
homological_complex V c

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

Equations
source
@[simp]
theorem homological_complex.unop_symm_X {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c.symm) (i : ι) :
X.unop_symm.X i = opposite.unop (X.X i)
source
@[simp]
theorem homological_complex.unop_symm_d {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c.symm) (i j : ι) :
X.unop_symm.d i j = (X.d j i).unop
source
@[simp]
theorem homological_complex.op_functor_map_f {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X Y : (homological_complex V c)ᵒᵖ) (f : X ⟶ Y) (i : ι) :
((homological_complex.op_functor V c).map f).f i = (f.unop.f i).op
source
def homological_complex.op_functor {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex V c)ᵒᵖ ⥤ homological_complex Vᵒᵖ c.symm

Auxilliary definition for op_equivalence.

Equations
Instances for homological_complex.op_functor
source
@[simp]
theorem homological_complex.op_functor_obj {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X : (homological_complex V c)ᵒᵖ) :
(homological_complex.op_functor V c).obj X = (opposite.unop X).op
source
@[simp]
theorem homological_complex.op_inverse_obj {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X : homological_complex Vᵒᵖ c.symm) :
(homological_complex.op_inverse V c).obj X = opposite.op X.unop_symm
source
def homological_complex.op_inverse {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
homological_complex Vᵒᵖ c.symm ⥤ (homological_complex V c)ᵒᵖ

Auxilliary definition for op_equivalence.

Equations
source
@[simp]
theorem homological_complex.op_inverse_map {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X Y : homological_complex Vᵒᵖ c.symm) (f : X ⟶ Y) :
(homological_complex.op_inverse V c).map f = quiver.hom.op {f := λ (i : ι), (f.f i).unop, comm' := _}
source
def homological_complex.op_unit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
𝟭 (homological_complex V c)ᵒᵖ ≅ homological_complex.op_functor V c ⋙ homological_complex.op_inverse V c

Auxilliary definition for op_equivalence.

Equations
source
def homological_complex.op_counit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
homological_complex.op_inverse V c ⋙ homological_complex.op_functor V c ≅ 𝟭 (homological_complex Vᵒᵖ c.symm)

Auxilliary definition for op_equivalence.

Equations
source
@[simp]
theorem homological_complex.op_equivalence_counit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.op_equivalence V c).counit_iso = homological_complex.op_counit_iso V c
source
@[simp]
theorem homological_complex.op_equivalence_unit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.op_equivalence V c).unit_iso = homological_complex.op_unit_iso V c
source
def homological_complex.op_equivalence {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex V c)ᵒᵖ ≌ homological_complex 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
source
@[simp]
theorem homological_complex.op_equivalence_functor {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.op_equivalence V c).functor = homological_complex.op_functor V c
source
@[simp]
theorem homological_complex.op_equivalence_inverse {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.op_equivalence V c).inverse = homological_complex.op_inverse V c
source
def homological_complex.unop_functor {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex Vᵒᵖ c)ᵒᵖ ⥤ homological_complex V c.symm

Auxilliary definition for unop_equivalence.

Equations
Instances for homological_complex.unop_functor
source
@[simp]
theorem homological_complex.unop_functor_obj {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X : (homological_complex Vᵒᵖ c)ᵒᵖ) :
(homological_complex.unop_functor V c).obj X = (opposite.unop X).unop
source
@[simp]
theorem homological_complex.unop_functor_map_f {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X Y : (homological_complex Vᵒᵖ c)ᵒᵖ) (f : X ⟶ Y) (i : ι) :
((homological_complex.unop_functor V c).map f).f i = (f.unop.f i).unop
source
@[simp]
theorem homological_complex.unop_inverse_map {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X Y : homological_complex V c.symm) (f : X ⟶ Y) :
(homological_complex.unop_inverse V c).map f = quiver.hom.op {f := λ (i : ι), (f.f i).op, comm' := _}
source
@[simp]
theorem homological_complex.unop_inverse_obj {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] (X : homological_complex V c.symm) :
(homological_complex.unop_inverse V c).obj X = opposite.op X.op_symm
source
def homological_complex.unop_inverse {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
homological_complex V c.symm ⥤ (homological_complex Vᵒᵖ c)ᵒᵖ

Auxilliary definition for unop_equivalence.

Equations
source
def homological_complex.unop_unit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
𝟭 (homological_complex Vᵒᵖ c)ᵒᵖ ≅ homological_complex.unop_functor V c ⋙ homological_complex.unop_inverse V c

Auxilliary definition for unop_equivalence.

Equations
source
def homological_complex.unop_counit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
homological_complex.unop_inverse V c ⋙ homological_complex.unop_functor V c ≅ 𝟭 (homological_complex V c.symm)

Auxilliary definition for unop_equivalence.

Equations
source
@[simp]
theorem homological_complex.unop_equivalence_counit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.unop_equivalence V c).counit_iso = homological_complex.unop_counit_iso V c
source
def homological_complex.unop_equivalence {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex Vᵒᵖ c)ᵒᵖ ≌ homological_complex 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
source
@[simp]
theorem homological_complex.unop_equivalence_unit_iso {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.unop_equivalence V c).unit_iso = homological_complex.unop_unit_iso V c
source
@[simp]
theorem homological_complex.unop_equivalence_inverse {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.unop_equivalence V c).inverse = homological_complex.unop_inverse V c
source
@[simp]
theorem homological_complex.unop_equivalence_functor {ι : Type u_1} (V : Type u_2) [category_theory.category V] (c : complex_shape ι) [category_theory.preadditive V] :
(homological_complex.unop_equivalence V c).functor = homological_complex.unop_functor V c
source
@[protected, instance]
def homological_complex.op_functor_additive {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] :
(homological_complex.op_functor V c).additive
source
@[protected, instance]
def homological_complex.unop_functor_additive {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.preadditive V] :
(homological_complex.unop_functor V c).additive
source
noncomputable def homological_complex.homology_op_def {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (C : homological_complex V c) (i : ι) :
C.op.homology i ≅ homology (C.d_from i).op (C.d_to i).op _

Auxilliary tautological definition for homology_op.

Equations
source
noncomputable def homological_complex.homology_op {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (C : homological_complex V c) (i : ι) :
C.op.homology i ≅ opposite.op (C.homology i)

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.

Equations
source
noncomputable def homological_complex.homology_unop_def {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (i : ι) (C : homological_complex Vᵒᵖ c) :
C.unop.homology i ≅ homology (C.d_from i).unop (C.d_to i).unop _

Auxilliary tautological definition for homology_unop.

Equations
source
noncomputable def homological_complex.homology_unop {ι : Type u_1} {V : Type u_2} [category_theory.category V] {c : complex_shape ι} [category_theory.abelian V] (i : ι) (C : homological_complex Vᵒᵖ c) :
C.unop.homology i ≅ opposite.unop (C.homology i)

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.

Equations