Left resolutions

Given a fully faithful functor ι : C ⥤ A to an abelian category, we introduce a structure Abelian.LeftResolution ι which gives a functor F : A ⥤ C and a natural epimorphism π.app X : ι.obj (F.obj X) ⟶ X for all X : A. This is used in order to construct a resolution functor LeftResolution.chainComplexFunctor : A ⥤ ChainComplex C ℕ.

This shall be used in order to construct functorial flat resolutions.

structure CategoryTheory.Abelian.LeftResolution {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] (ι : Functor C A) : Type (max (max (max u_1 u_2) v_1) v_2)

Given a fully faithful functor ι : C ⥤ A, this structure contains the data of a functor F : A ⥤ C and a functorial epimorphism π.app X : ι.obj (F.obj X) ⟶ X for all X : A.

• F : Functor A C

  a functor which sends X : A to an object F.obj X with an epimorphism π.app X : ι.obj (F.obj X) ⟶ X

• π : self.F.comp ι ⟶ Functor.id A

  the natural epimorphism

• epi_π_app (X : A) : Epi (self.π.app X)

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.π_naturality {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X Y : A) (f : X ⟶ Y) : CategoryStruct.comp (ι.map (Λ.F.map f)) (Λ.π.app Y) = CategoryStruct.comp (Λ.π.app X) f

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.π_naturality_assoc {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X Y : A) (f : X ⟶ Y) {Z : A} (h : Y ⟶ Z) : CategoryStruct.comp (ι.map (Λ.F.map f)) (CategoryStruct.comp (Λ.π.app Y) h) = CategoryStruct.comp (Λ.π.app X) (CategoryStruct.comp f h)

@[irreducible]

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplex {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : ChainComplex C ℕ

Given ι : C ⥤ A, Λ : LeftResolution ι, X : A, this is a chain complex which is a (functorial) resolution of A that is obtained inductively by using the epimorphisms given by Λ.

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : (Λ.chainComplex X).X 0 ≅ Λ.F.obj X

Given Λ : LeftResolution ι, the chain complex Λ.chainComplex X identifies in degree 0 to Λ.F.obj X.

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : (Λ.chainComplex X).X 1 ≅ Λ.F.obj (Limits.kernel (Λ.π.app X))

Given Λ : LeftResolution ι, the chain complex Λ.chainComplex X identifies in degree 1 to Λ.F.obj (kernel (Λ.π.app X)).

theorem CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0 {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : ι.map ((Λ.chainComplex X).d 1 0) = CategoryStruct.comp (ι.map (Λ.chainComplexXOneIso X).hom) (CategoryStruct.comp (Λ.π.app (Limits.kernel (Λ.π.app X))) (CategoryStruct.comp (Limits.kernel.ι (Λ.π.app X)) (ι.map (Λ.chainComplexXZeroIso X).inv)))

theorem CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] {Z : A} (h : ι.obj ((Λ.chainComplex X).X 0) ⟶ Z) : CategoryStruct.comp (ι.map ((Λ.chainComplex X).d 1 0)) h = CategoryStruct.comp (ι.map (Λ.chainComplexXOneIso X).hom) (CategoryStruct.comp (Λ.π.app (Limits.kernel (Λ.π.app X))) (CategoryStruct.comp (Limits.kernel.ι (Λ.π.app X)) (CategoryStruct.comp (ι.map (Λ.chainComplexXZeroIso X).inv) h)))

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexXIso {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (n : ℕ) : (Λ.chainComplex X).X (n + 2) ≅ Λ.F.obj (Limits.kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))

The isomorphism which gives the inductive step of the construction of Λ.chainComplex X.

theorem CategoryTheory.Abelian.LeftResolution.map_chainComplex_d {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (n : ℕ) : ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) = CategoryStruct.comp (ι.map (Λ.chainComplexXIso X n).hom) (CategoryStruct.comp (Λ.π.app (Limits.kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))) (Limits.kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))

theorem CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (n : ℕ) : ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).ExactAt (n + 1)

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexMap {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : Λ.chainComplex X ⟶ Λ.chainComplex Y

The morphism Λ.chainComplex X ⟶ Λ.chainComplex Y of chain complexes induced by f : X ⟶ Y.

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0 {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : (Λ.chainComplexMap f).f 0 = CategoryStruct.comp (Λ.chainComplexXZeroIso X).hom (CategoryStruct.comp (Λ.F.map f) (Λ.chainComplexXZeroIso Y).inv)

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1 {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : (Λ.chainComplexMap f).f 1 = CategoryStruct.comp (Λ.chainComplexXOneIso X).hom (CategoryStruct.comp (Λ.F.map (Limits.kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)) (Λ.chainComplexXOneIso Y).inv)

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y : A} (f : X ⟶ Y) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] (n : ℕ) : (Λ.chainComplexMap f).f (n + 2) = CategoryStruct.comp (Λ.chainComplexXIso X n).hom (CategoryStruct.comp (Λ.F.map (Limits.kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n)) (ι.map ((Λ.chainComplex Y).d (n + 1) n)) (ι.map ((Λ.chainComplexMap f).f (n + 1))) (ι.map ((Λ.chainComplexMap f).f n)) ⋯)) (Λ.chainComplexXIso Y n).inv)

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_id {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : Λ.chainComplexMap (CategoryStruct.id X) = CategoryStruct.id (Λ.chainComplex X)

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) (X Y : A) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] [Λ.F.PreservesZeroMorphisms] : Λ.chainComplexMap 0 = 0

@[simp]

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : Λ.chainComplexMap (CategoryStruct.comp f g) = CategoryStruct.comp (Λ.chainComplexMap f) (Λ.chainComplexMap g)

theorem CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] {Z✝ : ChainComplex C ℕ} (h : Λ.chainComplex Z ⟶ Z✝) : CategoryStruct.comp (Λ.chainComplexMap (CategoryStruct.comp f g)) h = CategoryStruct.comp (Λ.chainComplexMap f) (CategoryStruct.comp (Λ.chainComplexMap g) h)

noncomputable def CategoryTheory.Abelian.LeftResolution.chainComplexFunctor {A : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Category.{v_2, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [ι.Full] [ι.Faithful] [Limits.HasZeroMorphisms C] [Abelian A] : Functor A (ChainComplex C ℕ)

Given ι : C ⥤ A, Λ : LeftResolution ι, this is a functor A ⥤ ChainComplex C ℕ which sends X : A to a resolution consisting of objects in C.