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.
In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
Statement
Assume the Axiom of Choice (The Axiom of Choice).
In a nonzero commutative ring, every proper ideal is contained in a maximal ideal.
Facts & Assumptions
Given: A nonzero commutative ring and a proper ideal .
A maximal ideal is a maximal proper ideal under inclusion (Prime ideals and maximal ideals in a commutative ring).
Ideals are additive subgroups with multiplication absorption (Left, right and two-sided ideals).
An ideal criterion and intersection closure are available (Ideal criteria and intersections of ideals).
Assuming the Axiom of Choice, a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).
A chain is a subset linearly ordered by the ambient order (Chain in a poset).
A maximal element has no strictly larger element in the poset (Maximal element and greatest element).
A nonzero ring has and ring operations distribute (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).
Proof
Let be the poset of proper ideals of containing , ordered by inclusion.
is nonempty, because is a proper ideal containing .
The empty chain of has an upper bound in : every member of is vacuously above all of its members, and is nonempty, so is such an upper bound.
A nonempty chain has an upper bound in : is an ideal containing , and it is proper, since would place in some member of , forcing that member to equal and contradicting its properness.
Every chain of has an upper bound in , and is a nonempty poset, so Zorn's lemma yields a maximal element of .
is a proper ideal containing that is maximal among proper ideals of , so is a maximal ideal containing .
Depends on
- Prime ideals and maximal ideals in a commutative ring
- Left, right and two-sided ideals
- Ideal criteria and intersections of ideals
- Zorn's lemma
- The Axiom of Choice
- Chain in a poset
- Maximal element and greatest element
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
Used by
- Agreement on a schematically dense open Corollary
- Global functions on geometrically connected and geometrically reduced proper schemes Corollary
- In a finite-type algebra over a field, radical ideals are intersections of maximal ideals Corollary
- Delta invariant of a curve singularity Definition
- Geometric genus of a singular curve Definition
- Under AC, effective divisors on normal proper curves give finite subschemes of the same degree Example
- A clopen decomposition of the spectrum comes from a nontrivial idempotent Lemma
- A distinguished-open cover of the spectrum forces the covering ideal to be the unit ideal Lemma
- A flat local map is faithfully flat Lemma
- A local domain has a dominating valuation overring Lemma
- A quasi-compact image stable under specialization is closed Lemma
- A quasi-compact immersion with nonclosed image has a boundary specialization Lemma
- A zero-dimensional projective scheme has finitely many closed points with finite-dimensional local rings Lemma
- Affine chart quotients for invariant sections of a linear action Lemma
- Affine-local flatness Lemma
- Affineness is local on the target Lemma
- Closed immersions are affine quotients and survive base change Lemma
- Complex affine algebraic groups are smooth Lemma
- Constructible images for finite-presentation affine maps Lemma
- Every central character of a semisimple enveloping algebra arises from a weight Lemma
- Fibres of the orbit map and the scheme-theoretic stabilizer as a closed subgroup scheme Lemma
- Field-valued points and local-ring points Lemma
- Finite torsion-free modules over Dedekind domains are projective Lemma
- Finite-type field extensions with zero Ω Lemma
- Fpqc covers are universally submersive Lemma
- Fpqc descent of properness components Lemma
- Function field of an integral finite-type scheme Lemma
- Good quotients are local on the target and are categorical quotients Lemma
- Local DVRs at the nonzero primes force dimension one Lemma
- Normality of the Pfaffian rank ring Lemma
- reduced noetherian total fractions and normal components Lemma
- Regularity ascends and descends along a flat local homomorphism Lemma
- Smooth orbits are locally closed and their orbit maps are faithfully flat over every field Lemma
- Smooth projective analytifications have rational Kähler forms Lemma
- Standard smooth algebras are finitely presented and flat Lemma
- Surjectivity survives arbitrary base change Lemma
- The adele quotient V_X/(K + A_X) computes H¹ of the structure sheaf Lemma
- The auxiliary ideal is the unit ideal Lemma
- A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are Theorem
- Assuming Choice, every field has an algebraic extension containing roots of all nonconstant base polynomials Theorem
…and 16 more results.
Dependency tree · two levels
22 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
- Ernst, An Inquiry-Based Approach to Abstract Algebra, Maximal and Prime Ideals (standard reference, not scraped)