Principal ideal rings, principal ideal domains, and Bézout rings #
A principal ideal ring (PIR) is a ring in which all left ideals are principal. A principal ideal domain (PID) is an integral domain which is a principal ideal ring.
The definition of IsPrincipalIdealRing can be found in Mathlib.RingTheory.Ideal.Span.
Main definitions #
Note that for principal ideal domains, one should use
[IsDomain R] [IsPrincipalIdealRing R]. There is no explicit definition of a PID.
Theorems about PID's are in the PrincipalIdealRing namespace.
IsBezout: the predicate saying that every finitely generated left ideal is principal.generator: a generator of a principal ideal (or more generally submodule)to_uniqueFactorizationMonoid: a PID is a unique factorization domain
Main results #
Ideal.IsPrime.to_maximal_ideal: a non-zero prime ideal in a PID is maximal.EuclideanDomain.to_principal_ideal_domain: a Euclidean domain is a PID.IsBezout.nonemptyGCDMonoid: Every Bézout domain is a GCD domain.
instance
bot_isPrincipal
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommGroup M]
[Module R M]
:
⊥.IsPrincipal
@[instance 100]
instance
IsBezout.of_isPrincipalIdealRing
(R : Type u)
[Semiring R]
[IsPrincipalIdealRing R]
:
IsBezout R
@[instance 100]
noncomputable def
Submodule.IsPrincipal.generator
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
M
generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I
Equations
Instances For
theorem
Submodule.IsPrincipal.span_singleton_generator
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
@[simp]
theorem
Ideal.span_singleton_generator
{R : Type u}
[Semiring R]
(I : Ideal R)
[Submodule.IsPrincipal I]
:
@[simp]
theorem
Submodule.IsPrincipal.generator_mem
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
theorem
Submodule.IsPrincipal.mem_iff_eq_smul_generator
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
{x : M}
:
x ∈ S ↔ ∃ (s : R), x = s • Submodule.IsPrincipal.generator S
theorem
Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
(S : Submodule R M)
[S.IsPrincipal]
:
S = ⊥ ↔ Submodule.IsPrincipal.generator S = 0
theorem
Submodule.IsPrincipal.fg
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[Semiring R]
[Module R M]
{S : Submodule R M}
(h : S.IsPrincipal)
:
S.FG
@[instance 100]
@[instance 100]
instance
IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout
{R : Type u}
[Semiring R]
[IsNoetherianRing R]
[IsBezout R]
:
theorem
Submodule.IsPrincipal.associated_generator_span_self
{R : Type u}
[CommRing R]
[IsPrincipalIdealRing R]
[IsDomain R]
(r : R)
:
theorem
Submodule.IsPrincipal.mem_iff_generator_dvd
{R : Type u}
[CommRing R]
(S : Ideal R)
[Submodule.IsPrincipal S]
{x : R}
:
x ∈ S ↔ Submodule.IsPrincipal.generator S ∣ x
theorem
Submodule.IsPrincipal.prime_generator_of_isPrime
{R : Type u}
[CommRing R]
(S : Ideal R)
[Submodule.IsPrincipal S]
[is_prime : S.IsPrime]
(ne_bot : S ≠ ⊥)
:
theorem
Submodule.IsPrincipal.generator_map_dvd_of_mem
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[CommRing R]
[Module R M]
{N : Submodule R M}
(ϕ : M →ₗ[R] R)
[(Submodule.map ϕ N).IsPrincipal]
{x : M}
(hx : x ∈ N)
:
Submodule.IsPrincipal.generator (Submodule.map ϕ N) ∣ ϕ x
theorem
Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem
{R : Type u}
{M : Type v}
[AddCommMonoid M]
[CommRing R]
[Module R M]
{N O : Submodule R M}
(hNO : N ≤ O)
(ϕ : ↥O →ₗ[R] R)
[(ϕ.submoduleImage N).IsPrincipal]
{x : M}
(hx : x ∈ N)
:
Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩
instance
IsBezout.span_pair_isPrincipal
{R : Type u}
[Ring R]
[IsBezout R]
(x y : R)
:
Submodule.IsPrincipal (Ideal.span {x, y})
noncomputable def
IsBezout.gcd
{R : Type u}
[Ring R]
(x y : R)
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
R
A choice of gcd of two elements in a Bézout domain.
Note that the choice is usually not unique.
Equations
- IsBezout.gcd x y = Submodule.IsPrincipal.generator (Ideal.span {x, y})
Instances For
theorem
IsBezout.span_gcd
{R : Type u}
[Ring R]
(x y : R)
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}
theorem
IsBezout.gcd_dvd_left
{R : Type u}
[CommRing R]
(x y : R)
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
IsBezout.gcd x y ∣ x
theorem
IsBezout.gcd_dvd_right
{R : Type u}
[CommRing R]
(x y : R)
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
IsBezout.gcd x y ∣ y
theorem
IsBezout.dvd_gcd
{R : Type u}
[CommRing R]
{x y z : R}
[Submodule.IsPrincipal (Ideal.span {x, y})]
(hx : z ∣ x)
(hy : z ∣ y)
:
z ∣ IsBezout.gcd x y
theorem
IsBezout.gcd_eq_sum
{R : Type u}
[CommRing R]
(x y : R)
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
∃ (a : R) (b : R), a * x + b * y = IsBezout.gcd x y
theorem
IsRelPrime.isCoprime
{R : Type u}
[CommRing R]
{x y : R}
[Submodule.IsPrincipal (Ideal.span {x, y})]
(h : IsRelPrime x y)
:
IsCoprime x y
theorem
isRelPrime_iff_isCoprime
{R : Type u}
[CommRing R]
{x y : R}
[Submodule.IsPrincipal (Ideal.span {x, y})]
:
IsRelPrime x y ↔ IsCoprime x y
noncomputable def
IsBezout.toGCDDomain
(R : Type u)
[CommRing R]
[IsBezout R]
[IsDomain R]
[DecidableEq R]
:
Any Bézout domain is a GCD domain. This is not an instance since GCDMonoid contains data,
and this might not be how we would like to construct it.
Equations
- IsBezout.toGCDDomain R = gcdMonoidOfGCD (fun (x1 x2 : R) => IsBezout.gcd x1 x2) ⋯ ⋯ ⋯
Instances For
theorem
IsBezout.associated_gcd_gcd
(R : Type u)
[CommRing R]
{x y : R}
[Submodule.IsPrincipal (Ideal.span {x, y})]
[IsDomain R]
[GCDMonoid R]
:
Associated (IsBezout.gcd x y) (gcd x y)
theorem
IsPrime.to_maximal_ideal
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
{S : Ideal R}
[hpi : S.IsPrime]
(hS : S ≠ ⊥)
:
S.IsMaximal
@[instance 100]
theorem
PrincipalIdealRing.isMaximal_of_irreducible
{R : Type u}
[CommRing R]
[IsPrincipalIdealRing R]
{p : R}
(hp : Irreducible p)
:
Ideal.IsMaximal (Submodule.span R {p})
@[deprecated irreducible_iff_prime]
theorem
PrincipalIdealRing.irreducible_iff_prime
{M : Type u_1}
[CancelCommMonoidWithZero M]
[DecompositionMonoid M]
{a : M}
:
Irreducible a ↔ Prime a
Alias of irreducible_iff_prime.
@[deprecated associates_irreducible_iff_prime]
theorem
PrincipalIdealRing.associates_irreducible_iff_prime
{M : Type u_1}
[CancelCommMonoidWithZero M]
[DecompositionMonoid M]
{p : Associates M}
:
Irreducible p ↔ Prime p
Alias of associates_irreducible_iff_prime.
noncomputable def
PrincipalIdealRing.factors
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
(a : R)
:
Multiset R
factors a is a multiset of irreducible elements whose product is a, up to units
Equations
- PrincipalIdealRing.factors a = if h : a = 0 then ∅ else Classical.choose ⋯
Instances For
theorem
PrincipalIdealRing.factors_spec
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
(a : R)
(h : a ≠ 0)
:
(∀ b ∈ PrincipalIdealRing.factors a, Irreducible b) ∧ Associated (PrincipalIdealRing.factors a).prod a
theorem
PrincipalIdealRing.ne_zero_of_mem_factors
{R : Type v}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
{a b : R}
(ha : a ≠ 0)
(hb : b ∈ PrincipalIdealRing.factors a)
:
b ≠ 0
theorem
PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
(s : Submonoid R)
{a : R}
(ha : a ≠ 0)
(hfac : ∀ b ∈ PrincipalIdealRing.factors a, b ∈ s)
(hunit : ∀ (c : Rˣ), ↑c ∈ s)
:
a ∈ s
theorem
PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
[Semiring S]
(f : R →+* S)
(s : Submonoid S)
(a : R)
(ha : a ≠ 0)
(h : ∀ b ∈ PrincipalIdealRing.factors a, f b ∈ s)
(hf : ∀ (c : Rˣ), f ↑c ∈ s)
:
f a ∈ s
If a RingHom maps all units and all factors of an element a into a submonoid s, then it
also maps a into that submonoid.
@[instance 100]
instance
PrincipalIdealRing.to_uniqueFactorizationMonoid
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
:
A principal ideal domain has unique factorization
theorem
Submodule.IsPrincipal.map
{R : Type u}
{M : Type v}
{N : Type u_2}
[Ring R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(f : M →ₗ[R] N)
{S : Submodule R M}
(hI : S.IsPrincipal)
:
(Submodule.map f S).IsPrincipal
theorem
Submodule.IsPrincipal.of_comap
{R : Type u}
{M : Type v}
{N : Type u_2}
[Ring R]
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(f : M →ₗ[R] N)
(hf : Function.Surjective ⇑f)
(S : Submodule R N)
[hI : (Submodule.comap f S).IsPrincipal]
:
S.IsPrincipal
theorem
Submodule.IsPrincipal.map_ringHom
{R : Type u}
{S : Type u_1}
{F : Type u_3}
[Ring R]
[Ring S]
[FunLike F R S]
[RingHomClass F R S]
(f : F)
{I : Ideal R}
(hI : Submodule.IsPrincipal I)
:
theorem
Ideal.IsPrincipal.of_comap
{R : Type u}
{S : Type u_1}
{F : Type u_3}
[Ring R]
[Ring S]
[FunLike F R S]
[RingHomClass F R S]
(f : F)
(hf : Function.Surjective ⇑f)
(I : Ideal S)
[hI : Submodule.IsPrincipal (Ideal.comap f I)]
:
theorem
IsPrincipalIdealRing.of_surjective
{R : Type u}
{S : Type u_1}
{F : Type u_3}
[Ring R]
[Ring S]
[FunLike F R S]
[RingHomClass F R S]
[IsPrincipalIdealRing R]
(f : F)
(hf : Function.Surjective ⇑f)
:
The surjective image of a principal ideal ring is again a principal ideal ring.
theorem
Irreducible.coprime_iff_not_dvd
{R : Type u}
[CommRing R]
[IsBezout R]
{p n : R}
(hp : Irreducible p)
:
See also Irreducible.isRelPrime_iff_not_dvd.
theorem
Irreducible.dvd_iff_not_coprime
{R : Type u}
[CommRing R]
[IsBezout R]
{p n : R}
(hp : Irreducible p)
:
See also Irreducible.coprime_iff_not_dvd'.
theorem
Irreducible.coprime_or_dvd
{R : Type u}
[CommRing R]
[IsBezout R]
{p : R}
(hp : Irreducible p)
(i : R)
:
theorem
IsBezout.span_gcd_eq_span_gcd
{R : Type u}
[CommRing R]
[IsBezout R]
[IsDomain R]
[GCDMonoid R]
(x y : R)
:
Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}
theorem
exists_associated_pow_of_associated_pow_mul
{R : Type u}
[CommRing R]
[IsBezout R]
[IsDomain R]
{a b c : R}
(hab : IsCoprime a b)
{k : ℕ}
(h : Associated (c ^ k) (a * b))
:
∃ (d : R), Associated (d ^ k) a
theorem
isCoprime_of_irreducible_dvd
{R : Type u}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
{x y : R}
(nonzero : ¬(x = 0 ∧ y = 0))
(H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y)
:
IsCoprime x y
nonPrincipals R is the set of all ideals of R that are not principal ideals.
Equations
- nonPrincipals R = {I : Ideal R | ¬Submodule.IsPrincipal I}
Instances For
theorem
nonPrincipals_zorn
{R : Type u}
[CommRing R]
(c : Set (Ideal R))
(hs : c ⊆ nonPrincipals R)
(hchain : IsChain (fun (x1 x2 : Ideal R) => x1 ≤ x2) c)
{K : Ideal R}
(hKmem : K ∈ c)
:
∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
Any chain in the set of non-principal ideals has an upper bound which is non-principal. (Namely, the union of the chain is such an upper bound.)