Base change of Fitting ideals

For an R-algebra S and a finite R-module M, the Fitting ideals of S ⊗[R] M are the extensions of those of M: Fitt_k(S ⊗[R] M) = Fitt_k(M) S. A surjection from a finite free module onto M base changes to a surjection onto S ⊗[R] M. By right exactness of the tensor product, its kernel is the base change of the original kernel, and the minors of these relations generate the extension of the ideal of minors of the original relations.

Since localization is a base change (IsLocalizedModule.isBaseChange), the Fitting ideals of a module commute with localization. This is the compatibility needed for the Fitting ideals of a quasi-coherent module of finite type to glue to a quasi-coherent ideal sheaf; for the sheaf of relative differentials, this compatibility is used in constructing the intended singular-locus ideal.

Base change to a field K detects the rank of the fibre: Fitt_k(M) extends to the zero ideal of K exactly when K ⊗[R] M has dimension greater than k. For the residue field κ(p) of a prime p, this identifies the zero locus of Fitt_k(M): Fitt_k(M) ⊆ p exactly when the fibre κ(p) ⊗[R] M has dimension greater than k.

Main results

• IsBaseChange.minorsIdeal_span_image: the minors ideals of the S-span of the image of a submodule N of a free module of finite rank under a base change are the extensions of the minors ideals of N.
• Submodule.minorsIdeal_baseChange: the same for N.baseChange S.
• TauCeti.fittingIdeal_baseChange: Fitt_k(S ⊗[R] M) = Fitt_k(M) S.
• IsBaseChange.fittingIdeal_eq_map: the same for any base change of M, in particular for a localization of M.
• TauCeti.fittingIdeal_map_eq_bot_iff_lt_finrank: Fitt_k(M) K = 0 for a field K exactly when k < dim_K K ⊗[R] M.
• TauCeti.fittingIdeal_le_iff_lt_finrank: Fitt_k(M) ⊆ p exactly when k < dim_{κ(p)} κ(p) ⊗[R] M.

References

• Stacks Project, Tag 07ZA, part (3): Fitting ideals commute with base change.
• Stacks Project, Tag 07ZC, for the description of the zero locus of Fitt_k(M) by the dimensions of the fibres of M.

theorem IsBaseChange.minorsIdeal_span_image {R : Type u_1} {S : Type u_2} {F : Type u_3} {W : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup F] [Module R F] [AddCommGroup W] [Module R W] [Module S W] [IsScalarTower R S W] {j : F →ₗ[R] W} [Module.Free R F] [Module.Finite R F] (hj : IsBaseChange S j) (N : Submodule R F) (p : ℕ) : (Submodule.span S (⇑j '' ↑N)).minorsIdeal p = Ideal.map (algebraMap R S) (N.minorsIdeal p)

Let j : F → W exhibit W as the base change of a free R-module F of finite rank to S. The minors ideals of the S-submodule of W spanned by the image of a submodule N of F are the extensions to S of the minors ideals of N.

@[simp]

theorem Submodule.minorsIdeal_baseChange {R : Type u_1} {F : Type u_2} (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] (N : Submodule R F) (p : ℕ) : (baseChange S N).minorsIdeal p = Ideal.map (algebraMap R S) (N.minorsIdeal p)

The minors ideals of the base change of a submodule of a free module of finite rank are the extensions of its minors ideals.

@[simp]

theorem TauCeti.fittingIdeal_baseChange {R : Type u_1} (M : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.Finite R M] (k : ℕ) : fittingIdeal S (TensorProduct R S M) k = Ideal.map (algebraMap R S) (fittingIdeal R M k)

Fitting ideals commute with base change: Fitt_k(S ⊗[R] M) = Fitt_k(M) S.

theorem IsBaseChange.fittingIdeal_eq_map {R : Type u_1} {M : Type u_2} {M' : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup M'] [Module R M'] [Module S M'] [IsScalarTower R S M'] {g : M →ₗ[R] M'} (hg : IsBaseChange S g) (k : ℕ) : TauCeti.fittingIdeal S M' k = Ideal.map (algebraMap R S) (TauCeti.fittingIdeal R M k)

Fitting ideals commute with base change: if g : M → M' exhibits M' as the base change of M to S, then Fitt_k(M') = Fitt_k(M) S. This applies to localizations of M by IsLocalizedModule.isBaseChange.

@[simp]

theorem TauCeti.fittingIdeal_map_eq_bot_iff_lt_finrank {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (K : Type u_4) [Field K] [Algebra R K] (k : ℕ) : Ideal.map (algebraMap R K) (fittingIdeal R M k) = ⊥ ↔ k < Module.finrank K (TensorProduct R K M)

The extension of Fitt_k(M) to a field K vanishes exactly when the fibre K ⊗[R] M has dimension greater than k.

@[simp]

theorem TauCeti.fittingIdeal_le_iff_lt_finrank {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Ideal R) [p.IsPrime] (k : ℕ) : fittingIdeal R M k ≤ p ↔ k < Module.finrank p.ResidueField (TensorProduct R p.ResidueField M)

The zero locus of the k-th Fitting ideal of a finite module M is the set of primes p at which the fibre κ(p) ⊗[R] M has dimension greater than k.