Documentation

Mathlib.Algebra.Homology.LeftResolution.Reduced

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 Algebra.Homology.LeftResolution.Basic). 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).

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

Auxiliary definition for LeftResolution.karoubi.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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
    source
    @[simp]
    theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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
    source
    @[simp]
    theorem CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (X : A) :
    ((F' Λ).obj X).X = Λ.F.obj X
    source
    def CategoryTheory.Abelian.LeftResolution.karoubi.F {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] :
    Functor (Idempotents.Karoubi A) (Idempotents.Karoubi C)

    Auxiliary definition for LeftResolution.karoubi.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] (P : Idempotents.Karoubi A) :
      ((F Λ).obj P).X = Λ.F.obj P.X
      source
      @[simp]
      theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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
      source
      @[simp]
      theorem CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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
      source
      instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] :
      (karoubi.F Λ).PreservesZeroMorphisms
      source
      def CategoryTheory.Abelian.LeftResolution.karoubi.π' {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) :
        ((π' Λ).app X).f = Λ.π.app X
        source
        def CategoryTheory.Abelian.LeftResolution.karoubi.retractArrow {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ' {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) :
          Epi ((karoubi.π' Λ).app X)
          source
          def CategoryTheory.Abelian.LeftResolution.karoubi.π {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) :
            (π Λ).app ((Idempotents.toKaroubi A).obj X) = (π' Λ).app X
            source
            instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : A) :
            Epi ((karoubi.π Λ).app ((Idempotents.toKaroubi A).obj X))
            source
            instance CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] (X : Idempotents.Karoubi A) :
            Epi ((karoubi.π Λ).app X)
            source
            noncomputable def CategoryTheory.Abelian.LeftResolution.karoubi {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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 ι.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Abelian.LeftResolution.karoubi_F {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] :
              Λ.karoubi.F = karoubi.F Λ
              source
              @[simp]
              theorem CategoryTheory.Abelian.LeftResolution.karoubi_π {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] :
              Λ.karoubi.π = karoubi.π Λ
              source
              instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] :
              Λ.karoubi.F.PreservesZeroMorphisms
              source
              noncomputable def CategoryTheory.Abelian.LeftResolution.reduced {A : Type u_1} {C : Type u_2} [Category.{u_3, u_2} C] [Category.{u_4, 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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced {A : Type u_1} {C : Type u_2} [Category.{u_4, u_2} C] [Category.{u_3, u_1} A] {ι : Functor C A} (Λ : LeftResolution ι) [Preadditive C] [Preadditive A] [ι.Additive] [IsIdempotentComplete A] [IsIdempotentComplete C] :
                Λ.reduced.F.PreservesZeroMorphisms