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.

• IsPrincipalIdealRing: a predicate on rings, saying that every left ideal is principal.
• generator: a generator of a principal ideal (or more generally submodule)
• to_unique_factorization_monoid: a PID is a unique factorization domain

Main results

• to_maximal_ideal: a non-zero prime ideal in a PID is maximal.
• EuclideanDomain.to_principal_ideal_domain : a Euclidean domain is a PID.

theorem Submodule.IsPrincipal_iff {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 Submodule.IsPrincipal {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : Prop

• principal' : ∃ a, S = Submodule.span R {a}

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}

instance bot_isPrincipal {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : Submodule.IsPrincipal ⊥

Equations

• @bot_isPrincipal = @bot_isPrincipal.proof_1

instance top_isPrincipal {R : Type u} [Ring R] : Submodule.IsPrincipal ⊤

Equations

• @top_isPrincipal = @top_isPrincipal.proof_1

theorem isPrincipalIdealRing_iff (R : Type u) [Ring R] : IsPrincipalIdealRing R ↔ ∀ (S : Ideal R), Submodule.IsPrincipal S

class IsPrincipalIdealRing (R : Type u) [Ring R] : Prop

• principal : ∀ (S : Ideal R), Submodule.IsPrincipal S

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

instance DivisionRing.isPrincipalIdealRing (K : Type u) [DivisionRing K] : IsPrincipalIdealRing K

Equations

• DivisionRing.isPrincipalIdealRing = DivisionRing.isPrincipalIdealRing.proof_1

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] : M

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

Equations

• Submodule.IsPrincipal.generator S = Classical.choose (_ : ∃ a, S = Submodule.span R {a})

theorem Submodule.IsPrincipal.span_singleton_generator {R : Type u} {M : Type v} [AddCommGroup M] [Ring R] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] : Submodule.span R {Submodule.IsPrincipal.generator S} = S

theorem Ideal.span_singleton_generator {R : Type u} [Ring R] (I : Ideal R) [Submodule.IsPrincipal I] : Ideal.span {Submodule.IsPrincipal.generator I} = I

@[simp]

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

theorem Submodule.IsPrincipal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [AddCommGroup M] [Ring R] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] {x : M} : x ∈ S ↔ ∃ s, x = s • Submodule.IsPrincipal.generator S

theorem Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero {R : Type u} {M : Type v} [AddCommGroup M] [Ring R] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] : S = ⊥ ↔ Submodule.IsPrincipal.generator S = 0

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 : Ideal.IsPrime S] (ne_bot : S ≠ ⊥) : Prime (Submodule.IsPrincipal.generator S)

theorem Submodule.IsPrincipal.generator_map_dvd_of_mem {R : Type u} {M : Type v} [AddCommGroup M] [CommRing R] [Module R M] {N : Submodule R M} (ϕ : M →ₗ[R] R) [Submodule.IsPrincipal (Submodule.map ϕ N)] {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} [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 := (_ : x ∈ O) }

theorem IsPrime.to_maximal_ideal {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : Ideal.IsPrime S] (hS : S ≠ ⊥) : Ideal.IsMaximal S

theorem mod_mem_iff {R : Type u} [EuclideanDomain R] {S : Ideal R} {x : R} {y : R} (hy : y ∈ S) : x % y ∈ S ↔ x ∈ S

instance EuclideanDomain.to_principal_ideal_domain {R : Type u} [EuclideanDomain R] : IsPrincipalIdealRing R

Equations

• @EuclideanDomain.to_principal_ideal_domain = @EuclideanDomain.to_principal_ideal_domain.proof_1

theorem IsField.isPrincipalIdealRing {R : Type u_1} [CommRing R] (h : IsField R) : IsPrincipalIdealRing R

instance PrincipalIdealRing.isNoetherianRing {R : Type u} [Ring R] [IsPrincipalIdealRing R] : IsNoetherianRing R

Equations

• @PrincipalIdealRing.isNoetherianRing = @PrincipalIdealRing.isNoetherianRing.proof_1

theorem PrincipalIdealRing.isMaximal_of_irreducible {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {p : R} (hp : Irreducible p) : Ideal.IsMaximal (Submodule.span R {p})

theorem PrincipalIdealRing.irreducible_iff_prime {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {p : R} : Irreducible p ↔ Prime p

theorem PrincipalIdealRing.associates_irreducible_iff_prime {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {p : Associates R} : Irreducible p ↔ Prime p

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 (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)

theorem PrincipalIdealRing.factors_spec {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (a : R) (h : a ≠ 0) : (∀ (b : R), b ∈ PrincipalIdealRing.factors a → Irreducible b) ∧ Associated (Multiset.prod (PrincipalIdealRing.factors a)) a

theorem PrincipalIdealRing.ne_zero_of_mem_factors {R : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a : R} {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 : R), 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 : R), 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 PrincipalIdealRing.to_uniqueFactorizationMonoid {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : UniqueFactorizationMonoid R

A principal ideal domain has unique factorization

Equations

• @PrincipalIdealRing.to_uniqueFactorizationMonoid = @PrincipalIdealRing.to_uniqueFactorizationMonoid.proof_1

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)] : Submodule.IsPrincipal 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)] : Submodule.IsPrincipal I

theorem IsPrincipalIdealRing.of_surjective {R : Type u} {S : Type u_1} [Ring R] [Ring S] [IsPrincipalIdealRing R] (f : R →+* S) (hf : Function.Surjective ↑f) : IsPrincipalIdealRing S

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) : IsUnit (gcd x y) ↔ IsCoprime x y

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 R → z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x 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 z → z ∣ x → ¬z ∣ y) : IsCoprime x 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 z → z ∣ x → ¬z ∣ y) : IsCoprime x y

theorem Irreducible.coprime_iff_not_dvd {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] {p : R} {n : R} (pp : Irreducible p) : IsCoprime p n ↔ ¬p ∣ n

theorem Prime.coprime_iff_not_dvd {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] {p : R} {n : R} (pp : Prime p) : IsCoprime p n ↔ ¬p ∣ n

theorem Irreducible.dvd_iff_not_coprime {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] {p : R} {n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n

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] : Set (Ideal R)

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

Equations

• nonPrincipals R = {I | ¬Submodule.IsPrincipal I}

theorem nonPrincipals_def (R : Type u) [CommRing R] {I : Ideal R} : I ∈ nonPrincipals R ↔ ¬Submodule.IsPrincipal I

theorem nonPrincipals_eq_empty_iff {R : Type u} [CommRing R] : nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R

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 ∈ 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.)

theorem IsPrincipalIdealRing.of_prime {R : Type u} [CommRing R] (H : ∀ (P : Ideal R), Ideal.IsPrime P → Submodule.IsPrincipal P) : IsPrincipalIdealRing R

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