Fitting 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. For k : ℕ, the k-th Fitting ideals Fitt_k(Γ(M, U)) ⊆ Γ(X, U) of its modules of sections over the affine opens U glue to a quasi-coherent ideal sheaf Fitt_k(M) ⊆ 𝒪_X: over a basic open D(f) ⊆ U, the sections of M are the localization of Γ(M, U) at f, and Fitting ideals commute with localization.

The closed subscheme cut out by Fitt_k(M) is supported exactly at the points x whose fibre M ⊗ κ(x) has dimension greater than k, so it is a scheme-theoretic structure on the locus where M needs more than k local generators. Applied to the sheaf of relative differentials of a relative curve, the first Fitting ideal defines the relative singular locus.

Main definitions

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

Main results

• AlgebraicGeometry.Scheme.Modules.fittingIdeal_ideal: over an affine open U, it is the Fitting ideal Fitt_k(Γ(M, U)).
• AlgebraicGeometry.Scheme.Modules.fittingIdeal_monotone: Fitt₀(M) ≤ Fitt₁(M) ≤ ⋯.
• AlgebraicGeometry.Scheme.Modules.fittingIdeal_congr: invariance under module isomorphisms.
• AlgebraicGeometry.Scheme.Modules.fittingIdeal_Spec: the affine global-sections description.
• AlgebraicGeometry.Scheme.Modules.mem_support_fittingIdeal_iff: a point x of an affine open U lies in the support of Fitt_k(M) exactly when k < dim_{κ(x)} κ(x) ⊗ Γ(M, U).

FittingIdeal.Pullback proves compatibility with arbitrary pullback of quasicoherent modules of finite type.

Implementation notes

The finiteness of M is the hypothesis that Γ(M, U) is a finite Γ(X, U)-module for every affine open U. For quasi-coherent modules this is equivalent to being of finite type (Stacks, Tag 01PB).

References

• Stacks Project, Tag 0C3C: Fitting ideals of a finite type quasi-coherent module.
• Stacks Project, Tag 0C3D: the zero loci of the Fitting ideals.

noncomputable def AlgebraicGeometry.Scheme.Modules.fittingIdeal {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))) (k : ℕ) : X.IdealSheafData

The k-th Fitting ideal sheaf Fitt_k(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 k-th Fitting ideal of Γ(M, U). Its support is the set of points at which the fibre of M has dimension greater than k (AlgebraicGeometry.Scheme.Modules.mem_support_fittingIdeal_iff).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.fittingIdeal_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))) (k : ℕ) (U : ↑X.affineOpens) : (M.fittingIdeal hM k).ideal U = TauCeti.fittingIdeal (↑(X.presheaf.obj (Opposite.op ↑U))) (↑(M.presheaf.obj (Opposite.op ↑U))) k

Over an affine open U, the Fitting ideal sheaf Fitt_k(M) is the k-th Fitting ideal of the module of sections Γ(M, U).

theorem AlgebraicGeometry.Scheme.Modules.fittingIdeal_monotone {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))) : Monotone (M.fittingIdeal hM)

The Fitting ideal sheaves increase: Fitt₀(M) ≤ Fitt₁(M) ≤ ⋯.

theorem AlgebraicGeometry.Scheme.Modules.mem_support_fittingIdeal_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) (k : ℕ) : x ∈ (M.fittingIdeal hM k).support ↔ k < Module.finrank (↑(X.residueField x)) (TensorProduct ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(X.residueField x) ↑(M.presheaf.obj (Opposite.op ↑U)))

The support of a Fitting ideal sheaf. A point x of an affine open U lies in the support of Fitt_k(M) exactly when the fibre κ(x) ⊗ Γ(M, U) of M at x has dimension greater than k, that is, when M needs more than k generators near x.

theorem AlgebraicGeometry.Scheme.Modules.fittingIdeal_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) (k : ℕ) : have hN := ⋯; M.fittingIdeal hM k = N.fittingIdeal hN k

Isomorphic quasicoherent modules have the same Fitting ideal sheaves.

theorem AlgebraicGeometry.Scheme.Modules.fittingIdeal_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))) (k : ℕ) : (M.fittingIdeal hM k).ideal ⟨⊤, ⋯⟩ = Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (TauCeti.fittingIdeal (↑R) (↑(M.presheaf.obj (Opposite.op ⊤))) k)

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

theorem AlgebraicGeometry.Scheme.Modules.fittingIdeal_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))) (k : ℕ) : M.fittingIdeal hM k = IdealSheafData.ofIdealTop (Ideal.map (CommRingCat.Hom.hom (ΓSpecIso R).inv) (TauCeti.fittingIdeal (↑R) (↑(M.presheaf.obj (Opposite.op ⊤))) k))

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