The content of a submodule of a projective module

Let M be a module over a commutative ring A and N a submodule of M. The ideal N.minorsIdeal 1 of 1 × 1 minors is the ideal of A generated by the values φ x of all linear functionals φ : M →ₗ[A] A at all x ∈ N (Submodule.minorsIdeal_one_le_iff). When M is projective, it is the smallest ideal 𝔞 of A with N ≤ 𝔞 • M (Submodule.minorsIdeal_one_le_iff_le_smul_top): the content of N in the sense of Ohm and Rush.

The point of the content of a submodule of a projective module is that it computes where N vanishes after base change: for an A-algebra A', the image of N in A' ⊗[A] M is zero exactly when A → A' kills N.minorsIdeal 1 (IsBaseChange.minorsIdeal_one_le_ker_iff). The content itself commutes with base change (IsBaseChange.minorsIdeal_one_span_image), and for an ideal J of an A-algebra B which is projective as an A-module, the content of the extension of J to a pushout A' ⊗[A] B is the extension of the content of J (Ideal.minorsIdeal_one_restrictScalars_map). For finite projective M, the base change of the minors ideals of every size is IsBaseChange.minorsIdeal_span_image.

Geometrically, if Spec B → Spec A is finite locally free and J ⊆ B cuts out a closed subscheme Z ⊆ Spec B, the closed subscheme of Spec A cut out by the content of J is the locus over which Spec B lies inside Z: the Weil restriction of Z along Spec B → Spec A.

Main results

• Submodule.minorsIdeal_one_le_iff: the ideal of 1 × 1 minors lies in 𝔞 exactly when every functional maps N into 𝔞.
• Submodule.minorsIdeal_le_minorsIdeal_one_pow: the ideal of p × p minors lies in the p-th power of the content.
• Submodule.minorsIdeal_one_span_singleton: for a module with a basis, the content of A ∙ w is generated by the coordinates of w.
• Submodule.FG.minorsIdeal_one: if N and the dual of M are finitely generated, so is N.minorsIdeal 1.
• Submodule.iSup_minorsIdeal_one_map_eq: the contents of the images of N under a linearly varying family of maps are generated by those for a spanning set of parameters.
• Submodule.minorsIdeal_one_le_iff_le_smul_top: for projective M, N.minorsIdeal 1 is the smallest ideal 𝔞 with N ≤ 𝔞 • ⊤.
• IsBaseChange.minorsIdeal_one_le_ker_iff: for projective M, the image of N in the base change of M along A → A' is zero exactly when A → A' kills N.minorsIdeal 1.
• IsBaseChange.minorsIdeal_one_span_image: for projective M, the ideal of 1 × 1 minors of the image of N in a base change of M is the extension of that of N.
• Ideal.minorsIdeal_one_restrictScalars_map: the ideal version, for pushouts of algebras.

References

• J. Ohm and D. E. Rush, Content modules and algebras, Math. Scand. 31 (1972), 49–68.
• S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, §7.6, for Weil restriction.

theorem LinearMap.apply_mem_minorsIdeal_one {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {N : Submodule A M} (φ : Module.Dual A M) {x : M} (hx : x ∈ N) : φ x ∈ N.minorsIdeal 1

The value of a linear functional at an element of N is a 1 × 1 minor of N.

theorem Submodule.minorsIdeal_one_le_iff {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {N : Submodule A M} {𝔞 : Ideal A} : N.minorsIdeal 1 ≤ 𝔞 ↔ ∀ (φ : Module.Dual A M), ∀ x ∈ N, φ x ∈ 𝔞

The ideal of 1 × 1 minors of N lies in 𝔞 exactly when every functional maps N into 𝔞.

theorem Submodule.minorsIdeal_le_minorsIdeal_one_pow {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] (N : Submodule A M) (p : ℕ) : N.minorsIdeal p ≤ N.minorsIdeal 1 ^ p

Every p × p minor of N is a sum of products of p entries, so the ideal of p × p minors lies in the p-th power of the ideal of 1 × 1 minors.

theorem Submodule.FG.minorsIdeal_one {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Module.Finite A (Module.Dual A M)] {N : Submodule A M} (hN : N.FG) : (N.minorsIdeal 1).FG

The content of a finitely generated submodule is finitely generated when the dual module is finitely generated: it is generated by the values of finitely many generators of Dual A M at finitely many generators of N.

theorem Submodule.iSup_minorsIdeal_one_map_eq {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {M' : Type u_3} {R : Type u_4} {H : Type u_5} [AddCommGroup M'] [Module A M'] [CommSemiring R] [Algebra R A] [AddCommMonoid H] [Module R H] (N : Submodule A M) (f : H → M →ₗ[A] M') (hadd : ∀ (h h' : H), f (h + h') = f h + f h') (hsmul : ∀ (r : R) (h : H), f (r • h) = (algebraMap R A) r • f h) {s : Set H} (hs : span R s = ⊤) : ⨆ (h : H), (map (f h) N).minorsIdeal 1 = ⨆ (h : ↑s), (map (f ↑h) N).minorsIdeal 1

For a family of linear maps f h : M →ₗ[A] M' depending linearly on h in an R-module spanned by s, the contents of the images of N under all the f h are generated by those for h ∈ s.

theorem Submodule.minorsIdeal_one_span_singleton {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {ι : Type u_3} (b : Module.Basis ι A M) (w : M) : (A ∙ w).minorsIdeal 1 = Ideal.span (Set.range fun (i : ι) => (b.repr w) i)

For a module with a basis, the content of the submodule generated by one element is generated by the coordinates of that element.

theorem Submodule.le_minorsIdeal_one_smul_top {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Module.Projective A M] (N : Submodule A M) : N ≤ N.minorsIdeal 1 • ⊤

For projective M, every submodule N lies in N.minorsIdeal 1 • ⊤.

theorem LinearMap.apply_mem_map_minorsIdeal_one {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Module.Projective A M] {A' : Type u_3} [Semiring A'] [Algebra A A'] {N : Submodule A M} (χ : M →ₗ[A] A') {x : M} (hx : x ∈ N) : χ x ∈ Ideal.map (algebraMap A A') (N.minorsIdeal 1)

For projective M, an A-linear map to a possibly noncommutative A-algebra carries N into the extension of the content of N.

theorem Submodule.minorsIdeal_one_le_iff_le_smul_top {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Module.Projective A M] {N : Submodule A M} {𝔞 : Ideal A} : N.minorsIdeal 1 ≤ 𝔞 ↔ N ≤ 𝔞 • ⊤

The 1 × 1 minors as an Ohm–Rush content. For projective M, N.minorsIdeal 1 lies in an ideal 𝔞 exactly when N ≤ 𝔞 • ⊤: it is the smallest such ideal.

theorem IsBaseChange.minorsIdeal_one_le_ker_iff {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {A' : Type u_3} {M' : Type u_4} [CommSemiring A'] [Algebra A A'] [AddCommMonoid M'] [Module A' M'] [Module A M'] [IsScalarTower A A' M'] {f : M →ₗ[A] M'} (h : IsBaseChange A' f) [Module.Projective A M] {N : Submodule A M} : N.minorsIdeal 1 ≤ RingHom.ker (algebraMap A A') ↔ ∀ x ∈ N, f x = 0

For M projective and f : M → M' a base change of M along A → A', the submodule N maps to zero in M' exactly when A → A' kills the content N.minorsIdeal 1.

theorem IsBaseChange.minorsIdeal_one_span_image {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] {A' : Type u_3} {M' : Type u_4} [CommRing A'] [Algebra A A'] [AddCommGroup M'] [Module A' M'] [Module A M'] [IsScalarTower A A' M'] {f : M →ₗ[A] M'} (h : IsBaseChange A' f) [Module.Projective A M] (N : Submodule A M) : (Submodule.span A' (⇑f '' ↑N)).minorsIdeal 1 = Ideal.map (algebraMap A A') (N.minorsIdeal 1)

The content commutes with base change. For M projective and f : M → M' a base change of M along A → A', the content of the A'-submodule spanned by the image of N is the extension of the content of N.

theorem Ideal.minorsIdeal_one_restrictScalars_map {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CommRing A] [CommRing A'] [CommRing B] [CommRing B'] [Algebra A A'] [Algebra A B] [Algebra A' B'] [Algebra B B'] [Algebra A B'] [IsScalarTower A A' B'] [IsScalarTower A B B'] [h : Algebra.IsPushout A A' B B'] [Module.Projective A B] (J : Ideal B) : (Submodule.restrictScalars A' (map (algebraMap B B') J)).minorsIdeal 1 = map (algebraMap A A') ((Submodule.restrictScalars A J).minorsIdeal 1)

The content of an extended ideal. If B is projective as an A-module and B' is the pushout A' ⊗[A] B, the content over A' of the extension to B' of an ideal J of B is the extension of the content of J over A.