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
[is_domain R] [is_principal_ideal_ring R]. There is no explicit definition of a PID.
Theorems about PID's are in the principal_ideal_ring namespace.
is_principal_ideal_ring: 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.euclidean_domain.to_principal_ideal_domain: a Euclidean domain is a PID.
@[class]
structure
submodule.is_principal
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(S : submodule R M) :
Prop
- principal : ∃ (a : M), S = submodule.span R {a}
An R-submodule of M is principal if it is generated by one element.
@[protected, instance]
@[class]
- principal : ∀ (S : ideal R), submodule.is_principal S
A ring is a principal ideal ring if all (left) ideals are principal.
@[protected, instance]
noncomputable
def
submodule.is_principal.generator
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(S : submodule R M)
[S.is_principal] :
M
generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I
Equations
theorem
submodule.is_principal.span_singleton_generator
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(S : submodule R M)
[S.is_principal] :
theorem
ideal.span_singleton_generator
{R : Type u}
[ring R]
(I : ideal R)
[submodule.is_principal I] :
@[simp]
theorem
submodule.is_principal.generator_mem
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(S : submodule R M)
[S.is_principal] :
theorem
submodule.is_principal.mem_iff_eq_smul_generator
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(S : submodule R M)
[S.is_principal]
{x : M} :
x ∈ S ↔ ∃ (s : R), x = s • submodule.is_principal.generator S
theorem
submodule.is_principal.eq_bot_iff_generator_eq_zero
{R : Type u}
{M : Type v}
[add_comm_group M]
[ring R]
[module R M]
(S : submodule R M)
[S.is_principal] :
S = ⊥ ↔ submodule.is_principal.generator S = 0
theorem
submodule.is_principal.mem_iff_generator_dvd
{R : Type u}
[comm_ring R]
(S : ideal R)
[submodule.is_principal S]
{x : R} :
x ∈ S ↔ submodule.is_principal.generator S ∣ x
theorem
submodule.is_principal.prime_generator_of_is_prime
{R : Type u}
[comm_ring R]
(S : ideal R)
[submodule.is_principal S]
[is_prime : S.is_prime]
(ne_bot : S ≠ ⊥) :
theorem
submodule.is_principal.generator_map_dvd_of_mem
{R : Type u}
{M : Type v}
[add_comm_group M]
[comm_ring R]
[module R M]
{N : submodule R M}
(ϕ : M →ₗ[R] R)
[(submodule.map ϕ N).is_principal]
{x : M}
(hx : x ∈ N) :
submodule.is_principal.generator (submodule.map ϕ N) ∣ ⇑ϕ x
theorem
submodule.is_principal.generator_submodule_image_dvd_of_mem
{R : Type u}
{M : Type v}
[add_comm_group M]
[comm_ring R]
[module R M]
{N O : submodule R M}
(hNO : N ≤ O)
(ϕ : ↥O →ₗ[R] R)
[(ϕ.submodule_image N).is_principal]
{x : M}
(hx : x ∈ N) :
submodule.is_principal.generator (ϕ.submodule_image N) ∣ ⇑ϕ ⟨x, _⟩
theorem
is_prime.to_maximal_ideal
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
{S : ideal R}
[hpi : S.is_prime]
(hS : S ≠ ⊥) :
@[protected, instance]
@[protected, instance]
theorem
principal_ideal_ring.is_maximal_of_irreducible
{R : Type u}
[comm_ring R]
[is_principal_ideal_ring R]
{p : R}
(hp : irreducible p) :
ideal.is_maximal (submodule.span R {p})
theorem
principal_ideal_ring.irreducible_iff_prime
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
{p : R} :
irreducible p ↔ prime p
theorem
principal_ideal_ring.associates_irreducible_iff_prime
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
{p : associates R} :
irreducible p ↔ prime p
noncomputable
def
principal_ideal_ring.factors
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
(a : R) :
multiset R
factors a is a multiset of irreducible elements whose product is a, up to units
Equations
- principal_ideal_ring.factors a = dite (a = 0) (λ (h : a = 0), ∅) (λ (h : ¬a = 0), classical.some _)
theorem
principal_ideal_ring.factors_spec
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
(a : R)
(h : a ≠ 0) :
(∀ (b : R), b ∈ principal_ideal_ring.factors a → irreducible b) ∧ associated (principal_ideal_ring.factors a).prod a
theorem
principal_ideal_ring.ne_zero_of_mem_factors
{R : Type v}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
{a b : R}
(ha : a ≠ 0)
(hb : b ∈ principal_ideal_ring.factors a) :
b ≠ 0
theorem
principal_ideal_ring.mem_submonoid_of_factors_subset_of_units_subset
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
(s : submonoid R)
{a : R}
(ha : a ≠ 0)
(hfac : ∀ (b : R), b ∈ principal_ideal_ring.factors a → b ∈ s)
(hunit : ∀ (c : Rˣ), ↑c ∈ s) :
a ∈ s
theorem
principal_ideal_ring.ring_hom_mem_submonoid_of_factors_subset_of_units_subset
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[semiring S]
(f : R →+* S)
(s : submonoid S)
(a : R)
(ha : a ≠ 0)
(h : ∀ (b : R), b ∈ principal_ideal_ring.factors a → ⇑f b ∈ s)
(hf : ∀ (c : Rˣ), ⇑f ↑c ∈ s) :
If a ring_hom maps all units and all factors of an element a into a submonoid s, then it
also maps a into that submonoid.
@[protected, instance]
def
principal_ideal_ring.to_unique_factorization_monoid
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R] :
A principal ideal domain has unique factorization
theorem
submodule.is_principal.of_comap
{R : Type u}
{M : Type v}
{N : Type u_2}
[ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(f : M →ₗ[R] N)
(hf : function.surjective ⇑f)
(S : submodule R N)
[hI : (submodule.comap f S).is_principal] :
theorem
ideal.is_principal.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.is_principal (ideal.comap f I)] :
theorem
is_principal_ideal_ring.of_surjective
{R : Type u}
{S : Type u_1}
[ring R]
[ring S]
[is_principal_ideal_ring R]
(f : R →+* S)
(hf : function.surjective ⇑f) :
The surjective image of a principal ideal ring is again a principal ideal ring.
theorem
span_gcd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(x y : R) :
ideal.span {gcd x y} = ideal.span {x, y}
theorem
gcd_dvd_iff_exists
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(a b : R)
{z : R} :
theorem
exists_gcd_eq_mul_add_mul
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(a b : R) :
Bézout's lemma
theorem
gcd_is_unit_iff
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(x y : R) :
is_unit (gcd x y) ↔ is_coprime x y
theorem
is_coprime_of_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(x y : R)
(nonzero : ¬(x = 0 ∧ y = 0))
(H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y) :
is_coprime x y
theorem
dvd_or_coprime
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
(x y : R)
(h : irreducible x) :
x ∣ y ∨ is_coprime x y
theorem
is_coprime_of_irreducible_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{x y : R}
(nonzero : ¬(x = 0 ∧ y = 0))
(H : ∀ (z : R), irreducible z → z ∣ x → ¬z ∣ y) :
is_coprime x y
theorem
is_coprime_of_prime_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{x y : R}
(nonzero : ¬(x = 0 ∧ y = 0))
(H : ∀ (z : R), prime z → z ∣ x → ¬z ∣ y) :
is_coprime x y
theorem
irreducible.coprime_iff_not_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{p n : R}
(pp : irreducible p) :
is_coprime p n ↔ ¬p ∣ n
theorem
prime.coprime_iff_not_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{p n : R}
(pp : prime p) :
is_coprime p n ↔ ¬p ∣ n
theorem
irreducible.dvd_iff_not_coprime
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{p n : R}
(hp : irreducible p) :
p ∣ n ↔ ¬is_coprime p n
theorem
irreducible.coprime_pow_of_not_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{p a : R}
(m : ℕ)
(hp : irreducible p)
(h : ¬p ∣ a) :
is_coprime a (p ^ m)
theorem
irreducible.coprime_or_dvd
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{p : R}
(hp : irreducible p)
(i : R) :
is_coprime p i ∨ p ∣ i
theorem
exists_associated_pow_of_mul_eq_pow'
{R : Type u}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[gcd_monoid R]
{a b c : R}
(hab : is_coprime a b)
{k : ℕ}
(h : a * b = c ^ k) :
∃ (d : R), associated (d ^ k) a