Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Ext-modules in linear categories #

In this file, we show that if C is an R-linear abelian category, then there is an R-module structure on the groups Ext X Y n for X and Y in C and n : ℕ.

source
@[instance_reducible]
noncomputable instance CategoryTheory.Abelian.Ext.instModule {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} :
Module R (Ext X Y n)
Equations
source
theorem CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀ {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} (x : Ext X Y n) (r : R) :
r • x = x.comp (mk₀ (r • CategoryStruct.id Y)) ⋯
source
@[simp]
theorem CategoryTheory.Abelian.Ext.smul_hom {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} (x : Ext X Y n) (r : R) [HasDerivedCategory C] :
(r • x).hom = r • x.hom
source
@[simp]
theorem CategoryTheory.Abelian.Ext.comp_smul {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) (r : R) :
α.comp (r • β) h = r • α.comp β h
source
@[simp]
theorem CategoryTheory.Abelian.Ext.smul_comp {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) (r : R) :
(r • α).comp β h = r • α.comp β h
source
noncomputable def CategoryTheory.Abelian.Ext.homLinearEquiv {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] :
Ext X Y n ≃ₗ[R] ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑n

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Abelian.Ext.homLinearEquiv_apply {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (a✝ : Ext X Y n) :
    homLinearEquiv a✝ = homAddEquiv.toFun a✝
    source
    @[simp]
    theorem CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (a✝ : ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑n) :
    homLinearEquiv.symm a✝ = homAddEquiv.invFun a✝
    source
    theorem CategoryTheory.Abelian.Ext.mk₀_smul {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} (r : R) (f : X ⟶ Y) :
    mk₀ (r • f) = r • mk₀ f
    source
    noncomputable def CategoryTheory.Abelian.Ext.linearEquiv₀ {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} :
    Ext X Y 0 ≃ₗ[R] X ⟶ Y

    The linear equivalence Ext X Y 0 ≃ₜ[R] (X ⟶ Y).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} (a✝ : X ⟶ Y) :
      linearEquiv₀.symm a✝ = mk₀ a✝
      source
      @[simp]
      theorem CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply {R : Type t} [Ring R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] {X Y : C} (f : Ext X Y 0) :
      mk₀ (linearEquiv₀ f) = f
      source
      noncomputable def CategoryTheory.Abelian.Ext.bilinearCompOfLinear {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (R : Type t) [CommRing R] [Linear R C] (X Y Z : C) (a b c : ℕ) (h : a + b = c) :
      Ext X Y a →ₗ[R] Ext Y Z b →ₗ[R] Ext X Z c

      The composition of Ext, as a bilinear map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Abelian.Ext.bilinearCompOfLinear_apply_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (R : Type t) [CommRing R] [Linear R C] (X Y Z : C) (a b c : ℕ) (h : a + b = c) (α : Ext X Y a) (β : Ext Y Z b) :
        ((bilinearCompOfLinear R X Y Z a b c h) α) β = α.comp β h
        source
        @[reducible, inline]
        noncomputable abbrev CategoryTheory.Abelian.Ext.postcompOfLinear {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {Y Z : C} {n : ℕ} (β : Ext Y Z n) (R : Type t) [CommRing R] [Linear R C] (X : C) {a b : ℕ} (h : a + n = b) :
        Ext X Y a →ₗ[R] Ext X Z b

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

        Equations
        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev CategoryTheory.Abelian.Ext.precompOfLinear {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : Ext X Y n) (R : Type t) [CommRing R] [Linear R C] (Z : C) {a b : ℕ} (h : n + a = b) :
          Ext Y Z a →ₗ[R] Ext X Z b

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            noncomputable def CategoryTheory.Abelian.linearExtFunctorObj (R : Type t) [CommRing R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (X : C) (n : ℕ) :
            Functor C (ModuleCat R)

            Auxiliary definition for linearExtFunctor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Abelian.linearExtFunctorObj_obj_carrier (R : Type t) [CommRing R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (X : C) (n : ℕ) (Y : C) :
              ↑((linearExtFunctorObj R X n).obj Y) = Ext X Y n
              source
              @[simp]
              theorem CategoryTheory.Abelian.linearExtFunctorObj_map (R : Type t) [CommRing R] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (X : C) (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
              (linearExtFunctorObj R X n).map f = ModuleCat.ofHom ((Ext.mk₀ f).postcompOfLinear R X ⋯)
              source
              @[implicit_reducible]
              noncomputable def CategoryTheory.Abelian.linearExtFunctor (R : Type t) [CommRing R] (C : Type u) [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (n : ℕ) :
              Functor Cᵒᵖ (Functor C (ModuleCat R))

              The functor Cᵒᵖ ⥤ C ⥤ ModuleCat R 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
                source
                @[simp]
                theorem CategoryTheory.Abelian.linearExtFunctor_obj (R : Type t) [CommRing R] (C : Type u) [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (n : ℕ) (X : Cᵒᵖ) :
                (linearExtFunctor R C n).obj X = linearExtFunctorObj R (Opposite.unop X) n
                source
                @[simp]
                theorem CategoryTheory.Abelian.linearExtFunctor_map_app (R : Type t) [CommRing R] (C : Type u) [Category.{v, u} C] [Abelian C] [Linear R C] [HasExt C] (n : ℕ) {X₁ X₂ : Cᵒᵖ} (f : X₁ ⟶ X₂) (Y : C) :
                ((linearExtFunctor R C n).map f).app Y = ModuleCat.ofHom ((Ext.mk₀ f.unop).precompOfLinear R Y ⋯)