Fitting ideals

Let M be a finite module over a commutative ring R, and choose a surjection φ : F → M from a free module of finite rank n. The k-th Fitting ideal of M is the ideal generated by the (n - k) × (n - k) minors of the relations ker φ. It does not depend on the choice of φ. For a finite module, Fitt_k(M) cuts out the locus of primes at which M needs more than k generators; for a syntomic relative curve of dimension one, the first Fitting ideal of its module of differentials cuts out its singular locus.

To make the independence of the presentation transparent, the minors are formed with arbitrary linear functionals rather than with coordinates. For a submodule N of a module F, the ideal N.minorsIdeal p is generated by the determinants det (f j (v i)) of p linear functionals f j on F evaluated at p elements v i of N. For F = Fin n → R, taking coordinate functionals shows that every p × p minor of a matrix whose columns lie in N is such a determinant. Conversely, by the Cauchy–Binet formula, every such determinant is a combination of these minors. This formulation is manifestly invariant under linear equivalences of F.

The independence of the presentation reduces to two computations. Adjoining a free summand R to both F and N shifts the minors ideals by one. Two surjections φ : F → M and ψ : F' → M both factor through φ + ψ : F × F' → M, whose kernel is carried by a shear automorphism of F × F' onto ker φ × F'.

Main definitions

• Submodule.minorsIdeal N p: the ideal generated by the p × p determinants of linear functionals on F evaluated at elements of N.
• TauCeti.fittingIdeal R M k: the k-th Fitting ideal of the R-module M.

Main results

• Submodule.minorsIdeal_prod_top: adjoining a free summand of rank r shifts the minors ideals by r.
• Submodule.minorsIdeal_ker_eq_of_surjective: the minors ideals of the kernels of two surjections from free modules of finite rank onto the same module agree after the shift by the ranks.
• TauCeti.fittingIdeal_eq_minorsIdeal_ker: the Fitting ideals may be computed from any surjection from a free module of finite rank.
• TauCeti.fittingIdeal_monotone: Fitt₀(M) ≤ Fitt₁(M) ≤ ⋯.
• TauCeti.fittingIdeal_prod_add_finrank: adjoining a free summand of rank r to the module shifts its Fitting ideals by r.
• TauCeti.fittingIdeal_le_of_surjective: Fitting ideals grow along surjections.
• TauCeti.fittingIdeal_eq_top_of_surjective: Fitt_k(M) = ⊤ once M is generated by k elements.
• TauCeti.fittingIdeal_eq_bot_of_lt_finrank: a free module of rank n has Fitt_k = ⊥ for k < n.
• TauCeti.fittingIdeal_eq_top_iff_finrank_le: over a nontrivial ring, a free module of rank n has Fitt_k = ⊤ exactly when n ≤ k.
• TauCeti.fittingIdeal_quotient_zero: Fitt₀(R ⧸ I) = I.

References

• Stacks Project, Tag 07Z6
• Stacks Project, Tag 07ZA

def Submodule.minorsIdeal {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (N : Submodule R F) (p : ℕ) : Ideal R

The ideal of p × p minors of a submodule N of F: the ideal generated by the determinants det (f j (v i)) of p linear functionals f j on F evaluated at p elements v i of N.

Equations

• N.minorsIdeal p = Ideal.span {r : R | ∃ (f : Fin p → Module.Dual R F) (v : Fin p → F), (∀ (i : Fin p), v i ∈ N) ∧ (Matrix.of fun (i j : Fin p) => (f j) (v i)).det = r}

theorem Submodule.det_mem_minorsIdeal {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {N : Submodule R F} {p : ℕ} (f : Fin p → Module.Dual R F) {v : Fin p → F} (hv : ∀ (i : Fin p), v i ∈ N) : (Matrix.of fun (i j : Fin p) => (f j) (v i)).det ∈ N.minorsIdeal p

Each determinant det (f j (v i)) with all v i ∈ N lies in the ideal of minors.

theorem Submodule.minorsIdeal_le_iff {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {N : Submodule R F} {p : ℕ} {I : Ideal R} : N.minorsIdeal p ≤ I ↔ ∀ (f : Fin p → Module.Dual R F) (v : Fin p → F), (∀ (i : Fin p), v i ∈ N) → (Matrix.of fun (i j : Fin p) => (f j) (v i)).det ∈ I

The ideal of minors is contained in I exactly when all its generating determinants are.

@[simp]

theorem Submodule.minorsIdeal_zero {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (N : Submodule R F) : N.minorsIdeal 0 = ⊤

The ideal of 0 × 0 minors is the unit ideal.

theorem Submodule.minorsIdeal_succ_le {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (N : Submodule R F) (p : ℕ) : N.minorsIdeal (p + 1) ≤ N.minorsIdeal p

Laplace expansion along the first row: every (p + 1) × (p + 1) minor is a combination of p × p minors.

theorem Submodule.minorsIdeal_antitone {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (N : Submodule R F) : Antitone N.minorsIdeal

The minors ideals decrease with the size of the minors.

theorem Submodule.minorsIdeal_mono {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {N N' : Submodule R F} (h : N ≤ N') (p : ℕ) : N.minorsIdeal p ≤ N'.minorsIdeal p

The minors ideals grow with the submodule.

theorem Submodule.minorsIdeal_map_le {R : Type u_1} {F : Type u_2} {F' : Type u_3} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup F'] [Module R F'] (φ : F →ₗ[R] F') (N : Submodule R F) (p : ℕ) : (map φ N).minorsIdeal p ≤ N.minorsIdeal p

The minors ideals can only shrink under a linear map, since functionals pull back.

@[simp]

theorem Submodule.minorsIdeal_map_equiv {R : Type u_1} {F : Type u_2} {F' : Type u_3} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup F'] [Module R F'] (e : F ≃ₗ[R] F') (N : Submodule R F) (p : ℕ) : (map (↑e) N).minorsIdeal p = N.minorsIdeal p

The minors ideals are invariant under linear equivalences of the ambient module.

@[simp]

theorem Submodule.minorsIdeal_comap_equiv {R : Type u_1} {F : Type u_2} {F' : Type u_3} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup F'] [Module R F'] (e : F ≃ₗ[R] F') (N : Submodule R F') (p : ℕ) : (comap (↑e) N).minorsIdeal p = N.minorsIdeal p

The minors ideals are invariant under linear equivalences of the ambient module.

@[simp]

theorem Submodule.minorsIdeal_bot {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (p : ℕ) : ⊥.minorsIdeal (p + 1) = ⊥

The zero submodule has no nonzero minors of positive size.

theorem Submodule.minorsIdeal_prod_top {R : Type u_1} {F : Type u_2} {G : Type u_4} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup G] [Module R G] [Module.Free R G] [Module.Finite R G] (N : Submodule R F) (p : ℕ) : (N.prod ⊤).minorsIdeal (p + Module.finrank R G) = N.minorsIdeal p

Adjoining a free summand G of finite rank shifts the minors ideals by the rank of G.

@[simp]

theorem Submodule.minorsIdeal_prod_bot {R : Type u_1} {F : Type u_2} {G : Type u_4} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup G] [Module R G] (N : Submodule R F) (p : ℕ) : (N.prod ⊥).minorsIdeal p = N.minorsIdeal p

Adjoining a summand G with no relations leaves the minors ideals unchanged.

theorem Submodule.minorsIdeal_ker_eq_of_surjective {R : Type u_1} {F : Type u_2} {F' : Type u_3} {M : Type u_5} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup F'] [Module R F'] [AddCommGroup M] [Module R M] [Module.Free R F] [Module.Finite R F] [Module.Free R F'] [Module.Finite R F'] {φ : F →ₗ[R] M} {ψ : F' →ₗ[R] M} (hφ : Function.Surjective ⇑φ) (hψ : Function.Surjective ⇑ψ) (k : ℕ) : φ.ker.minorsIdeal (Module.finrank R F - k) = ψ.ker.minorsIdeal (Module.finrank R F' - k)

Independence of the presentation. For two surjections φ : F → M and ψ : F' → M from free modules of finite rank, the minors ideals of their kernels of sizes rank F - k and rank F' - k agree.

@[simp]

theorem Ideal.minorsIdeal_one {R : Type u_1} [CommRing R] (I : Ideal R) : Submodule.minorsIdeal I 1 = I

The ideal of 1 × 1 minors of an ideal, viewed as a submodule of R, is the ideal itself.

noncomputable def TauCeti.fittingIdeal (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (k : ℕ) : Ideal R

The k-th Fitting ideal of a finite R-module M. For a presentation as a quotient of Fin n → R, it is the ideal of (n - k) × (n - k) minors of the relations; this does not depend on the presentation (TauCeti.fittingIdeal_eq_minorsIdeal_ker).

Equations

• TauCeti.fittingIdeal R M k = ⋯.choose.ker.minorsIdeal (⋯.choose - k)

theorem TauCeti.fittingIdeal_eq_minorsIdeal_ker {R : Type u_1} {F : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R F] [Module.Finite R F] {φ : F →ₗ[R] M} (hφ : Function.Surjective ⇑φ) (k : ℕ) : fittingIdeal R M k = φ.ker.minorsIdeal (Module.finrank R F - k)

The Fitting ideals of a module may be computed from any surjection from a free module of finite rank.

theorem TauCeti.fittingIdeal_monotone (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Monotone (fittingIdeal R M)

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

theorem TauCeti.fittingIdeal_eq_top_of_surjective {R : Type u_1} {F : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup F] [Module R F] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R F] [Module.Finite R F] {φ : F →ₗ[R] M} (hφ : Function.Surjective ⇑φ) {k : ℕ} (hk : Module.finrank R F ≤ k) : fittingIdeal R M k = ⊤

A module generated by n elements has Fitt_k = ⊤ for k ≥ n.

theorem TauCeti.fittingIdeal_le_of_surjective {R : Type u_1} {M : Type u_3} {M' : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup M'] [Module R M'] [Module.Finite R M'] {q : M →ₗ[R] M'} (hq : Function.Surjective ⇑q) (k : ℕ) : fittingIdeal R M k ≤ fittingIdeal R M' k

The Fitting ideals grow along surjections.

theorem TauCeti.fittingIdeal_congr {R : Type u_1} {M : Type u_3} {M' : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup M'] [Module R M'] [Module.Finite R M'] (e : M ≃ₗ[R] M') (k : ℕ) : fittingIdeal R M k = fittingIdeal R M' k

Isomorphic modules have the same Fitting ideals.

theorem TauCeti.fittingIdeal_prod_add_finrank (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (G : Type u_5) [AddCommGroup G] [Module R G] [Module.Free R G] [Module.Finite R G] (k : ℕ) : fittingIdeal R (M × G) (k + Module.finrank R G) = fittingIdeal R M k

Adjoining a free summand G of finite rank shifts the Fitting ideals by the rank of G: Fitt_{k + rank G}(M × G) = Fitt_k(M).

theorem TauCeti.fittingIdeal_eq_bot_of_lt_finrank {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] {k : ℕ} (hk : k < Module.finrank R F) : fittingIdeal R F k = ⊥

A free module of rank n has Fitt_k = ⊥ for k < n.

@[simp]

theorem TauCeti.fittingIdeal_eq_top_iff_finrank_le {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] [Nontrivial R] [Module.Free R F] [Module.Finite R F] {k : ℕ} : fittingIdeal R F k = ⊤ ↔ Module.finrank R F ≤ k

A free module of rank n over a nontrivial ring has Fitt_k = ⊤ exactly when n ≤ k.

@[simp]

theorem TauCeti.fittingIdeal_quotient_zero {R : Type u_1} [CommRing R] (I : Ideal R) : fittingIdeal R (R ⧸ I) 0 = I

The zeroth Fitting ideal of R ⧸ I is I.