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.

theorem CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [HasExt C] [HasExt D] [EnoughProjectives C] [F.PreservesProjectiveObjects] (X Y : C) (n : ℕ) : Function.Bijective ⇑(F.mapExtAddHom X Y n)

theorem CategoryTheory.Functor.mapExt_bijective_of_preservesInjectiveObjects {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [HasExt C] [HasExt D] [EnoughInjectives C] [F.PreservesInjectiveObjects] (X Y : C) (n : ℕ) : Function.Bijective ⇑(F.mapExtAddHom X Y n)