TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Support of a tensor product of finite modules is the intersection of the supports

Statement

If $M$ and $N$ are finitely generated left $R$ -modules, then ${Supp}_{R} (M \otimes_{R} N) = {Supp}_{R} (M) \cap {Supp}_{R} (N) .$

Facts & Assumptions

Given: A commutative ring $R$ and finitely generated left $R$ -modules $M, N$ .

[L1]

For a finite module, the support is the set of primes containing its annihilator (For a finite module, support is the set of primes containing the annihilator).

[L2]

Localisation is naturally tensoring with the localised ring, so $(M \otimes_{R} N)_{p} ≅ M_{p} \otimes_{R_{p}} N_{p}$ (Localisation of modules is extension of scalars).

[L3]

The ring $R_{p}$ is local with maximal ideal $p R_{p}$ , and its residue field is $k (p) = R_{p} / p R_{p}$ ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ , $R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$ ).

[L4]

Tensoring preserves surjections, and nonzero finite-dimensional vector spaces over a field have nonzero tensor product (Tensoring is right exact, $R^{m} \otimes_{R} R^{n} ≅ R^{m n}$ with the product basis, and $\dim_{F} (V \otimes_{F} W) = \dim_{F} V \dim_{F} W$ ).

[L5]

A finitely generated module admits finite generators, and for a positive-size square matrix $A$ over a commutative ring one has $A adj (A) = \det (A) I$ (Generated submodule, cyclic and finitely generated modules, module basis and free module, For every positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ ).

Proof

technique · direct

1.1L1givenalgebra

Because $M$ and $N$ are finite, $M \otimes_{R} N$ is finite: if $m_{1}, \dots, m_{r}$ generate $M$ and $n_{1}, \dots, n_{s}$ generate $N$ , then the tensors $m_{i} \otimes n_{j}$ generate $M \otimes_{R} N$ . If $p \in {Supp}_{R} (M \otimes_{R} N)$ , then [L1] gives ${Ann}_{R} (M \otimes_{R} N) \subseteq p$ . Every element of ${Ann}_{R} (M)$ and every element of ${Ann}_{R} (N)$ annihilates every elementary tensor, so ${Ann}_{R} (M) + {Ann}_{R} (N) \subseteq {Ann}_{R} (M \otimes_{R} N)$ . Thus $p$ contains both annihilators, and [L1] gives $p \in {Supp}_{R} (M) \cap {Supp}_{R} (N)$ .

1.2L2L3

Conversely, let $p \in {Supp}_{R} (M) \cap {Supp}_{R} (N)$ . By [L2], it is enough to prove $M_{p} \otimes_{R_{p}} N_{p} \neq 0$ . Put $A = R_{p}$ , $m = p A$ , and $k = A / m$ ; by [L3], $A$ is a local ring with residue field $k$ .

1.3L3L5algebra

If $X$ is a finite nonzero $A$ -module, then $X / m X \neq 0$ . Indeed, if $X = m X$ , choose generators $x_{1}, \dots, x_{t}$ of $X$ and coefficients $a_{i j} \in m$ with $x_{i} = \sum_{j} a_{i j} x_{j}$ . Writing $B = (a_{i j})$ and $x = (x_{1}, \dots, x_{t})^{T}$ , this says $(I - B) x = 0$ . By [L5], $\det (I - B) x = 0$ . The determinant has the form $1 - a$ with $a \in m$ , so $1 - a \notin m$ and therefore is a unit in the local ring $A$ . Hence $x = 0$ and $X = 0$ , a contradiction.

2.1L4step 1.3

Apply step 1.3 to $M_{p}$ and $N_{p}$ . Since $p$ lies in both supports, these local modules are nonzero, so the $k$ -vector spaces $M_{p} / m M_{p}$ and $N_{p} / m N_{p}$ are nonzero. Tensoring the quotient maps with [L4] gives a surjection $M_{p} \otimes_{A} N_{p} ↠ (M_{p} / m M_{p}) \otimes_{A} (N_{p} / m N_{p})$ , and the target is the same as the tensor product over $k$ , hence nonzero by [L4]. Therefore $M_{p} \otimes_{A} N_{p} \neq 0$ .

3.1L2step 1.1step 2.1∎

Step 2.1 and [L2] give $p \in {Supp}_{R} (M \otimes_{R} N)$ . Together with step 1.1, this proves the support-intersection formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Proposition 13.30 (standard reference, not scraped)
The Stacks Project, Lemma 10.40.9 (standard reference, not scraped)