feat(algebra/homology/*): add hypotheses to the d_comp_d' axiom (#7673)

src/algebra/homology/additive.lean

@@ -101,7 +101,7 @@ def functor.map_homological_complex (F : V ⥤ W) [F.additive] (c : complex_shap
   { X := λ i, F.obj (C.X i),
     d := λ i j, F.map (C.d i j),
     shape' := λ i j w, by rw [C.shape _ _ w, F.map_zero],
-    d_comp_d' := λ i j k, by rw [←F.map_comp, C.d_comp_d, F.map_zero], },
+    d_comp_d' := λ i j k _ _, by rw [←F.map_comp, C.d_comp_d, F.map_zero], },
   map := λ C D f,
   { f := λ i, F.map (f.f i),
     comm' := λ i j h, by { dsimp,  rw [←F.map_comp, ←F.map_comp, f.comm], }, }, }.

src/algebra/homology/augment.lean

@@ -69,7 +69,7 @@ def augment (C : chain_complex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫
     { simpa using s, },
     { rw [C.shape], simp, omega, },
   end,
-  d_comp_d' := λ i j k, begin
+  d_comp_d' := λ i j k hij hjk, begin
     rcases i with _|_|i; rcases j with _|_|j; cases k; unfold_aux; try { simp },
     cases i,
     { exact w, },
@@ -207,7 +207,7 @@ def augment (C : cochain_complex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d
     { simpa using s, },
     { rw [C.shape], simp, omega, },
   end,
-  d_comp_d' := λ i j k, begin
+  d_comp_d' := λ i j k hij hjk, begin
     rcases k with _|_|k; rcases j with _|_|j; cases i; unfold_aux; try { simp },
     cases k,
     { exact w, },

src/algebra/homology/differential_object.lean

@@ -39,12 +39,10 @@ def dgo_to_homological_complex :
   { X := λ i, X.X i,
     d := λ i j, if h : i + b = j then X.d i ≫ eq_to_hom (congr_arg X.X h) else 0,
     shape' := λ i j w, by { dsimp at w, rw dif_neg w, },
-    d_comp_d' := λ i j k, begin
-      split_ifs with h h',
-      { substs h h',
-        simp only [category.comp_id, eq_to_hom_refl],
-        exact congr_fun (X.d_squared) i, },
-      all_goals { simp, },
+    d_comp_d' := λ i j k hij hjk, begin
+      dsimp at hij hjk, substs hij hjk,
+      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl],
+      exact congr_fun (X.d_squared) i,
     end },
   map := λ X Y f,
   { f := f.f,

src/algebra/homology/flip.lean

@@ -36,7 +36,7 @@ def flip_obj (C : homological_complex (homological_complex V c) c') :
   { X := λ j, (C.X j).X i,
     d := λ j j', (C.d j j').f i,
     shape' := λ j j' w, by { rw C.shape j j' w, simp, },
-    d_comp_d' := λ j₁ j₂ j₃, congr_hom (C.d_comp_d j₁ j₂ j₃) i, },
+    d_comp_d' := λ j₁ j₂ j₃ _ _, congr_hom (C.d_comp_d j₁ j₂ j₃) i, },
   d := λ i i',
   { f := λ j, (C.X j).d i i',
     comm' := λ j j' h, ((C.d j j').comm i i').symm, },

src/algebra/homology/homological_complex.lean

@@ -54,13 +54,26 @@ structure homological_complex (c : complex_shape ι) :=
 (X : ι → V)
 (d : Π i j, X i ⟶ X j)
 (shape' : ∀ i j, ¬ c.rel i j → d i j = 0 . obviously)
-(d_comp_d' : ∀ i j k, d i j ≫ d j k = 0 . obviously)
+(d_comp_d' : ∀ i j k, c.rel i j → c.rel j k → d i j ≫ d j k = 0 . obviously)
 
-restate_axiom homological_complex.shape'
-restate_axiom homological_complex.d_comp_d'
+namespace homological_complex
+
+restate_axiom shape'
+attribute [simp] shape
+
+variables {V} {c : complex_shape ι}
+
+@[simp, reassoc] lemma d_comp_d (C : homological_complex V c) (i j k : ι) :
+  C.d i j ≫ C.d j k = 0 :=
+begin
+  by_cases hij : c.rel i j,
+  { by_cases hjk : c.rel j k,
+    { exact C.d_comp_d' i j k hij hjk },
+    { rw [C.shape j k hjk, comp_zero] } },
+  { rw [C.shape i j hij, zero_comp] }
+end
 
-attribute [simp] homological_complex.shape
-attribute [simp, reassoc] homological_complex.d_comp_d
+end homological_complex
 
 /--
 An `α`-indexed chain complex is a `homological_complex`
@@ -505,13 +518,11 @@ def of (X : α → V) (d : Π n, X (n+1) ⟶ X n) (sq : ∀ n, d (n+1) ≫ d n =
   else
     0,
   shape' := λ i j w, by rw dif_neg (ne.symm w),
-  d_comp_d' := λ i j k,
+  d_comp_d' := λ i j k hij hjk,
   begin
-    split_ifs with h h' h',
-    { substs h h',
-      simp only [category.id_comp, eq_to_hom_refl],
-      exact sq k },
-    all_goals { simp },
+    dsimp at hij hjk, substs hij hjk,
+    simp only [category.id_comp, dif_pos rfl, eq_to_hom_refl],
+    exact sq k,
   end }
 
 variables (X : α → V) (d : Π n, X (n+1) ⟶ X n) (sq : ∀ n, d (n+1) ≫ d n = 0)