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
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
source
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
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] [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
    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] [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
    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] [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)
    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] [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
    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] [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)
    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] [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
    Instances For
      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] [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')
      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] [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)
      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] [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')
      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] [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)
      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] [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 ⋯
      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] [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✝
      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] [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 ⋯
      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] [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✝
      source
      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
      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] [K.HasTotal c] [DecidableEq J] [TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c] :
      K.flip.totalFlipIso c = (K.totalFlipIso c).symm