IsLocalization.AtPrime.isDedekindDomain
theorem IsLocalization.AtPrime.isDedekindDomain :
∀ (A : Type u_2) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDedekindDomain A] (P : Ideal A)
[inst_3 : P.IsPrime] (Aₘ : Type u_4) [inst_4 : CommRing Aₘ] [inst_5 : IsDomain Aₘ] [inst_6 : Algebra A Aₘ]
[inst : IsLocalization.AtPrime Aₘ P], IsDedekindDomain Aₘ
The theorem `IsLocalization.AtPrime.isDedekindDomain` asserts that for any Dedekind domain `A` and any nonzero prime ideal `P` of `A`, the localization of `A` at `P` is also a Dedekind domain. Here, localization is realized as a type `Aₘ` that is a commutative ring, a domain, and an algebra over `A`, and is isomorphic to `A` localized at the complement of `P`. In other words, the process of localization preserves the property of being a Dedekind domain, when applied to a Dedekind domain and a nonzero prime ideal.
More concisely: If `A` is a Dedekind domain and `P` is a nonzero prime ideal in `A`, then the localization of `A` at `P` is also a Dedekind domain.
|
IsDedekindDomain.isDedekindDomainDvr
theorem IsDedekindDomain.isDedekindDomainDvr :
∀ (A : Type u_2) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDedekindDomain A], IsDedekindDomainDvr A
This theorem states that for any type `A` that is a commutative ring and a domain, if `A` is a Dedekind domain in the sense of being a Noetherian integrally closed domain of Krull dimension less than or equal to 1, then `A` is also a Dedekind domain in the sense that the localization at every nonzero prime ideal is a discrete valuation ring (DVR).
More concisely: If `A` is a Noetherian integrally closed commutative domain of Krull dimension ≤ 1 that is also a domain, then `A` is a Dedekind domain if and only if every localization at a nonzero prime ideal is a discrete valuation ring.
|
IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain
theorem IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain :
∀ (A : Type u_2) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDedekindDomain A] {P : Ideal A},
P ≠ ⊥ →
∀ [pP : P.IsPrime] (Aₘ : Type u_4) [inst_3 : CommRing Aₘ] [inst_4 : IsDomain Aₘ] [inst_5 : Algebra A Aₘ]
[inst : IsLocalization.AtPrime Aₘ P], DiscreteValuationRing Aₘ
The theorem `IsLocalization.AtPrime.discreteValuationRing_of_dedekind_domain` states that in a Dedekind domain, the localization at every nonzero prime ideal is a Discrete Valuation Ring (DVR). Specifically, for any given commutative ring `A` that is also a domain and a Dedekind domain, and for any nonzero prime ideal `P` of `A`, if `Aₘ` is another commutative ring that is also a domain and is the localization of `A` at the complement of `P`, then `Aₘ` is a Discrete Valuation Ring.
More concisely: In a Dedekind domain, the localization at any nonzero prime ideal is a Discrete Valuation Ring.
|
Ring.DimensionLEOne.localization
theorem Ring.DimensionLEOne.localization :
∀ {R : Type u_4} (Rₘ : Type u_5) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing Rₘ]
[inst_3 : Algebra R Rₘ] {M : Submonoid R} [inst_4 : IsLocalization M Rₘ],
M ≤ nonZeroDivisors R → ∀ [h : Ring.DimensionLEOne R], Ring.DimensionLEOne Rₘ
This theorem states that the process of localizing a ring, specifically a domain (`IsDomain R`), with Krull dimension less than or equal to 1 (`Ring.DimensionLEOne R`), results in another ring (`Rₘ`) that also has Krull dimension less than or equal to 1 (`Ring.DimensionLEOne Rₘ`). The theorem further asserts that this is valid when the localization is done at a submonoid (`M`) of the ring that is contained within the submonoid of non-zero divisors of the ring (`M ≤ nonZeroDivisors R`). The theorem suggests that a similar argument could be used to show that localization preserves any Krull dimension, once a suitable definition for this is available.
More concisely: If `R` is a domain of Krull dimension less than or equal to 1 in Lean 4, then localizing `R` at a submonoid contained within its submonoid of non-zero divisors results in another domain `Rₘ` of Krull dimension less than or equal to 1.
|
IsLocalization.isDedekindDomain
theorem IsLocalization.isDedekindDomain :
∀ (A : Type u_2) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDedekindDomain A] {M : Submonoid A},
M ≤ nonZeroDivisors A →
∀ (Aₘ : Type u_4) [inst_3 : CommRing Aₘ] [inst_4 : IsDomain Aₘ] [inst_5 : Algebra A Aₘ]
[inst : IsLocalization M Aₘ], IsDedekindDomain Aₘ
The theorem `IsLocalization.isDedekindDomain` states that for any Dedekind domain `A` (a commutative ring with no zero divisors that satisfies certain other properties), if we define a submonoid `M` of `A` such that `M` is a subset of the non-zero divisors of `A`, then the localization of `A` at `M`, denoted `Aₘ`, is also a Dedekind domain. This property holds for any type `Aₘ` that is a commutative ring, has no zero divisors, and is an algebra over `A` such that it is a localization of `A` at `M`.
More concisely: If `A` is a commutative Dedekind domain and `M` is a subset of its non-zero divisors, then the localization `Aₘ` of `A` at `M` is also a Dedekind domain.
|