Documentation

Mathlib.RingTheory.PrincipalIdealDomain

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.

Main results #

instance bot_isPrincipal {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] :
class IsBezout (R : Type u) [Semiring R] :

A Bézout ring is a ring whose finitely generated ideals are principal.

Instances
    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
    @[simp]
    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 generator S
    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
    theorem Submodule.IsPrincipal.prime_generator_of_isPrime {R : Type u} [CommRing R] (S : Ideal R) [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) :
    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) :
    generator (ϕ.submoduleImage N) ϕ x,
    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
    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 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 = gcd 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
    theorem IsPrime.to_maximal_ideal {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : S.IsPrime] (hS : S ) :
    theorem mod_mem_iff {R : Type u} [EuclideanDomain R] {S : Ideal R} {x y : R} (hy : y S) :
    x % y S x S
    noncomputable def PrincipalIdealRing.factors {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (a : R) :

    factors a is a multiset of irreducible elements whose product is a, up to units

    Equations
    theorem PrincipalIdealRing.ne_zero_of_mem_factors {R : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} (ha : a 0) (hb : b 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 : bfactors 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 : bfactors 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]

    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) :
    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 : (comap f 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 : 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 (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 isCoprime_of_dvd {R : Type u} [CommRing R] [IsBezout R] (x y : R) (nonzero : ¬(x = 0 y = 0)) (H : znonunits R, z 0z x¬z y) :
    theorem dvd_or_isCoprime {R : Type u} [CommRing R] [IsBezout R] (x y : R) (h : Irreducible x) :
    x y IsCoprime x y
    @[deprecated dvd_or_isCoprime (since := "2025-01-23")]
    theorem dvd_or_coprime {R : Type u} [CommRing R] [IsBezout R] (x y : R) (h : Irreducible x) :
    x y IsCoprime x y

    Alias of dvd_or_isCoprime.

    theorem Irreducible.dvd_iff_not_isCoprime {R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) :

    See also Irreducible.coprime_iff_not_dvd'.

    @[deprecated Irreducible.dvd_iff_not_isCoprime (since := "2025-01-23")]
    theorem Irreducible.dvd_iff_not_coprime {R : Type u} [CommRing R] [IsBezout R] {p n : R} (hp : Irreducible p) :

    Alias of Irreducible.dvd_iff_not_isCoprime.


    See also Irreducible.coprime_iff_not_dvd'.

    theorem Irreducible.coprime_pow_of_not_dvd {R : Type u} [CommRing R] [IsBezout R] {p a : R} (m : ) (hp : Irreducible p) (h : ¬p a) :
    IsCoprime a (p ^ m)
    theorem Irreducible.isCoprime_or_dvd {R : Type u} [CommRing R] [IsBezout R] {p : R} (hp : Irreducible p) (i : R) :
    IsCoprime p i p i
    @[deprecated Irreducible.isCoprime_or_dvd (since := "2025-01-23")]
    theorem Irreducible.coprime_or_dvd {R : Type u} [CommRing R] [IsBezout R] {p : R} (hp : Irreducible p) (i : R) :
    IsCoprime p i p i

    Alias of Irreducible.isCoprime_or_dvd.

    theorem span_gcd {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (x y : R) :
    theorem gcd_dvd_iff_exists {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (a b : R) {z : R} :
    gcd a b z ∃ (x : R) (y : R), z = a * x + b * y
    theorem exists_gcd_eq_mul_add_mul {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (a b : R) :
    ∃ (x : R) (y : R), gcd a b = a * x + b * y

    Bézout's lemma

    theorem gcd_isUnit_iff {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R] (x y : R) :
    theorem Prime.coprime_iff_not_dvd {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {p n : R} (hp : Prime p) :
    theorem exists_associated_pow_of_mul_eq_pow' {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] {a b c : R} (hab : IsCoprime a b) {k : } (h : a * b = c ^ k) :
    ∃ (d : R), Associated (d ^ k) a
    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 zz x¬z y) :
    theorem isCoprime_of_prime_dvd {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : R), Prime zz x¬z y) :
    def nonPrincipals (R : Type u) [CommRing R] :

    nonPrincipals R is the set of all ideals of R that are not principal ideals.

    Equations
    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) :
    InonPrincipals R, Jc, 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.)