feat(Algebra/Homology): more lemmas for the biproduct of complexes (#35934)

joelriou · joelriou · commit a237616fe574 · 2026-03-02T13:09:15.000Z
diff --git a/Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean b/Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@@ -86,7 +86,49 @@ lemma biprod_inr_snd_f (i : ι) :
     (biprod.inr : L ⟶ K ⊞ L).f i ≫ (biprod.snd : K ⊞ L ⟶ L).f i = 𝟙 _ := by
   rw [← comp_f, biprod.inr_snd, id_f]
 
+@[simp]
+lemma biprod_total_f (i : ι) :
+    (biprod.fst : K ⊞ L ⟶ K).f i ≫ (biprod.inl : K ⟶ K ⊞ L).f i +
+      (biprod.snd : K ⊞ L ⟶ L).f i ≫ (biprod.inr : L ⟶ K ⊞ L).f i =
+    𝟙 ((biprod K L).X i) := by
+  simp [← comp_f, ← add_f_apply]
+
 variable {K L}
+
+section
+
+variable {A : C} {i : ι}
+
+lemma biprodX_ext_from_iff {f g : (K ⊞ L).X i ⟶ A} :
+    f = g ↔ (biprod.inl : K ⟶ K ⊞ L).f i ≫ f = (biprod.inl : K ⟶ K ⊞ L).f i ≫ g ∧
+      (biprod.inr : L ⟶ K ⊞ L).f i ≫ f = (biprod.inr : L ⟶ K ⊞ L).f i ≫ g := by
+  refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
+  rw [← cancel_epi (𝟙 _)]
+  simp [← biprod_total_f, h₁, h₂]
+
+@[ext]
+lemma biprodX_ext_from {f g : (K ⊞ L).X i ⟶ A}
+    (h₁ : (biprod.inl : K ⟶ K ⊞ L).f i ≫ f = (biprod.inl : K ⟶ K ⊞ L).f i ≫ g)
+    (h₂ : (biprod.inr : L ⟶ K ⊞ L).f i ≫ f = (biprod.inr : L ⟶ K ⊞ L).f i ≫ g) :
+    f = g := by
+  simp [biprodX_ext_from_iff, h₁, h₂]
+
+lemma biprodX_ext_to_iff {f g : A ⟶ (K ⊞ L).X i} :
+    f = g ↔ f ≫ (biprod.fst : K ⊞ L ⟶ K).f i = g ≫ (biprod.fst : K ⊞ L ⟶ K).f i ∧
+      f ≫ (biprod.snd : K ⊞ L ⟶ L).f i = g ≫ (biprod.snd : K ⊞ L ⟶ L).f i := by
+  refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
+  rw [← cancel_mono (𝟙 _)]
+  simp [← biprod_total_f, reassoc_of% h₁, reassoc_of% h₂]
+
+@[ext]
+lemma biprodX_ext_to {f g : A ⟶ (K ⊞ L).X i}
+    (h₁ : f ≫ (biprod.fst : K ⊞ L ⟶ K).f i = g ≫ (biprod.fst : K ⊞ L ⟶ K).f i)
+    (h₂ : f ≫ (biprod.snd : K ⊞ L ⟶ L).f i = g ≫ (biprod.snd : K ⊞ L ⟶ L).f i) :
+    f = g := by
+  simp [biprodX_ext_to_iff, h₁, h₂]
+
+end
+
 variable {M : HomologicalComplex C c}
 
 @[reassoc (attr := simp)]
