Loogle!

Result

Found 90 declarations mentioning CategoryTheory.GradedObject.mapObj.

• CategoryTheory.GradedObject.mapObj 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] : CategoryTheory.GradedObject J C
• CategoryTheory.GradedObject.ιMapObj 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] (i : I) (j : J) (hij : p i = j) : X i ⟶ X.mapObj p j
• CategoryTheory.GradedObject.ιMapObjOrZero 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) : X i ⟶ X.mapObj p j
• CategoryTheory.GradedObject.hasMap_comp 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) [(X.mapObj p).HasMap q] : X.HasMap r
• CategoryTheory.GradedObject.descMapObj 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) : X.mapObj p j ⟶ A
• CategoryTheory.GradedObject.mapIso 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] : X.mapObj p ≅ Y.mapObj p
• CategoryTheory.GradedObject.ιMapObjOrZero_eq 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i = j) : X.ιMapObjOrZero p i j = X.ιMapObj p i j h
• CategoryTheory.GradedObject.mapMap 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] : X.mapObj p ⟶ Y.mapObj p
• CategoryTheory.GradedObject.map_obj 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} (C : Type u_4) [CategoryTheory.Category.{v_1, u_4} C] (p : I → J) [∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C] (X : CategoryTheory.GradedObject I C) : (CategoryTheory.GradedObject.map C p).obj X = X.mapObj p
• CategoryTheory.GradedObject.mapMap_id 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] : CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.id X) p = CategoryTheory.CategoryStruct.id (X.mapObj p)
• CategoryTheory.GradedObject.ι_descMapObj 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
• CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i ≠ j) : X.ιMapObjOrZero p i j = 0
• CategoryTheory.GradedObject.mapIso_hom 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : J) : (CategoryTheory.GradedObject.mapIso e p).hom i = CategoryTheory.GradedObject.mapMap e.hom p i
• CategoryTheory.GradedObject.mapIso_inv 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : J) : (CategoryTheory.GradedObject.mapIso e p).inv i = CategoryTheory.GradedObject.mapMap e.inv p i
• CategoryTheory.GradedObject.ι_descMapObj_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.CategoryStruct.comp (X.descMapObj p φ) h) = CategoryTheory.CategoryStruct.comp (φ i hi) h
• CategoryTheory.GradedObject.congr_mapMap 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (p : I → J) [X.HasMap p] [Y.HasMap p] (φ₁ φ₂ : X ⟶ Y) (h : φ₁ = φ₂) : CategoryTheory.GradedObject.mapMap φ₁ p = CategoryTheory.GradedObject.mapMap φ₂ p
• CategoryTheory.GradedObject.mapObj_ext 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (f g : X.mapObj p j ⟶ A) (hfg : ∀ (i : I) (hij : p i = j), CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g) : f = g
• CategoryTheory.GradedObject.CofanMapObjFun.iso 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) : c.pt ≅ X.mapObj p j
• CategoryTheory.GradedObject.mapObj_ext_iff 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} [X.HasMap p] {A : C} {j : J} {f g : X.mapObj p j ⟶ A} : f = g ↔ ∀ (i : I) (hij : p i = j), CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g
• CategoryTheory.GradedObject.ι_mapMap 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryTheory.GradedObject.mapMap φ p j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)
• CategoryTheory.GradedObject.ιMapObjOrZero_mapMap 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) : CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryTheory.GradedObject.mapMap φ p j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)
• CategoryTheory.GradedObject.map_map 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} (C : Type u_4) [CategoryTheory.Category.{v_1, u_4} C] (p : I → J) [∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C] {X✝ Y✝ : CategoryTheory.GradedObject I C} (φ : X✝ ⟶ Y✝) (i : J) : (CategoryTheory.GradedObject.map C p).map φ i = CategoryTheory.GradedObject.mapMap φ p i
• CategoryTheory.GradedObject.ι_mapMap_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p j) h) = CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (Y.ιMapObj p i j hij) h)
• CategoryTheory.GradedObject.ιMapObjOrZero_mapMap_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) {Z : C} (h : Y.mapObj p j ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p j) h) = CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (Y.ιMapObjOrZero p i j) h)
• CategoryTheory.GradedObject.mapMap_comp 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y Z : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [X.HasMap p] [Y.HasMap p] [Z.HasMap p] : CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.comp φ ψ) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p) (CategoryTheory.GradedObject.mapMap ψ p)
• CategoryTheory.GradedObject.mapMap_comp_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X Y Z : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [X.HasMap p] [Y.HasMap p] [Z.HasMap p] {Z✝ : CategoryTheory.GradedObject J C} (h : Z.mapObj p ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.comp φ ψ) p) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap ψ p) h)
• CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).inv = CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩
• CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩) (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).hom = X.ιMapObj p i j hi
• CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩) h
• CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : X.mapObj p j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).hom h) = CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) h
• HomologicalComplex₂.D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'
• HomologicalComplex₂.D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'
• HomologicalComplex₂.d₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂
• HomologicalComplex₂.d₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂
• HomologicalComplex₂.totalAux.ιMapObj_D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i.1 i.2 i₁₂'
• HomologicalComplex₂.totalAux.ιMapObj_D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i.1 i.2 i₁₂'
• HomologicalComplex₂.ι_D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i₁ i₂ i₁₂'
• HomologicalComplex₂.ι_D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i₁ i₂ i₁₂'
• HomologicalComplex₂.D₁_shape 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : K.D₁ c₁₂ i₁₂ i₁₂' = 0
• HomologicalComplex₂.D₂_shape 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : K.D₂ c₁₂ i₁₂ i₁₂' = 0
• HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C} (h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i.1 i.2 i₁₂') h✝
• HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C} (h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i.1 i.2 i₁₂') h✝
• HomologicalComplex₂.d₁_eq_zero 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₁.Rel i₁ (c₁.next i₁)) : K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
• HomologicalComplex₂.d₂_eq_zero 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₂.Rel i₂ (c₂.next i₂)) : K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
• HomologicalComplex₂.d₁_eq_zero' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
• HomologicalComplex₂.d₂_eq_zero' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = 0
• HomologicalComplex₂.ι_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂') h✝
• HomologicalComplex₂.ι_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h✝ : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h✝) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂') h✝
• HomologicalComplex₂.D₁_D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') = 0
• HomologicalComplex₂.D₂_D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') = 0
• HomologicalComplex₂.total.mapAux.mapMap_D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (L.D₁ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
• HomologicalComplex₂.total.mapAux.mapMap_D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (L.D₂ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
• HomologicalComplex₂.D₁_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h
• HomologicalComplex₂.D₂_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h
• HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (L.D₁ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
• HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (L.D₂ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
• HomologicalComplex₂.total.mapAux.d₁_mapMap 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₁ c₁₂ i₁ i₂ i₁₂)
• HomologicalComplex₂.total.mapAux.d₂_mapMap 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₂ c₁₂ i₁ i₂ i₁₂)
• HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₁ c₁₂ i₁ i₂ i₁₂) h)
• HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₂ c₁₂ i₁ i₂ i₁₂) h)
• HomologicalComplex₂.total_d 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) : (K.total c₁₂).d i₁₂ i₁₂' = K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂'
• HomologicalComplex₂.D₁_D₂ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')
• HomologicalComplex₂.D₂_D₁ 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')
• HomologicalComplex₂.D₁_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')) h
• HomologicalComplex₂.D₂_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')) h
• HomologicalComplex₂.d₂_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂)
• HomologicalComplex₂.d₂_eq 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotal c₁₂ i₁ i₂' i₁₂ h')
• HomologicalComplex₂.d₁_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂)
• HomologicalComplex₂.totalAux.d₂_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂)
• HomologicalComplex₂.d₁_eq 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotal c₁₂ i₁' i₂ i₁₂ h')
• HomologicalComplex₂.totalAux.d₂_eq 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')
• HomologicalComplex₂.totalAux.d₁_eq' 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂)
• HomologicalComplex₂.totalAux.d₁_eq 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
• HomologicalComplex₂.totalFlipIsoX_hom_D₁ 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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
• HomologicalComplex₂.totalFlipIsoX_hom_D₂ 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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
• HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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)
• HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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)
• HomologicalComplex₂.totalFlipIso_hom_f_D₁ 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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')
• HomologicalComplex₂.totalFlipIso_hom_f_D₂ 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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')
• HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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)
• HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc 📋 Mathlib.Algebra.Homology.TotalComplexSymmetry
  {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, 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)
• HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux 📋 Mathlib.Algebra.Homology.BifunctorHomotopy
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] {i₁ i₁' : I₁} (hi₁ : c₁.Rel i₁ i₁') {i₂ i₂' : I₂} (hi₂ : c₂.Rel i₂ i₂') (j : J) (hj : c₁.π c₂ c (i₁', i₂) = j) : c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) = -CategoryTheory.CategoryStruct.comp ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j)) (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j)
• HomologicalComplex₂.D₁_totalShift₁XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')
• HomologicalComplex₂.D₁_totalShift₂XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')
• HomologicalComplex₂.D₂_totalShift₁XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')
• HomologicalComplex₂.D₂_totalShift₂XIso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')
• HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h
• HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h
• HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h
• HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c