Annihilators of Ext groups of modules

For modules N and M over a commutative ring R, the R-module Ext N M n is killed both by the annihilator of N and by the annihilator of M, since multiplication by r on Ext N M n is induced by multiplication by r on either argument. In particular Ext N M n vanishes when these two annihilators are comaximal, for example Ext (R ⧸ I) M n = 0 when I M = M for a finite module M. A map out of a finite free module with image in I F, for an ideal I killing N, is a combination of maps with coefficients in I, so it induces zero on Ext N - n; for N the residue field of a local ring this is the property of minimal free presentations used to compute depths.

Main results

• CategoryTheory.Abelian.Ext.smul_eq_zero_of_mem_annihilator_left and CategoryTheory.Abelian.Ext.smul_eq_zero_of_mem_annihilator_right: elements of the annihilator of either argument act by zero on Ext N M n.
• CategoryTheory.Abelian.Ext.subsingleton_of_annihilator_sup_eq_top: Ext N M n vanishes when the annihilators of N and M are comaximal.
• CategoryTheory.Abelian.Ext.comp_mk₀_eq_zero_of_range_le_smul_top: if I annihilates N, a map K ⟶ F from a finite free module with image in I • ⊤ induces zero on Ext N - n.

theorem CategoryTheory.Abelian.Ext.smul_eq_zero_of_mem_annihilator_left {R : Type u} [CommRing R] [Small.{v, u} R] {N M : ModuleCat R} {r : R} (hr : r ∈ Module.annihilator R ↑N) {n : ℕ} (x : Ext N M n) : r • x = 0

An element of the annihilator of N acts by zero on Ext N M n. This restates Ext.postcomp_smul_id_eq_zero_of_mem_annihilator as a statement about the scalar action.

theorem CategoryTheory.Abelian.Ext.smul_eq_zero_of_mem_annihilator_right {R : Type u} [CommRing R] [Small.{v, u} R] {N M : ModuleCat R} {r : R} (hr : r ∈ Module.annihilator R ↑M) {n : ℕ} (x : Ext N M n) : r • x = 0

An element of the annihilator of M acts by zero on Ext N M n.

theorem CategoryTheory.Abelian.Ext.subsingleton_of_annihilator_sup_eq_top {R : Type u} [CommRing R] [Small.{v, u} R] {N M : ModuleCat R} (h : Module.annihilator R ↑N ⊔ Module.annihilator R ↑M = ⊤) (n : ℕ) : Subsingleton (Ext N M n)

Ext N M n vanishes when the annihilators of N and M are comaximal.

theorem CategoryTheory.Abelian.Ext.comp_mk₀_eq_zero_of_range_le_smul_top {R : Type u} [CommRing R] [Small.{v, u} R] {N K F : ModuleCat R} [Module.Free R ↑K] [Module.Finite R ↑K] {I : Ideal R} (hI : I ≤ Module.annihilator R ↑N) (f : K ⟶ F) (hf : (ModuleCat.Hom.hom f).range ≤ I • ⊤) {n : ℕ} (x : Ext N K n) : x.comp (mk₀ f) ⋯ = 0

Let the ideal I annihilate N, and let f : K ⟶ F be a map out of a finite free module whose image lies in I • F. Then f induces the zero map Ext N K n → Ext N F n.