Revision #2383 → #3070 · back to history
modifiedMaximal spectrumcfba04652b37
| Field | From #2383 | To #3070 |
|---|
| note | `MaximalSpectrum R` is the type of maximal ideals of a commutative ring `R`. | `MaximalSpectrum R` is the structure type of maximal ideals of a commutative (semi)ring `R`. |
modifiedMaximal one-sided idealsd04bc61484bc
| Field | From #2383 | To #3070 |
|---|
| note | Mathlib's `Ideal` models left ideals (with two-sided in commutative case); right ideals are not a separate first-class concept, so maximal right ideals are not separately formalized. | Mathlib's `Ideal` models left ideals (with two-sided in the commutative case); maximal right ideals are not separately formalized. |
modifiedLocal ring via unique maximal right idealc1c41a9daf03
| Field | From #2383 | To #3070 |
|---|
| note | `IsLocalRing` is defined via the `a+b=1 → IsUnit a ∨ IsUnit b` condition; equivalence with a unique maximal ideal is `IsLocalRing.maximal_ideal_unique`, but only for (commutative-style) two-sided ideals. | `IsLocalRing.maximal_ideal_unique` characterises local rings as those with a unique maximal ideal, but the right-ideal version is not separately formalised. |
modified2x2 matrices: unique two-sided but many one-sided maximale8bcf9562912
| Field | From #2383 | To #3070 |
|---|
| note | No specific Mathlib statement about maximal ideals of `Matrix (Fin 2) (Fin 2) K` was found. | No specific Mathlib statement about the maximal ideals of `Matrix (Fin 2) (Fin 2) K` was found. |
modifiedEquivalent conditions for maximal two-sided ideale803a10ea827
| Field | From #2383 | To #3070 |
|---|
| note | `Ideal.isMaximal_iff` gives one characterization (proper + every strictly larger ideal contains 1); the full list of equivalences from the article is not packaged as one decl. | `Ideal.isMaximal_iff` gives one characterisation (proper + every strictly larger ideal contains 1); the full list of equivalences is not packaged as a single decl. |
modifiedEquivalent conditions for maximal right ideal03c5fc58c80d
| Field | From #2383 | To #3070 |
|---|
| note | Mathlib lacks a dedicated right-ideal API, so this list of equivalences is not formalized. | Mathlib lacks a dedicated right-ideal API, so this list of equivalences is not formalised. |
modifiedField has only {0} as maximal ideal7ae486c36fd9
| Field | From #2383 | To #3070 |
|---|
| note | `Ideal.bot_isMaximal` proves `⊥` is maximal in a division (semi)ring, which together with `eq_bot_or_top` for ideals of a field captures the example. | `Ideal.bot_isMaximal` proves `⊥` is maximal in a division ring, capturing the example. |
modifiedNonzero primes maximal in PID5a222d23e00f
| Field | From #2383 | To #3070 |
|---|
| note | `PrincipalIdealRing.isMaximal_of_irreducible` together with `Ideal.IsPrime.isMaximal` (under `DimensionLEOne`) gives the result; PIDs are zero/one-dimensional so nonzero primes are maximal. | `PrincipalIdealRing.isMaximal_of_irreducible` gives that the ideal generated by an irreducible element of a PID is maximal, matching nonzero primes. |
modifiedMaximal ideals of Z[x]dd6e28b6be45
| Field | From #2383 | To #3070 |
|---|
| note | No explicit Mathlib characterization of the maximal ideals of `ℤ[X]` was found. | No explicit Mathlib characterisation of the maximal ideals of `ℤ[X]` was found. |
modifiedBoolean ring: every prime is maximalb338269ee5f3
| Field | From #2383 | To #3070 |
|---|
| note | Mathlib's `BooleanRing` file has no theorem identifying prime and maximal ideals. | Mathlib's `BooleanRing` file has no theorem identifying prime and maximal ideals in a Boolean ring. |
modifiedMaximal ideals of k[x]403c05bd9b5a
| Field | From #2383 | To #3070 |
|---|
| note | `PrincipalIdealRing.isMaximal_of_irreducible` applied to `k[X]` (which is a PID over a field) gives that ideals generated by irreducible polynomials are maximal. | `PrincipalIdealRing.isMaximal_of_irreducible` applied to `k[X]` (a PID over a field) yields that ideals generated by irreducible polynomials are maximal. |
modifiedWeak Nullstellensatz2aa90673994f
| Field | From #2383 | To #3070 |
|---|
| note | `MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton` characterizes maximal ideals of `k[x₁,…,xₙ]` over an algebraically closed field as vanishing ideals of points. | `MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton` characterises maximal ideals of `k[x₁,…,xₙ]` over an algebraically closed field as vanishing ideals of singletons. |
modifiedMaximal ideals of coordinate ringa2f438c882bc
| Field | From #2383 | To #3070 |
|---|
| note | No direct Mathlib statement was found describing maximal ideals of the coordinate ring of an affine variety. | No direct Mathlib statement describing the maximal ideals of the coordinate ring of an affine variety was found. |
modifiedRadical ring has no maximal one-sided idealse375bd7fe9f4
| Field | From #2383 | To #3070 |
|---|
| note | No Mathlib decl about radical rings (Jacobson radical = whole ring) and absence of one-sided maximal ideals was found. | No Mathlib decl about radical rings (Jacobson radical = whole ring) and the absence of maximal one-sided ideals was found. |
modifiedMaximal implies prime in commutative ring91f0199648b5
| Field | From #2383 | To #3070 |
|---|
| note | `Ideal.IsMaximal.isPrime` (with an `instance IsMaximal.isPrime'`) gives that maximal ideals of a commutative (semi)ring are prime. | `Ideal.IsMaximal.isPrime` (with `instance IsMaximal.isPrime'`) gives that maximal ideals of a commutative (semi)ring are prime. |
modifiedZero-dimensional ring8d63d6fbc5a6
| Field | From #2383 | To #3070 |
|---|
| note | `Ring.KrullDimLE 0 R` expresses that the Krull dimension of `R` is at most zero, i.e., every prime ideal is maximal. | `Ring.KrullDimLE 0 R` expresses that the Krull dimension of `R` is at most zero, characterised by `Ring.krullDimLE_zero_iff` as every prime ideal being maximal. |
modifiedPreimage under k-algebra homomorphism6e58fb77afc9
| Field | From #2383 | To #3070 |
|---|
| note | Mathlib has the Jacobson-ring machinery (`Polynomial.isMaximal_comap_C_of_isJacobsonRing`, `MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing`) from which this preimage statement follows, but no direct lemma `(comap of maximal under finitely generated k-algebra hom is maximal)`. | Mathlib has the Jacobson-ring machinery (`Polynomial.isMaximal_comap_C_of_isJacobsonRing`, `MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing`) from which this preimage statement follows, but no packaged 'comap of maximal under finitely generated k-algebra hom is maximal' lemma. |
modifiedMaximal submodule977ba3888834
| Field | From #2383 | To #3070 |
|---|
| note | Mathlib expresses 'maximal submodule' as `IsCoatom (N : Submodule R M)` using the general order-theoretic `IsCoatom`; there is no dedicated `Submodule.IsMaximal`. | Mathlib expresses 'maximal submodule' via the general order-theoretic `IsCoatom (N : Submodule R M)`; there is no dedicated `Submodule.IsMaximal`. |
modifiedMaximal right ideals = maximal submodules of R_R0c276dab7e4d
| Field | From #2383 | To #3070 |
|---|
| note | `Ideal.isMaximal_def` (`I.IsMaximal ↔ IsCoatom I`) gives this identification for left ideals (Mathlib's `Ideal R = Submodule R R`); the right-ideal version is not separately formalized. | `Ideal.isMaximal_def` (`I.IsMaximal ↔ IsCoatom I`) gives this identification for left ideals (`Ideal R = Submodule R R`); the right-ideal version is not separately formalised. |
modifiedExistence of maximal submodulesc79ba34835c6
| Field | From #2383 | To #3070 |
|---|
| mathlib.decl | Module.Finite.instIsCoatomicSubmodule | Submodule.instIsCoatomicOfFinite |
| note | `Module.Finite.instIsCoatomicSubmodule` gives `IsCoatomic (Submodule R M)` for finitely generated `M`; the projective-module case is not formalized. | An unnamed instance in `Mathlib.RingTheory.Finiteness.Basic` supplies `IsCoatomic (Submodule R M)` for `[Module.Finite R M]`; the projective-module case is not formalised. |
modifiedJacobson radical via maximal ideals0c9ba1b09ab1
| Field | From #2383 | To #3070 |
|---|
| note | `Ideal.jacobson` formalizes the Jacobson radical as the intersection of all maximal ideals above a given ideal; `Ring.jacobson` (in `Mathlib.RingTheory.Jacobson.Radical`) gives the radical of the ring itself. | `Ideal.jacobson` formalises the Jacobson radical as the infimum of all maximal ideals containing the given ideal; `Ring.jacobson` in `Mathlib.RingTheory.Jacobson.Radical` specialises this to the whole ring. |
modifiedEvery nonzero finitely generated module has a maximal submodule398af5db4653
| Field | From #2383 | To #3070 |
|---|
| mathlib.decl | Module.Finite.instIsCoatomicSubmodule | Submodule.instIsCoatomicOfFinite |
| note | The `IsCoatomic (Submodule R M)` instance for finitely generated `M` combined with `IsCoatomic.eq_top_or_exists_le_coatom` yields the existence of a maximal submodule (`IsCoatom`) above any proper submodule. | The `IsCoatomic (Submodule R M)` instance for `[Module.Finite R M]` combined with `IsCoatomic.eq_top_or_exists_le_coatom` yields the existence of a maximal submodule above any proper submodule. |
addedPrime spectrum584ad0ddae6d
addedSimple module (quotient by maximal one-sided ideal)785d4474ba95
addedSimple ringf2fa950a070d