feat(Algebra/Homology): computation of the connecting homomorphism of…

… the homology sequence (#8771) This PR adds a variant of a lemma introduced in #8512: `ShortComplex.SnakeInput.δ_apply'` computes the connecting homomorphism of the snake lemma in a concrete categoriy `C` with a phrasing based on the functor `forget₂ C Ab` rather than `forget C`. From this, the lemma `ShortComplex.ShortExact.δ_apply` is obtained in a new file `Algebra.Homology.ConcreteCategory`: it gives a computation in terms of (co)cycles of the connecting homomorphism in homology attached to a short exact sequence of homological complexes in `C`. This PR also adds a lemma which computes "up to refinements" the connecting homomorphism of the homology sequence in general abelian categories.
leanprover-community · Dec 27, 2023 · d412c82 · d412c82
1 parent e0ae51d
commit d412c82
Show file tree

Hide file tree

Showing 7 changed files with 189 additions and 3 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -231,6 +231,7 @@ import Mathlib.Algebra.HierarchyDesign
 import Mathlib.Algebra.Homology.Additive
 import Mathlib.Algebra.Homology.Augment
 import Mathlib.Algebra.Homology.ComplexShape
+import Mathlib.Algebra.Homology.ConcreteCategory
 import Mathlib.Algebra.Homology.DifferentialObject
 import Mathlib.Algebra.Homology.Exact
 import Mathlib.Algebra.Homology.ExactSequence

diff --git a/Mathlib/Algebra/Homology/ConcreteCategory.lean b/Mathlib/Algebra/Homology/ConcreteCategory.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2023 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.HomologySequence
+import Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
+
+/-!
+# Homology of complexes in concrete categories
+
+The homology of short complexes in concrete categories was studied in
+`Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory`. In this file,
+we introduce specific definitions and lemmas for the homology
+of homological complexes in concrete categories. In particular,
+we give a computation of the connecting homomorphism of
+the homology sequence in terms of (co)cycles.
+
+-/
+
+open CategoryTheory
+
+universe v u
+
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] [HasForget₂ C Ab.{v}]
+  [Abelian C] [(forget₂ C Ab).Additive] [(forget₂ C Ab).PreservesHomology]
+  {ι : Type*} {c : ComplexShape ι}
+
+namespace HomologicalComplex
+
+variable (K : HomologicalComplex C c)
+
+/-- Constructor for cycles of a homological complex in a concrete category. -/
+noncomputable def cyclesMk {i : ι} (x : (forget₂ C Ab).obj (K.X i)) (j : ι) (hj : c.next i = j)
+    (hx : ((forget₂ C Ab).map (K.d i j)) x = 0) :
+    (forget₂ C Ab).obj (K.cycles i) :=
+  (K.sc i).cyclesMk x (by subst hj; exact hx)
+
+@[simp]
+lemma i_cyclesMk {i : ι} (x : (forget₂ C Ab).obj (K.X i)) (j : ι) (hj : c.next i = j)
+    (hx : ((forget₂ C Ab).map (K.d i j)) x = 0) :
+    ((forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x j hj hx) = x := by
+  subst hj
+  apply (K.sc i).i_cyclesMk
+
+end HomologicalComplex
+
+namespace CategoryTheory
+
+namespace ShortComplex
+
+namespace ShortExact
+
+variable {S : ShortComplex (HomologicalComplex C c)}
+  (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j)
+
+lemma δ_apply' (x₃ : (forget₂ C Ab).obj (S.X₃.homology i))
+    (x₂ : (forget₂ C Ab).obj (S.X₂.opcycles i))
+    (x₁ : (forget₂ C Ab).obj (S.X₁.cycles j))
+    (h₂ : (forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i) x₂ =
+      (forget₂ C Ab).map (S.X₃.homologyι i) x₃)
+    (h₁ : (forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j) x₁ =
+      (forget₂ C Ab).map (S.X₂.opcyclesToCycles i j) x₂) :
+    (forget₂ C Ab).map (hS.δ i j hij) x₃ = (forget₂ C Ab).map (S.X₁.homologyπ j) x₁ :=
+  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).δ_apply' x₃ x₂ x₁ h₂ h₁
+
+lemma δ_apply (x₃ : (forget₂ C Ab).obj (S.X₃.X i))
+    (hx₃ : (forget₂ C Ab).map (S.X₃.d i j) x₃ = 0)
+    (x₂ : (forget₂ C Ab).obj (S.X₂.X i)) (hx₂ : (forget₂ C Ab).map (S.g.f i) x₂ = x₃)
+    (x₁ : (forget₂ C Ab).obj (S.X₁.X j))
+    (hx₁ : (forget₂ C Ab).map (S.f.f j) x₁ = (forget₂ C Ab).map (S.X₂.d i j) x₂)
+    (k : ι) (hk : c.next j = k) :
+    (forget₂ C Ab).map (hS.δ i j hij)
+      ((forget₂ C Ab).map (S.X₃.homologyπ i) (S.X₃.cyclesMk x₃ j (c.next_eq' hij) hx₃)) =
+        (forget₂ C Ab).map (S.X₁.homologyπ j) (S.X₁.cyclesMk x₁ k hk (by
+          have := hS.mono_f
+          apply (Preadditive.mono_iff_injective (S.f.f k)).1 inferInstance
+          erw [← forget₂_comp_apply, ← HomologicalComplex.Hom.comm, forget₂_comp_apply, hx₁,
+            ← forget₂_comp_apply, HomologicalComplex.d_comp_d, Functor.map_zero, map_zero,
+            AddMonoidHom.zero_apply])) := by
+  refine hS.δ_apply' i j hij _ ((forget₂ C Ab).map (S.X₂.pOpcycles i) x₂) _ ?_ ?_
+  · erw [← forget₂_comp_apply, ← forget₂_comp_apply,
+      HomologicalComplex.p_opcyclesMap, Functor.map_comp, comp_apply,
+      HomologicalComplex.homology_π_ι, forget₂_comp_apply, hx₂, HomologicalComplex.i_cyclesMk]
+  · apply (Preadditive.mono_iff_injective (S.X₂.iCycles j)).1 inferInstance
+    conv_lhs =>
+      erw [← forget₂_comp_apply, HomologicalComplex.cyclesMap_i, forget₂_comp_apply,
+        HomologicalComplex.i_cyclesMk, hx₁]
+    conv_rhs =>
+      erw [← forget₂_comp_apply, ← forget₂_comp_apply,
+        HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]
+
+end ShortExact
+
+end ShortComplex
+
+end CategoryTheory
diff --git a/Mathlib/Algebra/Homology/HomologySequence.lean b/Mathlib/Algebra/Homology/HomologySequence.lean
@@ -302,6 +302,32 @@ lemma homology_exact₂ : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i
 lemma homology_exact₃ : (ShortComplex.mk _ _ (comp_δ hS i j hij)).Exact :=
   (snakeInput hS i j hij).L₁'_exact
 
+lemma δ_eq' {A : C} (x₃ : A ⟶ S.X₃.homology i) (x₂ : A ⟶ S.X₂.opcycles i)
+    (x₁ : A ⟶ S.X₁.cycles j)
+    (h₂ : x₂ ≫ HomologicalComplex.opcyclesMap S.g i = x₃ ≫ S.X₃.homologyι i)
+    (h₁ : x₁ ≫ HomologicalComplex.cyclesMap S.f j = x₂ ≫ S.X₂.opcyclesToCycles i j) :
+    x₃ ≫ hS.δ i j hij = x₁ ≫ S.X₁.homologyπ j :=
+  (snakeInput hS i j hij).δ_eq x₃ x₂ x₁ h₂ h₁
+
+lemma δ_eq {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : x₃ ≫ S.X₃.d i j = 0)
+    (x₂ : A ⟶ S.X₂.X i) (hx₂ : x₂ ≫ S.g.f i = x₃)
+    (x₁ : A ⟶ S.X₁.X j) (hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j)
+    (k : ι) (hk : c.next j = k) :
+    S.X₃.liftCycles x₃ j (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij =
+      S.X₁.liftCycles x₁ k hk (by
+        have := hS.mono_f
+        rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
+          d_comp_d, comp_zero, zero_comp]) ≫ S.X₁.homologyπ j := by
+  simpa only [assoc] using hS.δ_eq' i j hij (S.X₃.liftCycles x₃ j
+    (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i)
+    (x₂ ≫ S.X₂.pOpcycles i) (S.X₁.liftCycles x₁ k hk _)
+      (by simp only [assoc, HomologicalComplex.p_opcyclesMap,
+        HomologicalComplex.homology_π_ι,
+        HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂])
+      (by rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap,
+        HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles,
+        HomologicalComplex.p_fromOpcycles, hx₁])
+
 end ShortExact
 
 end ShortComplex

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Ab.lean b/Mathlib/Algebra/Homology/ShortComplex/Ab.lean
@@ -71,6 +71,13 @@ the abstract `S.cycles` of the homology API and the more concrete description as
 noncomputable def abCyclesIso : S.cycles ≅ AddCommGroupCat.of (AddMonoidHom.ker S.g) :=
   S.abLeftHomologyData.cyclesIso
 
+@[simp]
+lemma abCyclesIso_inv_apply_iCycles (x : AddMonoidHom.ker S.g) :
+    S.iCycles (S.abCyclesIso.inv x) = x := by
+  dsimp only [abCyclesIso]
+  erw [← comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]
+  rfl
+
 /-- Given a short complex `S` of abelian groups, this is the isomorphism between
 the abstract `S.homology` of the homology API and the more explicit
 quotient of `AddMonoidHom.ker S.g` by the image of

diff --git a/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean b/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
@@ -55,7 +55,7 @@ lemma Preadditive.mono_iff_injective' {X Y : C} (f : X ⟶ Y) :
   have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp)
   exact Arrow.isoOfNatIso e (Arrow.mk f)
 
-lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) :
+lemma Preadditive.epi_iff_surjective {X Y : C} (f : X ⟶ Y) :
     Epi f ↔ Function.Surjective ((forget₂ C Ab).map f) := by
   rw [← AddCommGroupCat.epi_iff_surjective]
   constructor
@@ -65,7 +65,7 @@ lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) :
 
 lemma Preadditive.epi_iff_surjective' {X Y : C} (f : X ⟶ Y) :
     Epi f ↔ Function.Surjective ((forget C).map f) := by
-  simp only [epi_iff_injective, ← CategoryTheory.epi_iff_surjective]
+  simp only [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective]
   apply (MorphismProperty.RespectsIso.epimorphisms (Type w)).arrow_mk_iso_iff
   have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp)
   exact Arrow.isoOfNatIso e (Arrow.mk f)
@@ -91,9 +91,25 @@ lemma ShortExact.injective_f (hS : S.ShortExact) :
 
 lemma ShortExact.surjective_g (hS : S.ShortExact) :
     Function.Surjective ((forget₂ C Ab).map S.g) := by
-  rw [← Preadditive.epi_iff_injective]
+  rw [← Preadditive.epi_iff_surjective]
   exact hS.epi_g
 
+variable (S)
+
+/-- Constructor for cycles of short complexes in a concrete category. -/
+noncomputable def cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂)
+    (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) :
+    (forget₂ C Ab).obj S.cycles :=
+  (S.mapCyclesIso (forget₂ C Ab)).hom ((ShortComplex.abCyclesIso _).inv ⟨x₂, hx₂⟩)
+
+@[simp]
+lemma i_cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂)
+    (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) :
+    (forget₂ C Ab).map S.iCycles (S.cyclesMk x₂ hx₂) = x₂ := by
+  dsimp [cyclesMk]
+  erw [← comp_apply, S.mapCyclesIso_hom_iCycles (forget₂ C Ab),
+    ← comp_apply, abCyclesIso_inv_apply_iCycles ]
+
 end ShortComplex
 
 end preadditive
@@ -136,6 +152,31 @@ lemma δ_apply (x₃ : D.L₀.X₃) (x₂ : D.L₁.X₂) (x₁ : D.L₂.X₁)
   rw [Functor.map_comp, types_comp_apply, eq₁]
   exact h₁.symm
 
+/-- This lemma allows the computation of the connecting homomorphism
+`D.δ` when `D : SnakeInput C` and `C` is a concrete category. -/
+lemma δ_apply' (x₃ : (forget₂ C Ab).obj D.L₀.X₃)
+    (x₂ : (forget₂ C Ab).obj D.L₁.X₂) (x₁ : (forget₂ C Ab).obj D.L₂.X₁)
+    (h₂ : (forget₂ C Ab).map D.L₁.g x₂ = (forget₂ C Ab).map D.v₀₁.τ₃ x₃)
+    (h₁ : (forget₂ C Ab).map D.L₂.f x₁ = (forget₂ C Ab).map D.v₁₂.τ₂ x₂) :
+    (forget₂ C Ab).map D.δ x₃ = (forget₂ C Ab).map D.v₂₃.τ₁ x₁ := by
+  have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp)
+  apply (mono_iff_injective (e.hom.app _)).1 inferInstance
+  refine (congr_hom (e.hom.naturality D.δ) x₃).trans
+    ((D.δ_apply (e.hom.app _ x₃) (e.hom.app _ x₂) (e.hom.app _ x₁) ?_ ?_ ).trans
+    (congr_hom (e.hom.naturality D.v₂₃.τ₁).symm x₁))
+  · refine ((congr_hom (e.hom.naturality D.L₁.g) x₂).symm.trans ?_).trans
+      (congr_hom (e.hom.naturality D.v₀₁.τ₃) x₃)
+    dsimp
+    rw [comp_apply, comp_apply]
+    erw [h₂]
+    rfl
+  · refine ((congr_hom (e.hom.naturality D.L₂.f) x₁).symm.trans ?_).trans
+      (congr_hom (e.hom.naturality D.v₁₂.τ₂) x₂)
+    dsimp
+    rw [comp_apply, comp_apply]
+    erw [h₁]
+    rfl
+
 end SnakeInput
 
 end ShortComplex

diff --git a/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@@ -400,6 +400,11 @@ noncomputable def mapCyclesIso [S.HasLeftHomology] [F.PreservesLeftHomologyOf S]
     (S.map F).cycles ≅ F.obj S.cycles :=
   (S.leftHomologyData.map F).cyclesIso
 
+@[reassoc (attr := simp)]
+lemma mapCyclesIso_hom_iCycles [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
+    (S.mapCyclesIso F).hom ≫ F.map S.iCycles = (S.map F).iCycles := by
+  apply LeftHomologyData.cyclesIso_hom_comp_i
+
 /-- When a functor `F` preserves the left homology of a short complex `S`, this is the
 canonical isomorphism `(S.map F).leftHomology ≅ F.obj S.leftHomology`. -/
 noncomputable def mapLeftHomologyIso [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :

diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -212,6 +212,15 @@ def forget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w}
   HasForget₂.forget₂
 #align category_theory.forget₂ CategoryTheory.forget₂
 
+attribute [local instance] ConcreteCategory.funLike ConcreteCategory.hasCoeToSort
+
+lemma forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C] [ConcreteCategory.{w} C]
+    [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] {X Y Z : C}
+    (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) :
+    ((forget₂ C D).map (f ≫ g) x) =
+      (forget₂ C D).map g ((forget₂ C D).map f x) := by
+  rw [Functor.map_comp, comp_apply]
+
 instance forget₂_faithful (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
     [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : Faithful (forget₂ C D) :=
   HasForget₂.forget_comp.faithful_of_comp