Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Ext groups in abelian categories #

Let C be an abelian category (with C : Type u and Category.{v} C). In this file, we introduce the assumption HasExt.{w} C which asserts that morphisms between single complexes in arbitrary degrees in the derived category of C are w-small. Under this assumption, we define Ext.{w} X Y n : Type w as shrunk versions of suitable types of morphisms in the derived category. In particular, when C has enough projectives or enough injectives, the property HasExt.{v} C shall hold (TODO).

Note: in certain situations, w := v shall be the preferred choice of universe (e.g. if C := ModuleCat.{v} R with R : Type v). However, in the development of the API for Ext-groups, it is important to keep a larger degree of generality for universes, as w < v may happen in certain situations. Indeed, if X : Scheme.{u}, then the underlying category of the étale site of X shall be a large category. However, the category Sheaf X.Etale AddCommGroupCat.{u} shall have good properties (because there is a small category of affine schemes with the same category of sheaves), and even though the type of morphisms in Sheaf X.Etale AddCommGroupCat.{u} shall be in Type (u + 1), these types are going to be u-small. Then, for C := Sheaf X.etale AddCommGroupCat.{u}, we will have Category.{u + 1} C, but HasExt.{u} C will hold (as C has enough injectives). Then, the Ext groups between étale sheaves over X shall be in Type u.

TODO #

@[reducible, inline]

The property that morphisms between single complexes in arbitrary degrees are w-small in the derived category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A Ext-group in an abelian category C, defined as a Type w when [HasExt.{w} C].

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CategoryTheory.Abelian.Ext.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {a : } {b : } (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : } (h : a + b = c) :

      The composition of Ext.

      Equations
      Instances For
        theorem CategoryTheory.Abelian.Ext.comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {T : C} {a₁ : } {a₂ : } {a₃ : } {a₁₂ : } {a₂₃ : } {a : } (α : CategoryTheory.Abelian.Ext X Y a₁) (β : CategoryTheory.Abelian.Ext Y Z a₂) (γ : CategoryTheory.Abelian.Ext Z T a₃) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h : a₁ + a₂ + a₃ = a) :
        (α.comp β h₁₂).comp γ = α.comp (β.comp γ h₂₃)
        @[simp]
        theorem CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {T : C} {a₁ : } {a₃ : } {a₁₃ : } (α : CategoryTheory.Abelian.Ext X Y a₁) (β : CategoryTheory.Abelian.Ext Y Z 0) (γ : CategoryTheory.Abelian.Ext Z T a₃) (h₁₃ : a₁ + a₃ = a₁₃) :
        (α.comp β ).comp γ h₁₃ = α.comp (β.comp γ ) h₁₃
        @[simp]
        theorem CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {T : C} {a₁ : } {a₂ : } {a₁₂ : } (α : CategoryTheory.Abelian.Ext X Y a₁) (β : CategoryTheory.Abelian.Ext Y Z a₂) (γ : CategoryTheory.Abelian.Ext Z T 0) (h₁₂ : a₁ + a₂ = a₁₂) :
        (α.comp β h₁₂).comp γ = α.comp (β.comp γ ) h₁₂

        When an instance of [HasDerivedCategory.{w'} C] is available, this is the bijection between Ext.{w} X Y n and a type of morphisms in the derived category.

        Equations
        Instances For
          @[reducible, inline]

          The morphism in the derived category which corresponds to an element in Ext X Y a.

          Equations
          • α.hom = CategoryTheory.Abelian.Ext.homEquiv α
          Instances For
            @[simp]
            theorem CategoryTheory.Abelian.Ext.comp_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} [HasDerivedCategory C] {a : } {b : } (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : } (h : a + b = c) :
            (α.comp β h).hom = α.hom.comp β.hom

            The canonical map (X ⟶ Y) → Ext X Y 0.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The abelian group structure on Ext X Y n is defined by transporting the abelian group structure on the constructed derived category (given by HasDerivedCategory.standard). This constructed derived category is used in order to obtain most of the compatibilities satisfied by this abelian group structure. It is then shown that the bijection homEquiv between Ext X Y n and Hom-types in the derived category can be promoted to an additive equivalence for any [HasDerivedCategory C] instance.

              Equations
              • CategoryTheory.Abelian.Ext.instAddCommGroup = CategoryTheory.Abelian.Ext.homEquiv.addCommGroup
              @[reducible, inline]

              The map from Ext X Y n to a ShiftedHom type in the constructed derived category given by HasDerivedCategory.standard: this definition is introduced only in order to prove properties of the abelian group structure on Ext-groups. Do not use this definition: use the more general hom instead.

              Equations
              • α.hom' = α.hom
              Instances For
                @[simp]
                theorem CategoryTheory.Abelian.Ext.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {n : } (α₁ : CategoryTheory.Abelian.Ext X Y n) (α₂ : CategoryTheory.Abelian.Ext X Y n) {m : } (β : CategoryTheory.Abelian.Ext Y Z m) {p : } (h : n + m = p) :
                (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
                @[simp]
                theorem CategoryTheory.Abelian.Ext.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {n : } (α : CategoryTheory.Abelian.Ext X Y n) {m : } (β₁ : CategoryTheory.Abelian.Ext Y Z m) (β₂ : CategoryTheory.Abelian.Ext Y Z m) {p : } (h : n + m = p) :
                α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
                @[simp]
                theorem CategoryTheory.Abelian.Ext.neg_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {n : } (α : CategoryTheory.Abelian.Ext X Y n) {m : } (β : CategoryTheory.Abelian.Ext Y Z m) {p : } (h : n + m = p) :
                (-α).comp β h = -α.comp β h
                @[simp]
                theorem CategoryTheory.Abelian.Ext.comp_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {Z : C} {n : } (α : CategoryTheory.Abelian.Ext X Y n) {m : } (β : CategoryTheory.Abelian.Ext Y Z m) {p : } (h : n + m = p) :
                α.comp (-β) h = -α.comp β h
                @[simp]
                theorem CategoryTheory.Abelian.Ext.comp_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {n : } (α : CategoryTheory.Abelian.Ext X Y n) (Z : C) (m : ) (p : ) (h : n + m = p) :
                α.comp 0 h = 0
                theorem CategoryTheory.Abelian.Ext.biprod_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {Y : C} {n : } {X₁ : C} {X₂ : C} {α : CategoryTheory.Abelian.Ext (X₁ X₂) Y n} {β : CategoryTheory.Abelian.Ext (X₁ X₂) Y n} (h₁ : (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp α = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp β ) (h₂ : (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp α = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp β ) :
                α = β

                When an instance of [HasDerivedCategory.{w'} C] is available, this is the additive bijection between Ext.{w} X Y n and a type of morphisms in the derived category.

                Equations
                • CategoryTheory.Abelian.Ext.homAddEquiv = { toEquiv := CategoryTheory.Abelian.Ext.homEquiv, map_add' := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.Abelian.Ext.homAddEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X : C} {Y : C} {n : } [HasDerivedCategory C] (α : CategoryTheory.Abelian.Ext X Y n) :
                  CategoryTheory.Abelian.Ext.homAddEquiv α = α.hom
                  @[simp]
                  theorem CategoryTheory.Abelian.Ext.bilinearComp_apply_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) (Y : C) (Z : C) (a : ) (b : ) (c : ) (h : a + b = c) (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) :
                  ((CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h) α) β = α.comp β h

                  The composition of Ext, as a bilinear map.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible, inline]

                    The postcomposition Ext X Y a →+ Ext X Z b with β : Ext Y Z n when a + n = b.

                    Equations
                    Instances For
                      @[reducible, inline]

                      The precomposition Ext Y Z a →+ Ext X Z b with α : Ext X Y n when n + a = b.

                      Equations
                      Instances For

                        Auxiliary definition for extFunctor.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The functor Cᵒᵖ ⥤ C ⥤ AddCommGrp which sends X : C and Y : C to Ext X Y n.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For