Principal ideal rings and principal ideal domains #

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.

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 principal_ideal_ring namespace.

Main results #

theorem Submodule.IsPrincipal_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) :
class Submodule.IsPrincipal {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) :

An R-submodule of M is principal if it is generated by one element.

    theorem Submodule.IsPrincipal.principal {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] :
    a, S = Submodule.span R {a}
    class IsPrincipalIdealRing (R : Type u) [Ring R] :

    A ring is a principal ideal ring if all (left) ideals are principal.

      noncomputable def Submodule.IsPrincipal.generator {R : Type u} {M : Type v} [AddCommGroup M] [Ring R] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] :

      generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I

      Instances For
        theorem Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem {R : Type u} {M : Type v} [AddCommGroup M] [CommRing R] [Module R M] {N : Submodule R M} {O : Submodule R M} (hNO : N O) (ϕ : { x // x O } →ₗ[R] R) [Submodule.IsPrincipal (LinearMap.submoduleImage ϕ N)] {x : M} (hx : x N) :
        Submodule.IsPrincipal.generator (LinearMap.submoduleImage ϕ N) ϕ { val := x, property := hNO x hx }
        theorem mod_mem_iff {R : Type u} [EuclideanDomain R] {S : Ideal R} {x : R} {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

        Instances For
          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 : R), b PrincipalIdealRing.factors ab 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 : R), b PrincipalIdealRing.factors af 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.

          A principal ideal domain has unique factorization

          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.IsPrincipal (Submodule.comap f S)] :
          theorem Ideal.IsPrincipal.of_comap {R : Type u} {S : Type u_1} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective f) (I : Ideal S) [hI : Submodule.IsPrincipal (Ideal.comap f I)] :

          The surjective image of a principal ideal ring is again a principal ideal ring.

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

          Bézout's lemma

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

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

          Instances For
            theorem nonPrincipals_zorn {R : Type u} [CommRing R] (c : Set (Ideal R)) (hs : c nonPrincipals R) (hchain : IsChain (fun x x_1 => x x_1) c) {K : Ideal R} (hKmem : K c) :
            I, I nonPrincipals R ∀ (J : Ideal R), J cJ 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.)

            If all prime ideals in a commutative ring are principal, so are all other ideals.