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.
Depth drops by one after quotienting by a regular element
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be Noetherian, let be finite, let lie in the Jacobson radical, and let be -regular. Then with .
Facts & Assumptions
Given: The Axiom of Choice and the data and regular element in the statement.
Proof
Regularity includes . Since acts injectively on , no nonzero element of is annihilated by . Thus .
Apply to . Multiplication by on each Ext group is zero because annihilates , so the long exact sequence yields , where . By step 1.1, the first nonzero Ext degree for is either a positive integer or . The sequence makes the first degree for equal when is finite and when all groups vanish. The Ext characterization gives the displayed depth formula with its stated convention.
Depends on
Used by
- Depth is additive for a flat local homomorphism Corollary
- Depth of a hypersurface quotient Example
- A normal Noetherian domain is the intersection of its height-one localizations Lemma
- A polynomial variable increases depth by one Lemma
- A regular parameter quotient preserves the depth--dimension gap Lemma
- A regular sequence lowers dimension exactly in a Cohen-Macaulay local ring Lemma
- Depth from first nonzero Koszul cohomology Lemma
- Depth is bounded by the quotient dimension at every associated prime Lemma
- finite residue field projective dimension forces depth equals dimension Lemma
- Localization gives the stated depth inequality Lemma
- Nilpotent-orbit tensor covariants extend and polarize Lemma
- normal domain implies s two Lemma
- Normality of the symmetric determinantal ring Lemma
- r one s two intersection of height one localisations Lemma
- Finite étale covers extend across the closed point of a regular local ring Theorem
- Radical, localization, and regular-quotient properties of depth Theorem
Dependency tree · two levels
13 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
- Depth and Cohen--Macaulay modules source treatment (standard reference, not scraped)