IsDedekindDomain.isPrincipalIdealRing_localization_over_prime
theorem IsDedekindDomain.isPrincipalIdealRing_localization_over_prime :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Type u_2) [inst_2 : CommRing S]
[inst_3 : Algebra R S] [inst_4 : Module.Free R S] [inst_5 : Module.Finite R S] (p : Ideal R),
p ≠ ⊥ →
∀ [inst_6 : p.IsPrime] {Sₚ : Type u_3} [inst_7 : CommRing Sₚ] [inst_8 : Algebra S Sₚ]
[inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_10 : Algebra R Sₚ]
[inst : IsScalarTower R S Sₚ] [inst : IsDedekindDomain Sₚ] [inst : IsDomain S], IsPrincipalIdealRing Sₚ
This theorem states that if we have a Dedekind domain `R` and an integral extension `S` of `R`, and `p` is a prime ideal in `R` which is not the zero ideal, then the localization `Sₚ` of `S` at `p` is a Principal Ideal Domain (PID). Here, `Sₚ` is a type that forms a commutative ring, has an algebra structure over `S` and `R`, is a scalar tower over `R` and `S`, is a Dedekind domain, and is a domain. Furthermore, `Sₚ` is a localization of `S` at the complement of the prime ideal `p` in `R`.
More concisely: If `R` is a Dedekind domain and `S` is an integral extension of `R`, then the localization `S_p` of `S` at a non-zero prime ideal `p` in `R` is a Principal Ideal Domain.
|
IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime
theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Type u_2) [inst_2 : CommRing S]
[inst_3 : Algebra R S] [inst_4 : Module.Free R S] [inst_5 : Module.Finite R S] (p : Ideal R),
p ≠ ⊥ →
∀ [inst_6 : p.IsPrime] {Sₚ : Type u_3} [inst_7 : CommRing Sₚ] [inst_8 : Algebra S Sₚ]
[inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_10 : Algebra R Sₚ]
[inst_11 : IsScalarTower R S Sₚ] [inst_12 : IsDedekindDomain Sₚ] [inst_13 : IsDomain S] {P : Ideal Sₚ},
P.IsPrime → P ≠ ⊥ → P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
This theorem states that if `p` is a prime ideal in a Dedekind domain `R`, `S` is a ring extension of `R`, and `Sₚ` is the localization of `S` at `p`, then any prime ideal `P` in `Sₚ` is a factor of the image of `p` under the ring homomorphism from `R` to `Sₚ`. More specifically, `P` is a member of the multiset of normalized factors of the image of `p`. This means that in the localized ring `Sₚ`, every prime ideal comes from a prime ideal in the original ring `R`, through the ring extension and localization process.
More concisely: Given a Dedekind domain `R`, a prime ideal `p` in `R`, a ring extension `S` of `R`, and the localization `Sₚ` of `S` at `p`, every prime ideal `P` in `Sₚ` is contained in the multiset of normalized factors of the ideal image of `p` under the ring homomorphism from `R` to `Sₚ`.
|
Ideal.IsPrincipal.of_finite_maximals_of_isUnit
theorem Ideal.IsPrincipal.of_finite_maximals_of_isUnit :
∀ {R : Type u_1} [inst : CommRing R],
{I | I.IsMaximal}.Finite → ∀ {I : Ideal R}, IsUnit ↑I → Submodule.IsPrincipal I
This theorem states that for any commutative ring `R` with a finite set of maximal ideals, any invertible ideal `I` in `R` is principal. In other words, if we have a commutative ring and the number of its maximal ideals is finite, then any ideal in that ring which has an inverse (i.e., it is a unit) can be generated by a single element.
More concisely: In a commutative ring with finite numbers of maximal ideas, any invertible ideal is principal.
|
IsPrincipalIdealRing.of_finite_primes
theorem IsPrincipalIdealRing.of_finite_primes :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R],
{I | I.IsPrime}.Finite → IsPrincipalIdealRing R
This theorem states that if a Dedekind domain, which is a commutative ring, has a finite set of prime ideals, then it is a Principal Ideal Ring. In other words, every ideal in such a ring can be generated by a single element. This theorem applies to any type `R` with the structure of a commutative ring that is also a Dedekind domain.
More concisely: If a Dedekind domain, as a commutative ring, has finitely many prime ideals, then it is a principal ideal domain.
|
FractionalIdeal.isPrincipal.of_finite_maximals_of_inv
theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv :
∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Submonoid R}
[inst_3 : IsLocalization S A],
S ≤ nonZeroDivisors R →
{I | I.IsMaximal}.Finite → ∀ (I I' : FractionalIdeal S A), I * I' = 1 → (↑I).IsPrincipal
This theorem states that given a commutative ring `R` with finitely many maximal ideals, and a fractional ideal `I` of `R` that is invertible (that is, there exists another fractional ideal `I'` such that the product of `I` and `I'` equals the identity), then `I` is a principal ideal. The statement also requires that the submonoid `S` of `R` is a subset of the non-zero divisors of `R`. This property is significant in the context of ring localization, which is a process that introduces more fractions into a ring. The theorem specifically refers to the localization `A` of `R` at the submonoid `S`. The link provided in the comment is a reference to a math.stackexchange post which presumably provides a proof or more context for the theorem.
More concisely: Given a commutative ring `R` with finitely many maximal ideals and a invertible fractional ideal `I` whose generator set is contained in the non-zero divisors of `R`, then `I` is a principal ideal in the localization of `R` at the submonoid of non-zero divisors.
|
Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne
theorem Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne :
∀ {R : Type u_1} [inst : CommRing R] {P : Ideal R},
P.IsPrime →
∀ [inst_1 : IsDedekindDomain R] {x : R},
x ∈ P → x ∉ P ^ 2 → (∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q) → P = Ideal.span {x}
This theorem states that in a commutative ring `R` that is a Dedekind domain, if `P` is a prime ideal, `x` is an element of `P` but not in the square of `P`, and `x` is not in any other prime ideal `Q` that is not equivalent to `P`, then the ideal `P` is generated by the single element `x`. In other words, `P` is the ideal spanned by `{x}`.
More concisely: In a commutative Dedekind domain `R`, if `x` is an element that lies in a prime ideal `P` but not in `P^2` nor any other non-equivalent prime ideal, then `P` is generated by `x`.
|