Documentation

Mathlib.Algebra.Homology.TotalComplexSymmetry

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.

source
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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) :
(HomologicalComplex₂.total (HomologicalComplex₂.flip K) c).X j ≅ (HomologicalComplex₂.total K c).X j

Auxiliary definition for totalFlipIso.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c) j' ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ (HomologicalComplex₂.flip K) c j j') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j').hom h)
    source
    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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j).hom (HomologicalComplex₂.D₁ K c j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ (HomologicalComplex₂.flip K) c j j') (HomologicalComplex₂.totalFlipIsoX K c j').hom
    source
    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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c) j' ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ (HomologicalComplex₂.flip K) c j j') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j').hom h)
    source
    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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalFlipIsoX K c j).hom (HomologicalComplex₂.D₂ K c j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ (HomologicalComplex₂.flip K) c j j') (HomologicalComplex₂.totalFlipIsoX K c j').hom
    source
    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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] :
    HomologicalComplex₂.total (HomologicalComplex₂.flip K) c ≅ HomologicalComplex₂.total K 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
    Instances For
      source
      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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c) j' ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ (HomologicalComplex₂.flip K) c j j') (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j') h)
      source
      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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) :
      CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j) (HomologicalComplex₂.D₁ K c j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ (HomologicalComplex₂.flip K) c j j') ((HomologicalComplex₂.totalFlipIso K c).hom.f j')
      source
      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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c) j' ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ (HomologicalComplex₂.flip K) c j j') (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j') h)
      source
      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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (j : J) (j' : J) :
      CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j) (HomologicalComplex₂.D₂ K c j j') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ (HomologicalComplex₂.flip K) c j j') ((HomologicalComplex₂.totalFlipIso K c).hom.f j')
      source
      @[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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₂ c₁ c (i₂, i₁) = j) {Z : C} (h : (HomologicalComplex₂.total K c).X j ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal (HomologicalComplex₂.flip K) c i₂ i₁ j h✝) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).hom.f j) h) = CategoryTheory.CategoryStruct.comp (ComplexShape.σ c₁ c₂ c i₁ i₂ • HomologicalComplex₂.ιTotal K c i₁ i₂ j ⋯) h
      source
      @[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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₂ c₁ c (i₂, i₁) = j) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal (HomologicalComplex₂.flip K) c i₂ i₁ j h) ((HomologicalComplex₂.totalFlipIso K c).hom.f j) = ComplexShape.σ c₁ c₂ c i₁ i₂ • HomologicalComplex₂.ιTotal K c i₁ i₂ j ⋯
      source
      @[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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) {Z : C} (h : (HomologicalComplex₂.total (HomologicalComplex₂.flip K) c).X j ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c i₁ i₂ j h✝) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.totalFlipIso K c).inv.f j) h) = CategoryTheory.CategoryStruct.comp (ComplexShape.σ c₁ c₂ c i₁ i₂ • HomologicalComplex₂.ιTotal (HomologicalComplex₂.flip K) c i₂ i₁ j ⋯) h
      source
      @[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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c i₁ i₂ j h) ((HomologicalComplex₂.totalFlipIso K c).inv.f j) = ComplexShape.σ c₁ c₂ c i₁ i₂ • HomologicalComplex₂.ιTotal (HomologicalComplex₂.flip K) c i₂ i₁ j ⋯
      source
      instance HomologicalComplex₂.instHasTotalFlipPreadditiveHasZeroMorphismsFlip {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] [HomologicalComplex₂.HasTotal K c] :
      HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip (HomologicalComplex₂.flip K)) c
      Equations
      • ⋯ = ⋯
      source
      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] [HomologicalComplex₂.HasTotal K c] [HomologicalComplex₂.HasTotal (HomologicalComplex₂.flip K) c] [DecidableEq J] [TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c] :
      HomologicalComplex₂.totalFlipIso (HomologicalComplex₂.flip K) c = (HomologicalComplex₂.totalFlipIso K c).symm