The symmetry of the total complex of a bicomplex
Let K : HomologicalComplex₂ C c₁ c₂ be a bicomplex. If we assume both
[TotalComplexShape c₁ c₂ c] and [TotalComplexShape c₂ c₁ c], we may form
the total complex K.total c and K.flip.total c.
In this file, we show that if we assume [TotalComplexShapeSymmetry c₁ c₂ c],
then there is an isomorphism K.totalFlipIso c : K.flip.total c ≅ K.total c.
Moreover, if we also have [TotalComplexShapeSymmetry c₂ c₁ c] and that the signs
are compatible [TotalComplexShapeSymmetrySymmetry c₁ c₂ c], then the isomorphisms
K.totalFlipIso c and K.flip.totalFlipIso c are inverse to each other.
instance
HomologicalComplex₂.instHasTotalFlip
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
:
K.flip.HasTotal c
Equations
- ⋯ = ⋯
theorem
HomologicalComplex₂.flip_hasTotal_iff
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
:
K.flip.HasTotal c ↔ K.HasTotal c
noncomputable def
HomologicalComplex₂.totalFlipIsoX
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j : J)
:
(K.flip.total c).X j ≅ (K.total c).X j
Auxiliary definition for totalFlipIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex₂.totalFlipIsoX_hom_D₁
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
:
CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (K.D₁ c j j') = CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j') (K.totalFlipIsoX c j').hom
theorem
HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (CategoryTheory.CategoryStruct.comp (K.D₁ c j j') h) = CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j')
(CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j').hom h)
theorem
HomologicalComplex₂.totalFlipIsoX_hom_D₂
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
:
CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (K.D₂ c j j') = CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j') (K.totalFlipIsoX c j').hom
theorem
HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (CategoryTheory.CategoryStruct.comp (K.D₂ c j j') h) = CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j')
(CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j').hom h)
noncomputable def
HomologicalComplex₂.totalFlipIso
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
:
K.flip.total c ≅ K.total c
The symmetry isomorphism K.flip.total c ≅ K.total c of the total complex of a
bicomplex when we have [TotalComplexShapeSymmetry c₁ c₂ c].
Equations
- K.totalFlipIso c = HomologicalComplex.Hom.isoOfComponents (K.totalFlipIsoX c) ⋯
Instances For
theorem
HomologicalComplex₂.totalFlipIso_hom_f_D₁
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
:
CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (K.D₁ c j j') = CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j') ((K.totalFlipIso c).hom.f j')
theorem
HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (CategoryTheory.CategoryStruct.comp (K.D₁ c j j') h) = CategoryTheory.CategoryStruct.comp (K.flip.D₂ c j j')
(CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j') h)
theorem
HomologicalComplex₂.totalFlipIso_hom_f_D₂
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
:
CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (K.D₂ c j j') = CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j') ((K.totalFlipIso c).hom.f j')
theorem
HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(j j' : J)
{Z : C}
(h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) (CategoryTheory.CategoryStruct.comp (K.D₂ c j j') h) = CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j')
(CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j') h)
@[simp]
theorem
HomologicalComplex₂.ιTotal_totalFlipIso_f_hom
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₂.π c₁ c (i₂, i₁) = j)
:
CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) ((K.totalFlipIso c).hom.f j) = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯
@[simp]
theorem
HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₂.π c₁ c (i₂, i₁) = j)
{Z : C}
(h✝ : (K.total c).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h)
(CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) h✝) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) h✝
@[simp]
theorem
HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) ((K.totalFlipIso c).inv.f j) = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯
@[simp]
theorem
HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
{Z : C}
(h✝ : (K.flip.total c).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h)
(CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).inv.f j) h✝) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) h✝
instance
HomologicalComplex₂.instHasTotalFlip_1
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K.HasTotal c]
:
K.flip.flip.HasTotal c
Equations
- ⋯ = ⋯
theorem
HomologicalComplex₂.flip_totalFlipIso
{C : Type u_1}
{I₁ : Type u_2}
{I₂ : Type u_3}
{J : Type u_4}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.Preadditive C]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
(K : HomologicalComplex₂ C c₁ c₂)
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[TotalComplexShape c₂ c₁ c]
[TotalComplexShapeSymmetry c₁ c₂ c]
[K.HasTotal c]
[DecidableEq J]
[TotalComplexShapeSymmetry c₂ c₁ c]
[TotalComplexShapeSymmetrySymmetry c₁ c₂ c]
:
K.flip.totalFlipIso c = (K.totalFlipIso c).symm