diff --git a/Mathlib.lean b/Mathlib.lean
index 6b712127435b5..b16fcc98e053a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -241,6 +241,7 @@ import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.HierarchyDesign
 import Mathlib.Algebra.Homology.Additive
 import Mathlib.Algebra.Homology.Augment
+import Mathlib.Algebra.Homology.Bifunctor
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Homology.ComplexShapeSigns
 import Mathlib.Algebra.Homology.ConcreteCategory
@@ -292,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
diff --git a/Mathlib/Algebra/Homology/Bifunctor.lean b/Mathlib/Algebra/Homology/Bifunctor.lean
new file mode 100644
index 0000000000000..b826901eb5865
--- /dev/null
+++ b/Mathlib/Algebra/Homology/Bifunctor.lean
@@ -0,0 +1,156 @@
+/-
+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
+import Mathlib.CategoryTheory.GradedObject.Bifunctor
+
+/-!
+# The action of a bifunctor on homological complexes
+
+Given a bifunctor `F : C₁ ⥤ C₂ ⥤ D` and complexes shapes `c₁ : ComplexShape I₁` and
+`c₂ : ComplexShape I₂`, we define a bifunctor `mapBifunctorHomologicalComplex F c₁ c₂`
+of type `HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂`.
+
+Then, when `K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂` and
+`c : ComplexShape J` are such that we have `TotalComplexShape c₁ c₂ c`, we introduce
+a typeclass `HasMapBifunctor K₁ K₂ F c` which allows to define
+`mapBifunctor K₁ K₂ F c : HomologicalComplex D c` as the total complex of the
+bicomplex `(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂)`.
+
+-/
+
+open CategoryTheory Limits
+
+variable {C₁ C₂ D : Type*} [Category C₁] [Category C₂] [Category D]
+
+namespace CategoryTheory
+
+namespace Functor
+
+variable [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroMorphisms D]
+  (F : C₁ ⥤ C₂ ⥤ D) {I₁ I₂ J : Type*} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
+  [F.PreservesZeroMorphisms] [∀ X₁, (F.obj X₁).PreservesZeroMorphisms]
+
+variable {c₁} in
+/-- Auxiliary definition for `mapBifunctorHomologicalComplex`. -/
+@[simps!]
+def mapBifunctorHomologicalComplexObj (K₁ : HomologicalComplex C₁ c₁) :
+    HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂ where
+  obj K₂ := HomologicalComplex₂.ofGradedObject c₁ c₂
+      (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
+      (fun i₁ i₁' i₂ => (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
+      (fun i₁ i₂ i₂' => (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))
+      (fun i₁ i₁' h₁ i₂ => by
+        dsimp
+        rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app])
+      (fun i₁ i₂ i₂' h₂ => by
+        dsimp
+        rw [K₂.shape _ _ h₂, Functor.map_zero])
+      (fun i₁ i₁' i₁'' i₂ => by
+        dsimp
+        rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
+          Functor.map_zero, zero_app])
+      (fun i₁ i₂ i₂' i₂'' => by
+        dsimp
+        rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero])
+      (fun i₁ i₁' i₂ i₂' => by
+        dsimp
+        rw [NatTrans.naturality])
+  map {K₂ K₂' φ} := HomologicalComplex₂.homMk
+      (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map φ.f) (by simp) (by
+        intros
+        dsimp
+        simp only [← Functor.map_comp, φ.comm])
+  map_id K₂ := by ext; dsimp; rw [Functor.map_id]
+  map_comp f g := by ext; dsimp; rw [Functor.map_comp]
+
+/-- Given a functor `F : C₁ ⥤ C₂ ⥤ D`, this is the bifunctor which sends
+`K₁ : HomologicalComplex C₁ c₁` and `K₂ : HomologicalComplex C₂ c₂` to the bicomplex
+which is degree `(i₁, i₂)` consists of `(F.obj (K₁.X i₁)).obj (K₂.X i₂)`. -/
+@[simps! obj_obj_X_X obj_obj_X_d obj_obj_d_f obj_map_f_f map_app_f_f]
+def mapBifunctorHomologicalComplex :
+    HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂ where
+  obj := mapBifunctorHomologicalComplexObj F c₂
+  map {K₁ K₁'} f :=
+    { app := fun K₂ => HomologicalComplex₂.homMk
+        (((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X) (by
+          intros
+          dsimp
+          simp only [← NatTrans.comp_app, ← F.map_comp, f.comm]) (by simp) }
+
+variable {c₁ c₂}
+
+@[simp]
+lemma mapBifunctorHomologicalComplex_obj_obj_toGradedObject
+    (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) :
+    (((mapBifunctorHomologicalComplex F c₁ c₂).obj K₁).obj K₂).toGradedObject =
+      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X := rfl
+
+end Functor
+
+end CategoryTheory
+
+namespace HomologicalComplex
+
+variable {I₁ I₂ J : Type*} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
+  [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [Preadditive D]
+  (K₁ L₁ : HomologicalComplex C₁ c₁) (K₂ L₂ : HomologicalComplex C₂ c₂)
+  (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂)
+  (F : C₁ ⥤ C₂ ⥤ D) [F.PreservesZeroMorphisms] [∀ X₁, (F.obj X₁).PreservesZeroMorphisms]
+  (c : ComplexShape J) [TotalComplexShape c₁ c₂ c]
+
+/-- The condition that `((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂` has
+a total complex. -/
+abbrev HasMapBifunctor := (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).HasTotal c
+
+variable [HasMapBifunctor K₁ K₂ F c] [HasMapBifunctor L₁ L₂ F c] [DecidableEq J]
+
+/-- Given `K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂`,
+a bifunctor `F : C₁ ⥤ C₂ ⥤ D` and a complex shape `ComplexShape J` such that we have
+`[TotalComplexShape c₁ c₂ c]`, this `mapBifunctor K₁ K₂ F c : HomologicalComplex D c`
+is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`. -/
+noncomputable abbrev mapBifunctor : HomologicalComplex D c :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).total c
+
+/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`. -/
+noncomputable abbrev ιMapBifunctor
+    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (mapBifunctor K₁ K₂ F c).X j :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h
+
+/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`, or zero. -/
+noncomputable abbrev ιMapBifunctorOrZero (i₁ : I₁) (i₂ : I₂) (j : J) :
+    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (mapBifunctor K₁ K₂ F c).X j :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotalOrZero c i₁ i₂ j
+
+lemma ιMapBifunctorOrZero_eq (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂ j = ιMapBifunctor K₁ K₂ F c i₁ i₂ j h := dif_pos h
+
+lemma ιMapBifunctorOrZero_eq_zero (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) ≠ j) :
+    ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂ j = 0 := dif_neg h
+
+section
+
+variable {K₁ K₂ L₁ L₂}
+
+/-- The morphism `mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c` induced by
+morphisms of complexes `K₁ ⟶ L₁` and `K₂ ⟶ L₂`. -/
+noncomputable def mapBifunctorMap : mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c :=
+  HomologicalComplex₂.total.map (((F.mapBifunctorHomologicalComplex c₁ c₂).map f₁).app K₂ ≫
+    ((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).map f₂) c
+
+@[reassoc (attr := simp)]
+lemma ι_mapBifunctorMap (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
+      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
+        ιMapBifunctor L₁ L₂ F c i₁ i₂ j h := by
+  simp [mapBifunctorMap]
+
+end
+
+end HomologicalComplex
diff --git a/Mathlib/Algebra/Homology/ComplexShapeSigns.lean b/Mathlib/Algebra/Homology/ComplexShapeSigns.lean
index ec6aa21df561c..8ae25ebe46fc2 100644
--- a/Mathlib/Algebra/Homology/ComplexShapeSigns.lean
+++ b/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
diff --git a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
index 4847614756fc7..f67dad01870b6 100644
--- a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
+++ b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
@@ -68,6 +68,61 @@ instance : Faithful (toGradedObjectFunctor C c₁ c₂) where
     ext i₁ i₂
     exact congr_fun h ⟨i₁, i₂⟩
 
+section OfGradedObject
+
+variable (c₁ c₂)
+variable (X : GradedObject (I₁ × I₂) C)
+    (d₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), X ⟨i₁, i₂⟩ ⟶ X ⟨i₁', i₂⟩)
+    (d₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), X ⟨i₁, i₂⟩ ⟶ X ⟨i₁, i₂'⟩)
+    (shape₁ : ∀ (i₁ i₁' : I₁) (_ : ¬c₁.Rel i₁ i₁') (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
+    (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂) (_ : ¬c₂.Rel i₂ i₂'), d₂ i₁ i₂ i₂' = 0)
+    (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0)
+    (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0)
+    (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' =
+      d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂')
+
+/-- Constructor for bicomplexes taking as inputs a graded object, horizontal differentials
+and vertical differentials satisfying suitable relations. -/
+@[simps]
+def ofGradedObject :
+    HomologicalComplex₂ C c₁ c₂ where
+  X i₁ :=
+    { X := fun i₂ => X ⟨i₁, i₂⟩
+      d := fun i₂ i₂' => d₂ i₁ i₂ i₂'
+      shape := shape₂ i₁
+      d_comp_d' := by intros; apply d₂_comp_d₂ }
+  d i₁ i₁' :=
+    { f := fun i₂ => d₁ i₁ i₁' i₂
+      comm' := by intros; apply comm }
+  shape i₁ i₁' h := by
+    ext i₂
+    exact shape₁ i₁ i₁' h i₂
+  d_comp_d' i₁ i₁' i₁'' _ _ := by ext i₂; apply d₁_comp_d₁
+
+@[simp]
+lemma ofGradedObject_toGradedObject :
+    (ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X :=
+  rfl
+
+end OfGradedObject
+
+/-- Constructor for a morphism `K ⟶ L` in the category `HomologicalComplex₂ C c₁ c₂` which
+takes as inputs a morphism `f : K.toGradedObject ⟶ L.toGradedObject` and
+the compatibilites with both horizontal and vertical differentials. -/
+@[simps!]
+def homMk {K L : HomologicalComplex₂ C c₁ c₂}
+    (f : K.toGradedObject ⟶ L.toGradedObject)
+    (comm₁ : ∀ i₁ i₁' i₂, c₁.Rel i₁ i₁' →
+      f ⟨i₁, i₂⟩ ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f ⟨i₁', i₂⟩)
+    (comm₂ : ∀ i₁ i₂ i₂', c₂.Rel i₂ i₂' →
+      f ⟨i₁, i₂⟩ ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f ⟨i₁, i₂'⟩) : K ⟶ L where
+  f i₁ :=
+    { f := fun i₂ => f ⟨i₁, i₂⟩
+      comm' := comm₂ i₁ }
+  comm' i₁ i₁' h₁ := by
+    ext i₂
+    exact comm₁ i₁ i₁' i₂ h₁
+
 lemma shape_f (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (h : ¬ c₁.Rel i₁ i₁') (i₂ : I₂) :
     (K.d i₁ i₁').f i₂ = 0 := by
   rw [K.shape _ _ h, zero_f]
@@ -103,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. -/
diff --git a/Mathlib/Algebra/Homology/TotalComplexSymmetry.lean b/Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
new file mode 100644
index 0000000000000..4d0726411fed0
--- /dev/null
+++ b/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₂
diff --git a/Mathlib/Analysis/Normed/Group/Tannery.lean b/Mathlib/Analysis/Normed/Group/Tannery.lean
index 117cbde2562d4..f1d4eeaeccaeb 100644
--- a/Mathlib/Analysis/Normed/Group/Tannery.lean
+++ b/Mathlib/Analysis/Normed/Group/Tannery.lean
@@ -23,7 +23,7 @@ open Filter Topology
 open scoped BigOperators
 
 /-- **Tannery's theorem**: topological sums commute with termwise limits, when the norms of the
-summands are uniformly bounded by a summable function.
+summands are eventually uniformly bounded by a summable function.
 
 (This is the special case of the Lebesgue dominated convergence theorem for the counting measure
 on a discrete set. However, we prove it under somewhat weaker assumptions than the general
@@ -39,7 +39,7 @@ lemma tendsto_tsum_of_dominated_convergence {α β G : Type*} {𝓕 : Filter α}
     [NormedAddCommGroup G] [CompleteSpace G]
     {f : α → β → G} {g : β → G} {bound : β → ℝ} (h_sum : Summable bound)
     (hab : ∀ k : β, Tendsto (f · k) 𝓕 (𝓝 (g k)))
-    (h_bound : ∀ n k, ‖f n k‖ ≤ bound k) :
+    (h_bound : ∀ᶠ n in 𝓕, ∀ k, ‖f n k‖ ≤ bound k) :
     Tendsto (∑' k, f · k) 𝓕 (𝓝 (∑' k, g k)) := by
   -- WLOG β is nonempty
   rcases isEmpty_or_nonempty β
@@ -49,11 +49,12 @@ lemma tendsto_tsum_of_dominated_convergence {α β G : Type*} {𝓕 : Filter α}
   · simp only [tendsto_bot]
   -- Auxiliary lemmas
   have h_g_le (k : β) : ‖g k‖ ≤ bound k :=
-    le_of_tendsto (tendsto_norm.comp (hab k)) <| eventually_of_forall (h_bound · k)
+    le_of_tendsto (tendsto_norm.comp (hab k)) <| h_bound.mono (fun n h => h k)
   have h_sumg : Summable (‖g ·‖) :=
     h_sum.of_norm_bounded _ (fun k ↦ (norm_norm (g k)).symm ▸ h_g_le k)
-  have h_suma (n : α) : Summable (‖f n ·‖) :=
-    h_sum.of_norm_bounded _ <| by simpa only [norm_norm] using h_bound n
+  have h_suma : ∀ᶠ n in 𝓕, Summable (‖f n ·‖) := by
+    filter_upwards [h_bound] with n h
+    exact h_sum.of_norm_bounded _ <| by simpa only [norm_norm] using h
   -- Now main proof, by an `ε / 3` argument
   rw [Metric.tendsto_nhds]
   intro ε hε
@@ -68,15 +69,15 @@ lemma tendsto_tsum_of_dominated_convergence {α β G : Type*} {𝓕 : Filter α}
     simpa only [sum_add_tsum_compl h_sum, eq_sub_iff_add_eq'] using hS.tsum_eq
   have h2 : Tendsto (∑ k in T, f · k) 𝓕 (𝓝 (T.sum g)) := tendsto_finset_sum _ (fun i _ ↦ hab i)
   rw [Metric.tendsto_nhds] at h2
-  refine (h2 (ε / 3) (by positivity)).mp (eventually_of_forall (fun n hn ↦ ?_))
-  rw [dist_eq_norm, ← tsum_sub (h_suma n).of_norm h_sumg.of_norm,
-    ← sum_add_tsum_compl (s := T) ((h_suma n).of_norm.sub h_sumg.of_norm),
+  filter_upwards [h2 (ε / 3) (by positivity), h_suma, h_bound] with n hn h_suma h_bound
+  rw [dist_eq_norm, ← tsum_sub h_suma.of_norm h_sumg.of_norm,
+    ← sum_add_tsum_compl (s := T) (h_suma.of_norm.sub h_sumg.of_norm),
     (by ring : ε = ε / 3 + (ε / 3 + ε / 3))]
   refine (norm_add_le _ _).trans_lt (add_lt_add ?_ ?_)
   · simpa only [dist_eq_norm, Finset.sum_sub_distrib] using hn
-  · rw [tsum_sub ((h_suma n).subtype _).of_norm (h_sumg.subtype _).of_norm]
+  · rw [tsum_sub (h_suma.subtype _).of_norm (h_sumg.subtype _).of_norm]
     refine (norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)
-    · refine ((norm_tsum_le_tsum_norm ((h_suma n).subtype _)).trans ?_).trans_lt h1
-      exact tsum_le_tsum (h_bound n ·) ((h_suma n).subtype _) (h_sum.subtype _)
+    · refine ((norm_tsum_le_tsum_norm (h_suma.subtype _)).trans ?_).trans_lt h1
+      exact tsum_le_tsum (h_bound ·) (h_suma.subtype _) (h_sum.subtype _)
     · refine ((norm_tsum_le_tsum_norm <| h_sumg.subtype _).trans ?_).trans_lt h1
       exact tsum_le_tsum (h_g_le ·) (h_sumg.subtype _) (h_sum.subtype _)
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index d47a7aa7f7f9c..a23c77a6e3ed4 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -72,7 +72,7 @@ open Rat
 open multiplicity
 
 /-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
-that `p^k` divides `z`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
+that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
 def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
   if h : p ≠ 1 ∧ 0 < n then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h) else 0
 #align padic_val_nat padicValNat