Relative projectives and injectives in full subcategories

An extension-closed full subcategory inherits an exact structure from its ambient category. Ambient relative projectives and injectives remain projective and injective for that structure: the inclusion preserves conflations and fullness transports lifts and extensions back inside. The converse requires presentations inside the subcategory; it need not hold in general.

theorem TauCeti.ExactStructure.isProjective_fullSubcategory_of_isProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (X : P.FullSubcategory) (hX : E.isProjective X.obj) : (fullSubcategory P hP).isProjective X

An ambient relatively projective object lying in an extension-closed full subcategory is relatively projective for the induced exact structure.

theorem TauCeti.ExactStructure.isInjective_fullSubcategory_of_isInjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) (X : P.FullSubcategory) (hX : E.isInjective X.obj) : (fullSubcategory P hP).isInjective X

An ambient relatively injective object lying in an extension-closed full subcategory is relatively injective for the induced exact structure.