feat(Algebra/Homology): the symmetry of the total complex (#10770)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib.lean

@@ -293,6 +293,7 @@ import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 import Mathlib.Algebra.Homology.Single
 import Mathlib.Algebra.Homology.SingleHomology
 import Mathlib.Algebra.Homology.TotalComplex
+import Mathlib.Algebra.Homology.TotalComplexSymmetry
 import Mathlib.Algebra.Invertible.Basic
 import Mathlib.Algebra.Invertible.Defs
 import Mathlib.Algebra.Invertible.GroupWithZero

Mathlib/Algebra/Homology/ComplexShapeSigns.lean

@@ -21,7 +21,7 @@ In particular, we construct an instance of `TotalComplexShape c c c` when `c : C
 and `I` is an additive monoid equipped with a group homomorphism `ε' : Multiplicative I → ℤˣ`
 satisfying certain properties (see `ComplexShape.TensorSigns`).
 
-TODO @joelriou: add more classes for the symmetry of the total complex, the associativity, etc.
+TODO @joelriou: add more classes for the associativity of the total complex, etc.
 
 -/
 
@@ -165,3 +165,75 @@ lemma ε_up_ℤ (n : ℤ) : (ComplexShape.up ℤ).ε n = n.negOnePow := rfl
 end
 
 end ComplexShape
+
+/-- A total complex shape symmetry contains the data and properties which allow the
+identification of the two total complex functors
+`HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂`
+and `HomologicalComplex₂ C c₂ c₁ ⥤ HomologicalComplex C c₁₂` via the flip. -/
+class TotalComplexShapeSymmetry [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂] where
+  symm (i₁ : I₁) (i₂ : I₂) : ComplexShape.π c₂ c₁ c₁₂ ⟨i₂, i₁⟩ = ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩
+  /-- the signs involved in the symmetry isomorphism of the total complex -/
+  σ (i₁ : I₁) (i₂ : I₂) : ℤˣ
+  σ_ε₁ {i₁ i₁' : I₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : I₂) :
+    σ i₁ i₂ * ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ComplexShape.ε₂ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ i₁' i₂
+  σ_ε₂ (i₁ : I₁) {i₂ i₂' : I₂} (h₂ : c₂.Rel i₂ i₂') :
+    σ i₁ i₂ * ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ComplexShape.ε₁ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ i₁ i₂'
+
+namespace ComplexShape
+
+variable [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂]
+  [TotalComplexShapeSymmetry c₁ c₂ c₁₂]
+
+/-- The signs involved in the symmetry isomorphism of the total complex. -/
+abbrev σ (i₁ : I₁) (i₂ : I₂) : ℤˣ := TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂
+
+lemma π_symm (i₁ : I₁) (i₂ : I₂) :
+    π c₂ c₁ c₁₂ ⟨i₂, i₁⟩ = π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ := by
+  apply TotalComplexShapeSymmetry.symm
+
+variable {c₁}
+
+lemma σ_ε₁ {i₁ i₁' : I₁} (h₁ : c₁.Rel i₁ i₁') (i₂ : I₂) :
+    σ c₁ c₂ c₁₂ i₁ i₂ * ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ε₂ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ c₁ c₂ c₁₂ i₁' i₂ :=
+  TotalComplexShapeSymmetry.σ_ε₁ h₁ i₂
+
+variable (c₁) {c₂}
+
+lemma σ_ε₂ (i₁ : I₁) {i₂ i₂' : I₂} (h₂ : c₂.Rel i₂ i₂') :
+    σ c₁ c₂ c₁₂ i₁ i₂ * ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ε₁ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ c₁ c₂ c₁₂ i₁ i₂' :=
+  TotalComplexShapeSymmetry.σ_ε₂ i₁ h₂
+
+@[simps]
+instance : TotalComplexShapeSymmetry (up ℤ) (up ℤ) (up ℤ) where
+  symm p q := add_comm q p
+  σ p q := (p * q).negOnePow
+  σ_ε₁ := by
+    rintro p _ rfl q
+    dsimp
+    rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
+      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]
+  σ_ε₂ := by
+    rintro p q _ rfl
+    dsimp
+    rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]
+
+end ComplexShape
+
+/-- This typeclass expresses that the signs given by `[TotalComplexShapeSymmetry c₁ c₂ c₁₂]`
+and by `[TotalComplexShapeSymmetry c₂ c₁ c₁₂]` are compatible. -/
+class TotalComplexShapeSymmetrySymmetry [TotalComplexShape c₁ c₂ c₁₂]
+    [TotalComplexShape c₂ c₁ c₁₂] [TotalComplexShapeSymmetry c₁ c₂ c₁₂]
+    [TotalComplexShapeSymmetry c₂ c₁ c₁₂] : Prop where
+  σ_symm i₁ i₂ : ComplexShape.σ c₂ c₁ c₁₂ i₂ i₁ = ComplexShape.σ c₁ c₂ c₁₂ i₁ i₂
+
+namespace ComplexShape
+
+variable [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂]
+  [TotalComplexShapeSymmetry c₁ c₂ c₁₂] [TotalComplexShapeSymmetry c₂ c₁ c₁₂]
+  [TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂]
+
+lemma σ_symm (i₁ : I₁) (i₂ : I₂) :
+    σ c₂ c₁ c₁₂ i₂ i₁ = σ c₁ c₂ c₁₂ i₁ i₂ := by
+  apply TotalComplexShapeSymmetrySymmetry.σ_symm
+
+end ComplexShape

Mathlib/Algebra/Homology/HomologicalBicomplex.lean

@@ -158,6 +158,9 @@ def flip (K : HomologicalComplex₂ C c₁ c₂) : HomologicalComplex₂ C c₂
     exact (K.X j).shape i i' w
 #align homological_complex.flip_obj HomologicalComplex₂.flip
 
+@[simp]
+lemma flip_flip (K : HomologicalComplex₂ C c₁ c₂) : K.flip.flip = K := rfl
+
 variable (C c₁ c₂)
 
 /-- Flipping a complex of complexes over the diagonal, as a functor. -/

Mathlib/Algebra/Homology/TotalComplexSymmetry.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.TotalComplex
+
+/-! 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.
+
+-/
+
+open CategoryTheory Category Limits
+
+namespace HomologicalComplex₂
+
+variable {C I₁ I₂ J : Type*} [Category C] [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] [DecidableEq J]
+
+attribute [local simp] smul_smul
+
+/-- Auxiliary definition for `totalFlipIso`. -/
+noncomputable def totalFlipIsoX (j : J) : (K.flip.total c).X j ≅ (K.total c).X j where
+  hom := K.flip.totalDesc (fun i₂ i₁ h => ComplexShape.σ c₁ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j (by
+    rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]))
+  inv := K.totalDesc (fun i₁ i₂ h => ComplexShape.σ c₁ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j (by
+    rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]))
+
+@[reassoc]
+lemma totalFlipIsoX_hom_D₁ (j j' : J) :
+    (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' =
+      K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom := by
+  by_cases h₀ : c.Rel j j'
+  · ext i₂ i₁ h₁
+    dsimp [totalFlipIsoX]
+    rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₁, ι_D₂_assoc]
+    dsimp
+    by_cases h₂ : c₁.Rel i₁ (c₁.next i₁)
+    · have h₃ : ComplexShape.π c₂ c₁ c ⟨i₂, c₁.next i₁⟩ = j' := by
+        rw [← ComplexShape.next_π₂ c₂ c i₂ h₂, h₁, c.next_eq' h₀]
+      have h₄ : ComplexShape.π c₁ c₂ c ⟨c₁.next i₁, i₂⟩ = j' := by
+        rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
+      rw [K.d₁_eq _ h₂ _ _ h₄, K.flip.d₂_eq _ _ h₂ _ h₃, Linear.units_smul_comp,
+        assoc, ι_totalDesc, Linear.comp_units_smul, smul_smul, smul_smul,
+        ComplexShape.σ_ε₁ c₂ c h₂ i₂]
+      dsimp only [flip_X_X, flip_X_d]
+    · rw [K.d₁_eq_zero _ _ _ _ h₂, K.flip.d₂_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]
+  · rw [K.D₁_shape _ _ _ h₀, K.flip.D₂_shape c _ _ h₀, zero_comp, comp_zero]
+
+@[reassoc]
+lemma totalFlipIsoX_hom_D₂ (j j' : J) :
+    (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' =
+      K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom := by
+  by_cases h₀ : c.Rel j j'
+  · ext i₂ i₁ h₁
+    dsimp [totalFlipIsoX]
+    rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₂, ι_D₁_assoc]
+    dsimp
+    by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
+    · have h₃ : ComplexShape.π c₂ c₁ c (ComplexShape.next c₂ i₂, i₁) = j' := by
+        rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
+      have h₄ : ComplexShape.π c₁ c₂ c (i₁, ComplexShape.next c₂ i₂) = j' := by
+        rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
+      rw [K.d₂_eq _ _ h₂ _ h₄, K.flip.d₁_eq _ h₂ _ _ h₃, Linear.units_smul_comp,
+        assoc, ι_totalDesc, Linear.comp_units_smul, smul_smul, smul_smul,
+        ComplexShape.σ_ε₂ c₁ c i₁ h₂]
+      rfl
+    · rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]
+  · rw [K.D₂_shape _ _ _ h₀, K.flip.D₁_shape c _ _ h₀, zero_comp, comp_zero]
+
+/-- The symmetry isomorphism `K.flip.total c ≅ K.total c` of the total complex of a
+bicomplex when we have `[TotalComplexShapeSymmetry c₁ c₂ c]`. -/
+noncomputable def totalFlipIso : K.flip.total c ≅ K.total c :=
+  HomologicalComplex.Hom.isoOfComponents (K.totalFlipIsoX c) (fun j j' _ => by
+    dsimp
+    simp only [Preadditive.comp_add, totalFlipIsoX_hom_D₁,
+      totalFlipIsoX_hom_D₂, Preadditive.add_comp]
+    rw [add_comm])
+
+@[reassoc]
+lemma totalFlipIso_hom_f_D₁ (j j' : J) :
+    (K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' =
+      K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j' := by
+  apply totalFlipIsoX_hom_D₁
+
+@[reassoc]
+lemma totalFlipIso_hom_f_D₂ (j j' : J) :
+    (K.totalFlipIso c).hom.f j ≫ K.D₂ c j j' =
+      K.flip.D₁ c j j' ≫ (K.totalFlipIso c).hom.f j' := by
+  apply totalFlipIsoX_hom_D₂
+
+@[reassoc (attr := simp)]
+lemma ιTotal_totalFlipIso_f_hom
+    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₂ c₁ c (i₂, i₁) = j) :
+    K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j =
+      ComplexShape.σ c₁ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j
+        (by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]) := by
+  simp [totalFlipIso, totalFlipIsoX]
+
+@[reassoc (attr := simp)]
+lemma ιTotal_totalFlipIso_f_inv
+    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j =
+      ComplexShape.σ c₁ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j
+        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]) := by
+  simp [totalFlipIso, totalFlipIsoX]
+
+instance : K.flip.flip.HasTotal c := (inferInstance : K.HasTotal c)
+
+section
+
+variable [TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c]
+
+lemma flip_totalFlipIso : K.flip.totalFlipIso c = (K.totalFlipIso c).symm := by
+  ext j i₁ i₂ h
+  rw [Iso.symm_hom, ιTotal_totalFlipIso_f_hom]
+  dsimp only [flip_flip]
+  rw [ιTotal_totalFlipIso_f_inv, ComplexShape.σ_symm]
+
+end
+
+end HomologicalComplex₂