Fitting ideals over a local ring

Let M be a finite module over a local ring R with maximal ideal 𝔪 and residue field κ, and let μ = dim_κ κ ⊗[R] M be the minimal number of generators of M. Presenting M by a minimal set of generators, every relation has all its coordinates in 𝔪, so every p × p minor of the relations lies in 𝔪 ^ p. Hence

Fitt_k(M) ≤ 𝔪 ^ (μ - k).

In particular, if Fitt_k(M) is not contained in 𝔪², then M is generated by k + 1 elements. For the module of differentials of a curve this bounds the embedding dimension at a point where the singular locus, cut out by the first Fitting ideal, is reduced.

Main results

• TauCeti.fittingIdeal_le_maximalIdeal_pow: over a local ring, Fitt_k(M) ≤ 𝔪 ^ (dim_κ κ ⊗[R] M - k).

References

• Stacks Project, Tag 07ZA: Fitting ideals and their basic properties.

theorem TauCeti.fittingIdeal_le_maximalIdeal_pow {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (k : ℕ) : fittingIdeal R M k ≤ IsLocalRing.maximalIdeal R ^ (Module.finrank (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) M) - k)

Fitting ideals over a local ring. If M needs μ = dim_κ κ ⊗[R] M generators, then its k-th Fitting ideal lies in 𝔪 ^ (μ - k).