LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Nonzerodivisors from free differential summands in Noetherian local Q-algebras

Statement

Assume the Axiom of Choice. Let $R \to S$ be a homomorphism of commutative rings with $S$ a nonzero $Q$ -algebra, and let $f \in S$ . Assume that there is an $S$ -linear map $θ : Ω_{S / R} \to S$ with $θ (d f) = 1$ ; equivalently, $S d f$ is freely generated by $d f$ and $Ω_{S / R} = S d f \oplus C$ for an $S$ -submodule $C$ (then $θ$ is projection onto this free summand and $C = \ker θ$ ). Then $f$ is not nilpotent, and if $S$ is a Noetherian local ring then $f$ is a nonzerodivisor. No finiteness of $S$ over $R$ is assumed. The Axiom of Choice is inherited through the local-ring unit characterization and the Krull intersection theorem in the nonzerodivisor statement.

Facts & Assumptions

Given: A homomorphism $R \to S$ of commutative rings with $S$ a nonzero $Q$ -algebra, an element $f \in S$ , and an $S$ -linear map $θ : Ω_{S / R} \to S$ with $θ (d f) = 1$ .

[F1]

Universal Kähler differential module: $Ω_{S / R}$ is an $S$ -module with universal $R$ -derivation $d : S \to Ω_{S / R}$ ; $d$ is additive, satisfies $d (a b) = a d b + b d a$ and kills the image of $R$ , and composition $g \mapsto g \circ d$ is a bijection ${Hom}_{S} (Ω_{S / R}, M) \to {Der}_{R} (S, M)$ for every $S$ -module $M$ .

[F2]

Derivation of an algebra: an $R$ -derivation $D : S \to S$ is additive, kills the image of $R$ , and satisfies the Leibniz rule $D (a b) = a D (b) + b D (a)$ ; sums and scalar multiples of derivations are derivations.

[F3]

Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of $x$ and $1 - x$ is a unit for every $x$ : assuming Choice, in a nonzero local ring the nonunits are exactly the elements of the unique maximal ideal.

[F4]

The Jacobson radical of a ring: the Jacobson radical $J (S)$ is the intersection of the maximal ideals; combined with [F3], in a local ring $J (S)$ is the unique maximal ideal.

[F5]

The Krull intersection is the $(1 - a)$ -torsion submodule, and it vanishes in the Jacobson-radical case: for a Noetherian ring $S$ , an ideal $I$ and a finite $S$ -module $M$ , if $I \subseteq J (S)$ then $⋂_{n \geq 0} I^{n} M = 0$ .

Proof

1.1F1givenalgebra

The two hypotheses are equivalent: if $θ (d f) = 1$ then $S d f \cap \ker θ = 0$ , because $θ (s d f) = s$ vanishes only for $s = 0$ , and every element of $Ω_{S / R}$ is the sum of its $S d f$ -component $(θ (ω)) d f$ and its $\ker θ$ -component; conversely, such a decomposition with $S d f$ freely generated by $d f$ defines an $S$ -linear $θ$ by $θ (d f) = 1$ and $θ ∣_{C} = 0$ , so the displayed hypothesis and its reformulation agree.

1.2F1F2givenconstruct

Define $D : S \to S$ by $D (a) = θ (d a)$ . Then $D$ is an $R$ -derivation in the sense of [F2]: it is additive because $d$ and $θ$ are additive; it kills the image of $R$ because $d$ does and $θ$ is $S$ -linear; and it satisfies the Leibniz rule because $D (a b) = θ (a d b + b d a) = a θ (d b) + b θ (d a) = a D (b) + b D (a)$ . In particular $D (f) = θ (d f) = 1$ .

2.1F2step 1.2givenalgebra

The element $f$ is not nilpotent. Suppose $f^{n} = 0$ and let $n \geq 1$ be minimal with this property. If $n = 1$ , then $f = 0$ and $D (f) = D (0) = 0$ , contradicting $D (f) = 1$ . If $n \geq 2$ , then the Leibniz rule and induction on $n$ give $D (f^{n}) = n f^{n - 1} D (f) = n f^{n - 1}$ , while $D (f^{n}) = D (0) = 0$ ; since $n$ is invertible in the $Q$ -algebra $S$ , this forces $f^{n - 1} = 0$ , contradicting the minimality of $n$ . So no such $n$ exists.

2.2F2F3F4step 1.2algebra

Assume now that $S$ is a Noetherian local ring and let $a \in S$ with $f a = 0$ . If $f$ is a unit then $a = 0$ ; otherwise $f$ is a nonunit, so $f$ lies in the unique maximal ideal $m$ of $S$ by [F3], and $J (S) = m$ by [F4]. We prove $a \in (f^{n})$ for all $n \geq 1$ by induction. For $n = 1$ the Leibniz rule gives $0 = D (f a) = f D (a) + a D (f) = f D (a) + a$ , so $a = - f D (a) \in (f)$ . If $a = f^{n} b$ , then $0 = D (f^{n + 1} b) = (n + 1) f^{n} b + f^{n + 1} D (b)$ , so $f^{n} b = - (n + 1)^{- 1} f^{n + 1} D (b)$ and $a = f^{n + 1} (- (n + 1)^{- 1} D (b)) \in (f^{n + 1})$ , using that $n + 1$ is invertible in $S$ .

3.1F5step 2.2∎

By step 2.2, $a \in ⋂_{n \geq 1} (f^{n})$ , an intersection inside the finite $S$ -module $M = S$ ; since $(f) \subseteq m = J (S)$ and $S$ is Noetherian, the Krull intersection theorem [F5] gives $⋂_{n \geq 0} (f^{n}) = 0$ . Hence $a = 0$ , so $f a = 0$ implies $a = 0$ : the element $f$ is a nonzerodivisor.

Depends on

Used by

Free differentials imply regularity in characteristic zero Lemma

Dependency tree · two levels

21 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

The Stacks Project, Commutative Algebra chapter (standard reference, not scraped)