feat: computation of the connecting homomorphism of the snake lemma in concrete categories (#8512)

This PR provides a lemma `ShortComplex.SnakeInput.δ_apply` which allows the computation of the connecting homomorphism in concrete categories. Incidentally, we also deduce from previous results that functors which preserve homology preserve finite limits and finite colimits.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib.lean

@@ -246,6 +246,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Abelian
 import Mathlib.Algebra.Homology.ShortComplex.Basic
 import Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
 import Mathlib.Algebra.Homology.ShortComplex.Exact
+import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
 import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
 import Mathlib.Algebra.Homology.ShortComplex.Homology

Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.Algebra.Homology.ShortComplex.Ab
+import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
+import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
+import Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
 
 /-!
 # Exactness of short complexes in concrete abelian categories
@@ -14,11 +17,15 @@ if and only if it is so after applying the functor `forget₂ C Ab`.
 
 -/
 
+universe w v u
+
 namespace CategoryTheory
 
 open Limits
 
-variable {C : Type*} [Category C] [ConcreteCategory C] [HasForget₂ C Ab]
+section
+
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C] [HasForget₂ C Ab]
 
 @[simp]
 lemma ShortComplex.zero_apply
@@ -41,6 +48,13 @@ lemma Preadditive.mono_iff_injective {X Y : C} (f : X ⟶ Y) :
     infer_instance
   · apply Functor.mono_of_mono_map
 
+lemma Preadditive.mono_iff_injective' {X Y : C} (f : X ⟶ Y) :
+    Mono f ↔ Function.Injective ((forget C).map f) := by
+  simp only [mono_iff_injective, ← CategoryTheory.mono_iff_injective]
+  apply (MorphismProperty.RespectsIso.monomorphisms (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)
+
 lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) :
     Epi f ↔ Function.Surjective ((forget₂ C Ab).map f) := by
   rw [← AddCommGroupCat.epi_iff_surjective]
@@ -49,6 +63,13 @@ lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) :
     infer_instance
   · apply Functor.epi_of_epi_map
 
+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]
+  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)
+
 namespace ShortComplex
 
 lemma exact_iff_exact_map_forget₂ [S.HasHomology] :
@@ -77,4 +98,48 @@ end ShortComplex
 
 end preadditive
 
+end
+
+section abelian
+
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] [HasForget₂ C Ab]
+  [Abelian C] [(forget₂ C Ab).Additive] [(forget₂ C Ab).PreservesHomology]
+
+attribute [local instance] ConcreteCategory.funLike ConcreteCategory.hasCoeToSort
+
+namespace ShortComplex
+
+namespace SnakeInput
+
+variable (D : SnakeInput C)
+
+/-- This lemma allows the computation of the connecting homomorphism
+`D.δ` when `D : SnakeInput C` and `C` is a concrete category. -/
+lemma δ_apply (x₃ : D.L₀.X₃) (x₂ : D.L₁.X₂) (x₁ : D.L₂.X₁)
+    (h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃) (h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂) :
+    D.δ x₃ = D.v₂₃.τ₁ x₁ := by
+  have := (forget₂ C Ab).preservesFiniteLimitsOfPreservesHomology
+  have : PreservesFiniteLimits (forget C) := by
+    have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp
+    simpa only [← this] using compPreservesFiniteLimits _ _
+  have eq := congr_fun ((forget C).congr_map D.snd_δ)
+    (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
+  have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
+  have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
+  dsimp [FunLike.coe] at eq₁ eq₂
+  rw [Functor.map_comp, types_comp_apply, FunctorToTypes.map_comp_apply] at eq
+  rw [eq₂] at eq
+  refine' eq.trans (congr_arg ((forget C).map D.v₂₃.τ₁) _)
+  apply (Preadditive.mono_iff_injective' D.L₂.f).1 inferInstance
+  rw [← FunctorToTypes.map_comp_apply, φ₁_L₂_f]
+  dsimp [φ₂]
+  rw [Functor.map_comp, types_comp_apply, eq₁]
+  exact h₁.symm
+
+end SnakeInput
+
+end ShortComplex
+
+end abelian
+
 end CategoryTheory

Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean

@@ -0,0 +1,51 @@
+/-
+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.ShortComplex.PreservesHomology
+import Mathlib.CategoryTheory.Preadditive.LeftExact
+
+/-!
+# Exact functors
+
+In this file, it is shown that additive functors which preserves homology
+also preserves finite limits and finite colimits.
+
+TODO: provive alternate characterizations of left/right exact functors
+in terms of preservation of exactness.
+
+-/
+
+namespace CategoryTheory
+
+open Limits ZeroObject
+
+namespace Functor
+
+variable {C D : Type*} [Category C] [Category D] [Preadditive C] [Preadditive D]
+  (F : C ⥤ D) [F.Additive] [F.PreservesHomology] [HasZeroObject C]
+
+/-- An additive functor which preserves homology preserves finite limits. -/
+noncomputable def preservesFiniteLimitsOfPreservesHomology
+    [HasFiniteProducts C] [HasKernels C] : PreservesFiniteLimits F := by
+  have := fun {X Y : C} (f : X ⟶ Y) => PreservesHomology.preservesKernel F f
+  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
+  have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
+  have : HasZeroObject D :=
+    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
+  exact preservesFiniteLimitsOfPreservesKernels F
+
+/-- An additive which preserves homology preserves finite colimits. -/
+noncomputable def preservesFiniteColimitsOfPreservesHomology
+    [HasFiniteCoproducts C] [HasCokernels C] : PreservesFiniteColimits F := by
+  have := fun {X Y : C} (f : X ⟶ Y) => PreservesHomology.preservesCokernel F f
+  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryCoproducts
+  have : HasCoequalizers C := Preadditive.hasCoequalizers_of_hasCokernels
+  have : HasZeroObject D :=
+    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
+  exact preservesFiniteColimitsOfPreservesCokernels F
+
+end Functor
+
+end CategoryTheory