tfae_of_isNoetherianRing_of_localRing_of_isDomain
theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain :
∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : LocalRing R] [inst_3 : IsDomain R],
[IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = LocalRing.maximalIdeal R,
Submodule.IsPrincipal (LocalRing.maximalIdeal R),
FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) ≤ 1,
∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = LocalRing.maximalIdeal R ^ n].TFAE
The theorem states that for a noetherian local domain `R` (which could also be a field), the following conditions are equivalent:
0. `R` is a Principal Ideal Domain (PID).
1. `R` is a valuation ring.
2. `R` is a Dedekind domain.
3. `R` is integrally closed and has at most one non-zero prime ideal.
4. The maximal ideal `m` of `R` is principal.
5. The dimension of the quotient of `m` by `m` squared, when viewed as a vector space over the residue field `k`, is less than or equal to 1.
6. Every nonzero ideal in `R` is a power of `m`.
This theorem thus provides a number of characterizations of the structure of a Noetherian local domain. It is also mentioned that there is a version of this theorem for Discrete Valuation Rings that do not assume `R` to be a field.
More concisely: In a Noetherian local domain, being a Principal Ideal Domain (PID), a valuation ring, a Dedekind domain, integrally closed with at most one non-zero prime ideal, having a principal maximal ideal, and having the property that the maximal ideal's quotient by its square has dimension less than or equal to 1 are all equivalent conditions.
|
DiscreteValuationRing.TFAE
theorem DiscreteValuationRing.TFAE :
∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : LocalRing R] [inst_3 : IsDomain R],
¬IsField R →
[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
Submodule.IsPrincipal (LocalRing.maximalIdeal R),
FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1,
∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = LocalRing.maximalIdeal R ^ n].TFAE
The theorem states that for a Noetherian local domain `R` that is not a field, the following properties are equivalent:
0. `R` is a discrete valuation ring.
1. `R` is a valuation ring.
2. `R` is a Dedekind domain.
3. `R` is integrally closed and there exists a unique non-zero prime ideal in `R`.
4. The maximal ideal `m` of `R` is principal (i.e., it is generated by a single element).
5. The dimension of the cotangent space `m/m²` over the residue field `k` is 1.
6. Every non-zero ideal in `R` is a power of the maximal ideal `m`.
In other words, if `R` is a Noetherian local domain that is not a field, then any one of the above properties implies all the others.
More concisely: For a Noetherian local domain `R` that is not a field, the properties of being a discrete valuation ring, a valuation ring, a Dedekind domain, integrally closed with a unique non-zero prime ideal, having a principal maximal ideal, and having a cotangent space of dimension 1 over the residue field, are equivalent.
|