feat(algebra/homology): three lemmas on homological complexes (#12742)

joelriou · joelriou · commit b535c2d5d996 · 2022-03-29T07:35:11.000Z
diff --git a/src/algebra/homology/additive.lean b/src/algebra/homology/additive.lean
@@ -21,7 +21,7 @@ universes v u
 open_locale classical
 noncomputable theory
 
-open category_theory category_theory.limits homological_complex
+open category_theory category_theory.category category_theory.limits homological_complex
 
 variables {ι : Type*}
 variables {V : Type u} [category.{v} V] [preadditive V]
@@ -140,6 +140,28 @@ by tidy
 
 end category_theory
 
+namespace chain_complex
+
+variables {W : Type*} [category W] [preadditive W]
+variables {α : Type*} [add_right_cancel_semigroup α] [has_one α] [decidable_eq α]
+
+lemma map_chain_complex_of (F : V ⥤ W) [F.additive] (X : α → V) (d : Π n, X (n+1) ⟶ X n)
+  (sq : ∀ n, d (n+1) ≫ d n = 0) :
+  (F.map_homological_complex _).obj (chain_complex.of X d sq) =
+  chain_complex.of (λ n, F.obj (X n))
+    (λ n, F.map (d n)) (λ n, by rw [ ← F.map_comp, sq n, functor.map_zero]) :=
+begin
+  apply homological_complex.ext,
+  intros i j hij,
+  { have h : j+1=i := hij,
+    subst h,
+    simp only [category_theory.functor.map_homological_complex_obj_d, of_d,
+      eq_to_hom_refl, comp_id, id_comp], },
+  { refl, }
+end
+
+end chain_complex
+
 variables [has_zero_object V] {W : Type*} [category W] [preadditive W] [has_zero_object W]
 
 namespace homological_complex
diff --git a/src/algebra/homology/differential_object.lean b/src/algebra/homology/differential_object.lean
@@ -47,7 +47,7 @@ by { cases h, dsimp, simp }
   X.d x y ≫ eq_to_hom (congr_arg X.X h) = X.d x z :=
 by { cases h, simp }
 
-@[simp, reassoc] lemma eq_to_hom_f {X Y : differential_object (graded_object_with_shift b V)}
+@[simp, reassoc] lemma eq_to_hom_f' {X Y : differential_object (graded_object_with_shift b V)}
   (f : X ⟶ Y) {x y : β} (h : x = y) :
   X.X_eq_to_hom h ≫ f.f y = f.f x ≫ Y.X_eq_to_hom h :=
 by { cases h, simp }
@@ -81,7 +81,7 @@ def dgo_to_homological_complex :
       subst h,
       have : f.f i ≫ Y.d i = X.d i ≫ f.f (i + 1 • b) := (congr_fun f.comm i).symm,
       reassoc! this,
-      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl, this, category.assoc, eq_to_hom_f]
+      simp only [category.comp_id, eq_to_hom_refl, dif_pos rfl, this, category.assoc, eq_to_hom_f']
     end, } }
 
 /--
diff --git a/src/algebra/homology/homological_complex.lean b/src/algebra/homology/homological_complex.lean
@@ -35,7 +35,7 @@ Defined in terms of these we have `C.d_from i : C.X i ⟶ C.X_next i` and
 
 universes v u
 
-open category_theory category_theory.limits
+open category_theory category_theory.category category_theory.limits
 
 variables {ι : Type*}
 variables (V : Type u) [category.{v} V] [has_zero_morphisms V]
@@ -74,6 +74,21 @@ begin
   { rw [C.shape i j hij, zero_comp] }
 end
 
+lemma ext {C₁ C₂ : homological_complex V c} (h_X : C₁.X = C₂.X)
+  (h_d : ∀ (i j : ι), c.rel i j → C₁.d i j ≫ eq_to_hom (congr_fun h_X j) =
+    eq_to_hom (congr_fun h_X i) ≫ C₂.d i j) : C₁ = C₂ :=
+begin
+  cases C₁,
+  cases C₂,
+  dsimp at h_X,
+  subst h_X,
+  simp only [true_and, eq_self_iff_true, heq_iff_eq],
+  ext i j,
+  by_cases hij : c.rel i j,
+  { simpa only [id_comp, eq_to_hom_refl, comp_id] using h_d i j hij, },
+  { rw [C₁_shape' i j hij, C₂_shape' i j hij], }
+end
+
 end homological_complex
 
 /--
@@ -176,6 +191,12 @@ end
   (f ≫ g).f i = f.f i ≫ g.f i :=
 rfl
 
+@[simp]
+lemma eq_to_hom_f {C₁ C₂ : homological_complex V c} (h : C₁ = C₂) (n : ι) :
+  homological_complex.hom.f (eq_to_hom h) n =
+  eq_to_hom (congr_fun (congr_arg homological_complex.X h) n) :=
+by { subst h, refl, }
+
 -- We'll use this later to show that `homological_complex V c` is preadditive when `V` is.
 lemma hom_f_injective {C₁ C₂ : homological_complex V c} :
   function.injective (λ f : hom C₁ C₂, f.f) :=
