feat(Homology): bijection between Ext (#31697)

For `F : C ⥤ D` fully faithful functor between abelian category, if one of the following
1: `C` has enough projectives and `F` preserve projective object
2: `C` has enough injectives and `F` preserve injective object
The induced map `Ext X Y n → Ext F(X) F(Y) n` is bijective.

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Author: Thmoas-Guan

Mathlib.lean

@@ -570,6 +570,7 @@ public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
 public import Mathlib.Algebra.Homology.DerivedCategory.Fractions
 public import Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Mathlib/Algebra/Homology/DerivedCategory/Ext/MapBijective.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2025 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan
+-/
+module
+
+public import Mathlib.Algebra.Category.Grp.Zero
+public import Mathlib.Algebra.FiveLemma
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
+public import Mathlib.CategoryTheory.Preadditive.Injective.Preserves
+public import Mathlib.CategoryTheory.Preadditive.Projective.Preserves
+
+/-!
+
+# Bijections Between Ext
+
+In this file, we show that the maps between `Ext` induced
+by a fully faithful exact functor `F : C ⥤ D` are bijective when either
+1. `F` preserves projective objects and `C` has enough projectives, or
+2. `F` preserves injective objects and `C` has enough injectives.
+
+-/
+
+@[expose] public section
+
+universe w w' v v' u u'
+
+namespace CategoryTheory
+
+open Limits Abelian
+
+variable {C : Type u} [Category.{v} C] [Abelian C]
+variable {D : Type u'} [Category.{v'} D] [Abelian D]
+
+variable (F : C ⥤ D) [F.Additive] [PreservesFiniteLimits F] [PreservesFiniteColimits F]
+
+attribute [local simp] Ext.mapExactFunctor_comp Ext.mapExactFunctor_mk₀ Ext.mapExactFunctor_extClass
+
+attribute [local instance] Ext.subsingleton_of_projective in
+lemma Functor.mapExt_bijective_of_preservesProjectiveObjects [F.Full] [F.Faithful] [HasExt.{w} C]
+    [HasExt.{w'} D] [EnoughProjectives C] [F.PreservesProjectiveObjects] (X Y : C) (n : ℕ) :
+    Function.Bijective (F.mapExtAddHom X Y n) := by
+  induction n generalizing X with
+  | zero => simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩
+  | succ n hn =>
+    let P : ProjectivePresentation X := Classical.arbitrary _
+    let S := ShortComplex.mk _ _ (kernel.condition P.f)
+    have : Projective (S.map F).X₂ := Functor.PreservesProjectiveObjects.projective_obj P.projective
+    have hS : S.ShortExact := { exact := ShortComplex.exact_kernel P.f }
+    exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
+      (F.mapExtAddHom S.X₂ Y n) (F.mapExtAddHom S.X₁ Y n) (F.mapExtAddHom S.X₃ Y (n + 1))
+      (by cat_disch) (by cat_disch)
+      ((ShortComplex.ab_exact_iff_function_exact _).1
+        (Ext.contravariant_sequence_exact₁' hS Y n (n + 1) (add_comm 1 n)))
+      ((ShortComplex.ab_exact_iff_function_exact _).1
+        (Ext.contravariant_sequence_exact₁' (hS.map F) (F.obj Y) n (n + 1) (add_comm 1 n)))
+      (hn _).surjective (hn _)
+      (fun x₃ ↦ Ext.contravariant_sequence_exact₃ hS _ x₃ (by subsingleton) (add_comm 1 n))
+      (fun y₃ ↦ Ext.contravariant_sequence_exact₃ (hS.map F) _ y₃ (by subsingleton) (add_comm 1 n))
+
+attribute [local instance] Ext.subsingleton_of_injective in
+lemma Functor.mapExt_bijective_of_preservesInjectiveObjects [F.Full] [F.Faithful] [HasExt.{w} C]
+    [HasExt.{w'} D] [EnoughInjectives C] [F.PreservesInjectiveObjects] (X Y : C) (n : ℕ) :
+    Function.Bijective (F.mapExtAddHom X Y n) := by
+  induction n generalizing Y with
+  | zero => simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩
+  | succ n hn =>
+    let I : InjectivePresentation Y := Classical.arbitrary _
+    let S := ShortComplex.mk _ _ (cokernel.condition I.f)
+    have : Injective (S.map F).X₂ := Functor.PreservesInjectiveObjects.injective_obj I.injective
+    have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.f }
+    exact AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact _ _ _ _
+      (F.mapExtAddHom X S.X₂ n) (F.mapExtAddHom X S.X₃ n) (F.mapExtAddHom X S.X₁ (n + 1))
+      (by cat_disch) (by cat_disch)
+      ((ShortComplex.ab_exact_iff_function_exact _).mp
+        (Ext.covariant_sequence_exact₃' X hS n (n + 1) rfl))
+      ((ShortComplex.ab_exact_iff_function_exact _).mp
+        (Ext.covariant_sequence_exact₃' (F.obj X) (hS.map F) n (n + 1) rfl))
+      (hn _).surjective (hn _)
+      (fun x₁ ↦ Ext.covariant_sequence_exact₁ _ hS x₁ (by subsingleton) rfl)
+      (fun y₁ ↦ Ext.covariant_sequence_exact₁ _ (hS.map F) y₁ (by subsingleton) rfl)
+
+end CategoryTheory

Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean

@@ -66,6 +66,8 @@ class EnoughInjectives : Prop where
 
 attribute [inherit_doc EnoughInjectives] EnoughInjectives.presentation
 
+attribute [instance low] EnoughInjectives.presentation
+
 end
 
 namespace Injective

Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean

@@ -77,6 +77,8 @@ an epimorphism `P ↠ X`. -/
 class EnoughProjectives : Prop where
   presentation : ∀ X : C, Nonempty (ProjectivePresentation X)
 
+attribute [instance low] EnoughProjectives.presentation
+
 end
 
 namespace Projective