Left resolutions which preserve the zero object

The structure LeftResolution allows to define a functorial resolution of an object (see LeftResolution.chainComplexFunctor in the file Mathlib/Algebra/Homology/LeftResolution/Basic.lean). In order to extend this resolution to complexes, we not only need the functoriality but also that zero morphisms are sent to zero. In this file, given ι : C ⥤ A, we extend Λ : LeftResolution ι to idempotent completions as Λ.karoubi : LeftResolution ((functorExtension₂ C A).obj ι), and when both C and A are idempotent complete, we define Λ.reduced : LeftResolution ι in such a way that the functor Λ.reduced.F : A ⥤ C preserves zero morphisms.

For example, if A := ModuleCat R and C is the full subcategory of flat R-modules, we may first define Λ by using the functor which sends an R-module M to the free R-module on the elements of M. Then, Λ.reduced.F.obj M will be obtained from the free R-module on M by factoring out the direct factor corresponding to the submodule spanned by the generator corresponding to 0 : M (TODO).

def CategoryTheory.Abelian.LeftResolution.karoubi.F' {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] : Functor A (Idempotents.Karoubi C)

Auxiliary definition for LeftResolution.karoubi.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] {X Y : A} (f : X ⟶ Y) : ((F' Λ).map f).f = Λ.F.map f - Λ.F.map 0

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (X : A) : ((F' Λ).obj X).p = CategoryStruct.id (Λ.F.obj X) - Λ.F.map 0

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (X : A) : ((F' Λ).obj X).X = Λ.F.obj X

def CategoryTheory.Abelian.LeftResolution.karoubi.F {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] : Functor (Idempotents.Karoubi A) (Idempotents.Karoubi C)

Auxiliary definition for LeftResolution.karoubi.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] {X✝ Y✝ : Idempotents.Karoubi A} (f : X✝ ⟶ Y✝) : ((F Λ).map f).f = Λ.F.map f.f - Λ.F.map 0

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (P : Idempotents.Karoubi A) : ((F Λ).obj P).p = Λ.F.map P.p - Λ.F.map 0

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (P : Idempotents.Karoubi A) : ((F Λ).obj P).X = Λ.F.obj P.X

instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] : (karoubi.F Λ).PreservesZeroMorphisms

def CategoryTheory.Abelian.LeftResolution.karoubi.π' {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : (Idempotents.toKaroubi A).comp ((F Λ).comp ((Idempotents.functorExtension₂ C A).obj ι)) ⟶ Idempotents.toKaroubi A

Auxiliary definition for LeftResolution.karoubi.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) : ((π' Λ).app X).f = Λ.π.app X

def CategoryTheory.Abelian.LeftResolution.karoubi.retractArrow {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) : RetractArrow ((π' Λ).app X) ((Idempotents.toKaroubi A).map (Λ.π.app X))

The morphism (karoubi.π' Λ).app X is a retract of (toKaroubi _).map (Λ.π.app X).

instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ' {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) : Epi ((karoubi.π' Λ).app X)

def CategoryTheory.Abelian.LeftResolution.karoubi.π {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : (F Λ).comp ((Idempotents.functorExtension₂ C A).obj ι) ⟶ Functor.id (Idempotents.Karoubi A)

Auxiliary definition for LeftResolution.karoubi.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) : (π Λ).app ((Idempotents.toKaroubi A).obj X) = (π' Λ).app X

instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) : Epi ((karoubi.π Λ).app ((Idempotents.toKaroubi A).obj X))

instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : Idempotents.Karoubi A) : Epi ((karoubi.π Λ).app X)

noncomputable def CategoryTheory.Abelian.LeftResolution.karoubi {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : LeftResolution ((Idempotents.functorExtension₂ C A).obj ι)

Given ι : C ⥤ A, this is the extension of Λ : LeftResolution ι to LeftResolution ((functorExtension₂ C A).obj ι), where (functorExtension₂ C A).obj ι : Karoubi C ⥤ Karoubi A is the extension of ι.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi_π {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : Λ.karoubi.π = karoubi.π Λ

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.karoubi_F {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : Λ.karoubi.F = karoubi.F Λ

instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] : Λ.karoubi.F.PreservesZeroMorphisms

noncomputable def CategoryTheory.Abelian.LeftResolution.reduced {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] [IsIdempotentComplete A] [IsIdempotentComplete C] : LeftResolution ι

Given an additive functor ι : C ⥤ A between idempotent complete categories, any Λ : LeftResolution ι induces a term Λ.reduced : LeftResolution ι such that Λ.reduced.F preserves zero morphisms.

instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] [IsIdempotentComplete A] [IsIdempotentComplete C] : Λ.reduced.F.PreservesZeroMorphisms