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 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).

source
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.

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.{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
    source
    @[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
    source
    @[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
    source
    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.

    Equations
    Instances For
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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
      source
      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.

      Equations
      Instances For
        source
        @[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
        source
        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).

        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.{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)
          source
          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.

          Equations
          Instances For
            source
            @[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
            source
            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))
            source
            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)
            source
            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 ι.

            Equations
            Instances For
              source
              @[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 Λ
              source
              @[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.π Λ
              source
              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
              source
              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.

              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.{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