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 : ℕ.

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)

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

@[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

@[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

@[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

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.

@[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✝

@[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✝

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

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

@[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✝

@[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

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.

@[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

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

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