isDedekindDomain_iff
theorem isDedekindDomain_iff :
∀ (A : Type u_2) [inst : CommRing A] (K : Type u_4) [inst_1 : Field K] [inst_2 : Algebra A K]
[inst_3 : IsFractionRing A K],
IsDedekindDomain A ↔
IsDomain A ∧
IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
An integral domain `A` is a Dedekind domain if and only if it is Noetherian, has Krull dimension less than or equal to 1, and is integrally closed in a given fraction field `K`. Here, being integrally closed means that for any element `x` in `K` that is integral over `A`, there exists an element `y` in `A` such that `y` maps to `x` under the canonical map from `A` to `K` defined by the algebra structure. This definition is independent of the choice of the fraction field `K`.
More concisely: A commutative ring `A` is a Dedekind domain if and only if it is Noetherian, has Krull dimension ≤ 1, and is integrally closed in its fraction field.
|
isDedekindRing_iff
theorem isDedekindRing_iff :
∀ (A : Type u_2) [inst : CommRing A] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra A K]
[inst_3 : IsFractionRing A K],
IsDedekindRing A ↔
IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
The theorem `isDedekindRing_iff` states that for any integral domain `A` and its field of fractions `K`, `A` is a Dedekind domain if and only if it is Noetherian, has dimension less than or equal to 1, and is integrally closed in `K`. Here, being Noetherian means that all ideals in `A` are finitely generated. The dimension of `A` is the supremum of the lengths of all chains of prime ideals in `A`. An element in `K` is said to be integrally closed in `A` if it is a root of some monic polynomial with coefficients in `A`. The theorem also states that the choice of field of fractions `K` for `A` doesn't impact whether `A` is a Dedekind domain or not.
More concisely: A domain is a Dedekind ring if and only if it is Noetherian, has dimension at most 1, and is integrally closed in its field of fractions.
|
Ideal.IsPrime.isMaximal
theorem Ideal.IsPrime.isMaximal :
∀ {R : Type u_4} [inst : CommRing R] [inst_1 : Ring.DimensionLEOne R] {p : Ideal R},
p.IsPrime → p ≠ ⊥ → p.IsMaximal
This theorem states that for a given type `R` which forms a commutative ring and has dimension less than or equal to one, if `p` is a prime ideal and it is not the bottom element (the smallest ideal, usually `{0}`), then `p` is a maximal ideal. In the language of ring theory, a prime ideal of a commutative, one-dimensional ring that is not the zero ideal is necessarily a maximal ideal.
More concisely: In a one-dimensional commutative ring `R` with unit, a prime ideal `p` different from the bottom ideal is a maximal ideal.
|