Annihilator ideal sheaves of quasi-coherent modules

Let M be a quasi-coherent 𝒪_X-module on a scheme X whose sections over every affine open are finitely generated, that is, a quasi-coherent module of finite type. The annihilators Ann(Γ(M, U)) ⊆ Γ(X, U) of its modules of sections over the affine opens U glue to a quasi-coherent ideal sheaf Ann(M) ⊆ 𝒪_X: over a basic open D(f) ⊆ U, the sections of M are the localization of Γ(M, U) at f, and annihilators of finite modules commute with localization.

The closed subscheme cut out by Ann(M) is a scheme structure on the support of M: a point lies in it exactly when the fibre M ⊗ κ(x) is nonzero. It has the same support as the zeroth Fitting ideal sheaf Fitt₀(M), but in general a different scheme structure. For the cokernel of 𝒪_X → ν_*𝒪_{X'} along a finite morphism ν : X' → X, such as the normalization of a reduced curve, the annihilator ideal sheaf is the conductor of ν.

Main definitions

• AlgebraicGeometry.Scheme.Modules.annihilator M hM: the annihilator ideal sheaf of a quasi-coherent module M with finitely generated modules of sections hM over affine opens.

Main results

• AlgebraicGeometry.Scheme.Modules.annihilator_ideal: over an affine open U, it is the annihilator of Γ(M, U).
• AlgebraicGeometry.Scheme.Modules.annihilator_congr: invariance under module isomorphisms.
• AlgebraicGeometry.Scheme.Modules.annihilator_Spec: the affine global-sections description.
• AlgebraicGeometry.Scheme.Modules.support_annihilator: Ann(M) and Fitt₀(M) have the same support.
• AlgebraicGeometry.Scheme.Modules.mem_support_annihilator_iff: a point x of an affine open U lies in the support of Ann(M) exactly when the fibre κ(x) ⊗ Γ(M, U) is nonzero.

References

• Stacks Project, Tag 01PB: quasi-coherent modules of finite type have finitely generated modules of sections over affine opens.
• Stacks Project, Tag 00L2: the support of a finite module is the zero locus of its annihilator.

noncomputable def AlgebraicGeometry.Scheme.Modules.annihilator {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑X.affineOpens), Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) : X.IdealSheafData

The annihilator ideal sheaf Ann(M) of a quasi-coherent module M whose sections over every affine open U form a finite Γ(X, U)-module: over U it is the annihilator of Γ(M, U). Its support is the set of points at which the fibre of M is nonzero (AlgebraicGeometry.Scheme.Modules.mem_support_annihilator_iff).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.annihilator_ideal {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑X.affineOpens), Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) (U : ↑X.affineOpens) : (M.annihilator hM).ideal U = Module.annihilator ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))

Over an affine open U, the annihilator ideal sheaf Ann(M) is the annihilator of the module of sections Γ(M, U).

theorem AlgebraicGeometry.Scheme.Modules.support_annihilator {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑X.affineOpens), Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) : (M.annihilator hM).support = (M.fittingIdeal hM 0).support

The annihilator ideal sheaf and the zeroth Fitting ideal sheaf have the same support, the set of points at which the fibre of M is nonzero.

theorem AlgebraicGeometry.Scheme.Modules.mem_support_annihilator_iff {X : Scheme} (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑X.affineOpens), Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) {x : ↥X} {U : ↑X.affineOpens} (hx : x ∈ ↑U) : x ∈ (M.annihilator hM).support ↔ 0 < Module.finrank (↑(X.residueField x)) (TensorProduct ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(X.residueField x) ↑(M.presheaf.obj (Opposite.op ↑U)))

The support of an annihilator ideal sheaf. A point x of an affine open U lies in the support of Ann(M) exactly when the fibre κ(x) ⊗ Γ(M, U) of M at x is nonzero.

theorem AlgebraicGeometry.Scheme.Modules.annihilator_congr {X : Scheme} {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑X.affineOpens), Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) (e : M ≅ N) : have hN := ⋯; M.annihilator hM = N.annihilator hN

Isomorphic quasicoherent modules have the same annihilator ideal sheaves.

theorem AlgebraicGeometry.Scheme.Modules.annihilator_ideal_top_Spec {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑(Spec R).affineOpens), Module.Finite ↑((Spec R).presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) : (M.annihilator hM).ideal ⟨⊤, ⋯⟩ = Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (Module.annihilator ↑R ↑(M.presheaf.obj (Opposite.op ⊤)))

On a spectrum, the annihilator ideal of global sections is the image of the annihilator computed over the original ring under the canonical global-sections isomorphism.

theorem AlgebraicGeometry.Scheme.Modules.annihilator_Spec {R : CommRingCat} (M : (Spec R).Modules) [SheafOfModules.IsQuasicoherent M] (hM : ∀ (U : ↑(Spec R).affineOpens), Module.Finite ↑((Spec R).presheaf.obj (Opposite.op ↑U)) ↑(M.presheaf.obj (Opposite.op ↑U))) : M.annihilator hM = IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (Module.annihilator ↑R ↑(M.presheaf.obj (Opposite.op ⊤))))

The annihilator ideal sheaf of a quasicoherent module on a spectrum is generated by the annihilator of its module of global sections.