doc-next-gen

Mathlib.RingTheory.PrincipalIdealDomain

Module docstring

{"# 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.

"}

IsBezout structure
Full source 
/-- A Bézout ring is a ring whose finitely generated ideals are principal. -/
class IsBezout : Prop where
  /-- Any finitely generated ideal is principal. -/
  isPrincipal_of_FG : ∀ I : Ideal R, I.FG → I.IsPrincipal
Bézout ring
Informal description
A Bézout ring is a ring in which every finitely generated ideal is principal.
Submodule.IsPrincipal.generator definition
(S : Submodule R M) [S.IsPrincipal] : M
Full source 
/-- `generator I`, if `I` is a principal submodule, is an `x ∈ M` such that `span R {x} = I` -/
noncomputable def generator (S : Submodule R M) [S.IsPrincipal] : M :=
  Classical.choose (principal S)
Generator of a principal submodule
Informal description
Given a principal submodule \( S \) of a module \( M \) over a ring \( R \), the function `generator` returns an element \( x \in M \) such that the span of \( \{x\} \) equals \( S \), i.e., \( \text{span}_R \{x\} = S \).
Submodule.IsPrincipal.span_singleton_generator theorem
(S : Submodule R M) [S.IsPrincipal] : span R {generator S} = S
Full source 
theorem span_singleton_generator (S : Submodule R M) [S.IsPrincipal] : span R {generator S} = S :=
  Eq.symm (Classical.choose_spec (principal S))
Span of Generator Equals Principal Submodule
Informal description
For any principal submodule $S$ of a module $M$ over a ring $R$, the span of the singleton set containing the generator of $S$ is equal to $S$ itself, i.e., $\text{span}_R \{\text{generator}(S)\} = S$.
Ideal.span_singleton_generator theorem
(I : Ideal R) [I.IsPrincipal] : Ideal.span ({generator I} : Set R) = I
Full source 
@[simp]
theorem _root_.Ideal.span_singleton_generator (I : Ideal R) [I.IsPrincipal] :
    Ideal.span ({generator I} : Set R) = I :=
  Eq.symm (Classical.choose_spec (principal I))
Principal Ideal Generated by its Generator
Informal description
For any principal ideal $I$ in a ring $R$, the ideal generated by the singleton set containing the generator of $I$ is equal to $I$ itself, i.e., $\text{span}_R \{\text{generator}(I)\} = I$.
Submodule.IsPrincipal.generator_mem theorem
(S : Submodule R M) [S.IsPrincipal] : generator S ∈ S
Full source 
@[simp]
theorem generator_mem (S : Submodule R M) [S.IsPrincipal] : generatorgenerator S ∈ S := by
  have : generatorgenerator S ∈ span R {generator S} := subset_span (mem_singleton _)
  convert this
  exact span_singleton_generator S |>.symm
Generator of Principal Submodule Belongs to the Submodule
Informal description
For any principal submodule $S$ of a module $M$ over a ring $R$, the generator of $S$ is an element of $S$, i.e., $\text{generator}(S) \in S$.
Submodule.IsPrincipal.mem_iff_eq_smul_generator theorem
(S : Submodule R M) [S.IsPrincipal] {x : M} : x ∈ S ↔ ∃ s : R, x = s • generator S
Full source 
theorem mem_iff_eq_smul_generator (S : Submodule R M) [S.IsPrincipal] {x : M} :
    x ∈ Sx ∈ S ↔ ∃ s : R, x = s • generator S := by
  simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]
Characterization of Membership in a Principal Submodule via Generator
Informal description
For a principal submodule $S$ of a module $M$ over a ring $R$, an element $x \in M$ belongs to $S$ if and only if there exists an element $s \in R$ such that $x = s \cdot \text{generator}(S)$.
Submodule.IsPrincipal.associated_generator_span_self theorem
[IsPrincipalIdealRing R] [IsDomain R] (r : R) : Associated (generator <| Ideal.span { r }) r
Full source 
theorem associated_generator_span_self [IsPrincipalIdealRing R] [IsDomain R] (r : R) :
    Associated (generator <| Ideal.span {r}) r := by
  rw [← Ideal.span_singleton_eq_span_singleton]
  exact Ideal.span_singleton_generator _
Generator of Principal Ideal $\langle r \rangle$ is Associated to $r$ in a PID
Informal description
Let $R$ be a principal ideal domain and let $r \in R$. Then the generator of the principal ideal $\langle r \rangle$ is associated to $r$, i.e., there exists a unit $u \in R$ such that $\text{generator}(\langle r \rangle) = u \cdot r$.
Submodule.IsPrincipal.mem_iff_generator_dvd theorem
(S : Ideal R) [S.IsPrincipal] {x : R} : x ∈ S ↔ generator S ∣ x
Full source 
theorem mem_iff_generator_dvd (S : Ideal R) [S.IsPrincipal] {x : R} : x ∈ Sx ∈ S ↔ generator S ∣ x :=
  (mem_iff_eq_smul_generator S).trans (exists_congr fun a => by simp only [mul_comm, smul_eq_mul])
Membership in Principal Ideal via Generator Divisibility
Informal description
For a principal ideal $S$ of a ring $R$, an element $x \in R$ belongs to $S$ if and only if the generator of $S$ divides $x$.
Submodule.IsPrincipal.prime_generator_of_isPrime theorem
(S : Ideal R) [S.IsPrincipal] [is_prime : S.IsPrime] (ne_bot : S ≠ ⊥) : Prime (generator S)
Full source 
theorem prime_generator_of_isPrime (S : Ideal R) [S.IsPrincipal] [is_prime : S.IsPrime]
    (ne_bot : S ≠ ⊥) : Prime (generator S) :=
  ⟨fun h => ne_bot ((eq_bot_iff_generator_eq_zero S).2 h), fun h =>
    is_prime.ne_top (S.eq_top_of_isUnit_mem (generator_mem S) h), fun _ _ => by
    simpa only [← mem_iff_generator_dvd S] using is_prime.2⟩
Generator of a Nonzero Prime Principal Ideal is Prime
Informal description
Let $R$ be a ring and $S$ a principal ideal of $R$ that is prime and nonzero. Then the generator of $S$ is a prime element in $R$.
Submodule.IsPrincipal.generator_map_dvd_of_mem theorem
{N : Submodule R M} (ϕ : M →ₗ[R] R) [(N.map ϕ).IsPrincipal] {x : M} (hx : x ∈ N) : generator (N.map ϕ) ∣ ϕ x
Full source 
theorem generator_map_dvd_of_mem {N : Submodule R M} (ϕ : M →ₗ[R] R) [(N.map ϕ).IsPrincipal] {x : M}
    (hx : x ∈ N) : generatorgenerator (N.map ϕ) ∣ ϕ x := by
  rw [← mem_iff_generator_dvd, Submodule.mem_map]
  exact ⟨x, hx, rfl⟩
Divisibility by Generator of Linear Image of Submodule
Informal description
Let $R$ be a ring and $M$ an $R$-module. Given a submodule $N$ of $M$ and a linear map $\phi: M \to R$, if the image of $N$ under $\phi$ is a principal ideal of $R$, then for any element $x \in N$, the generator of $\phi(N)$ divides $\phi(x)$.
Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem theorem
{N O : Submodule R M} (hNO : N ≤ O) (ϕ : O →ₗ[R] R) [(ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N) : generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩
Full source 
theorem generator_submoduleImage_dvd_of_mem {N O : Submodule R M} (hNO : N ≤ O) (ϕ : O →ₗ[R] R)
    [(ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N) :
    generatorgenerator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩ := by
  rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
  exact ⟨x, hx, rfl⟩
Divisibility by Generator in Linear Image of Submodule
Informal description
Let $R$ be a ring and $M$ an $R$-module. Let $N$ and $O$ be submodules of $M$ with $N \subseteq O$, and let $\phi: O \to R$ be a linear map. If the image of $N$ under $\phi$ is a principal submodule, then for any $x \in N$, the generator of $\phi(N)$ divides $\phi(x)$ (where $x$ is viewed as an element of $O$ via the inclusion $N \subseteq O$).
IsBezout.gcd definition
: R
Full source 
/-- A choice of gcd of two elements in a Bézout domain.

Note that the choice is usually not unique. -/
noncomputable def gcd : R := Submodule.IsPrincipal.generator (Ideal.span {x, y})
Greatest common divisor in a Bézout domain
Informal description
A choice of greatest common divisor (gcd) of two elements \( x \) and \( y \) in a Bézout domain \( R \). The gcd is chosen such that the ideal generated by \( \text{gcd}(x, y) \) equals the ideal generated by \( \{x, y\} \), i.e., \( \text{span}_R \{\text{gcd}(x, y)\} = \text{span}_R \{x, y\} \). Note that the choice of gcd is not necessarily unique.
IsBezout.span_gcd theorem
: Ideal.span {gcd x y} = Ideal.span { x, y }
Full source 
theorem span_gcd : Ideal.span {gcd x y} = Ideal.span {x, y} :=
  Ideal.span_singleton_generator _
GCD Generates Same Ideal as Pair in Bézout Ring
Informal description
For any two elements $x$ and $y$ in a Bézout ring $R$, the ideal generated by their greatest common divisor $\gcd(x,y)$ is equal to the ideal generated by $\{x, y\}$, i.e., $\text{span}_R \{\gcd(x,y)\} = \text{span}_R \{x, y\}$.
IsBezout.dvd_gcd theorem
(hx : z ∣ x) (hy : z ∣ y) : z ∣ gcd x y
Full source 
theorem dvd_gcd (hx : z ∣ x) (hy : z ∣ y) : z ∣ gcd x y := by
  rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
  rw [span_gcd, Ideal.span_insert, sup_le_iff]
  exact ⟨hx, hy⟩
Divisibility of GCD by Common Divisors in Bézout Rings
Informal description
For any elements $x$, $y$, and $z$ in a Bézout ring $R$, if $z$ divides both $x$ and $y$, then $z$ divides the greatest common divisor $\gcd(x, y)$.
IsRelPrime.isCoprime theorem
(h : IsRelPrime x y) : IsCoprime x y
Full source 
theorem _root_.IsRelPrime.isCoprime (h : IsRelPrime x y) : IsCoprime x y := by
  rw [← Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_sup_eq, ← Ideal.span_union,
    Set.singleton_union, ← span_gcd, Ideal.span_singleton_eq_top]
  exact h (gcd_dvd_left x y) (gcd_dvd_right x y)
Relatively Prime Implies Coprime in Bézout Rings
Informal description
If two elements $x$ and $y$ in a Bézout ring $R$ are relatively prime (i.e., $\text{span}_R \{x, y\} = \text{span}_R \{1\}$), then they are coprime (i.e., there exist $a, b \in R$ such that $a x + b y = 1$).
isRelPrime_iff_isCoprime theorem
: IsRelPrime x y ↔ IsCoprime x y
Full source 
theorem _root_.isRelPrime_iff_isCoprime : IsRelPrimeIsRelPrime x y ↔ IsCoprime x y :=
  ⟨IsRelPrime.isCoprime, IsCoprime.isRelPrime⟩
Equivalence of Relatively Prime and Coprime in Bézout Rings
Informal description
Two elements $x$ and $y$ in a Bézout ring $R$ are relatively prime (i.e., $\text{span}_R \{x, y\} = \text{span}_R \{1\}$) if and only if they are coprime (i.e., there exist $a, b \in R$ such that $a x + b y = 1$).
IsBezout.toGCDDomain definition
[IsBezout R] [IsDomain R] [DecidableEq R] : GCDMonoid R
Full source 
/-- 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. -/
noncomputable def toGCDDomain [IsBezout R] [IsDomain R] [DecidableEq R] : GCDMonoid R :=
  gcdMonoidOfGCD (gcd · ·) (gcd_dvd_left · ·) (gcd_dvd_right · ·) dvd_gcd
GCD Monoid Structure on a Bézout Domain
Informal description
Given a Bézout domain \( R \) with decidable equality, the structure `GCDMonoid R` is defined, where the greatest common divisor (gcd) of two elements \( x \) and \( y \) is chosen such that the ideal generated by \( \text{gcd}(x, y) \) equals the ideal generated by \( \{x, y\} \). This structure satisfies the properties that the gcd divides both \( x \) and \( y \), and any common divisor of \( x \) and \( y \) divides the gcd.
IsBezout.nonemptyGCDMonoid instance
[IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R)
Full source 
instance nonemptyGCDMonoid [IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R) := by
  classical exact ⟨toGCDDomain R⟩
Existence of GCD Monoid Structure on Bézout Domains
Informal description
For any Bézout domain $R$, there exists a GCD monoid structure on $R$.
IsBezout.associated_gcd_gcd theorem
[IsDomain R] [GCDMonoid R] : Associated (IsBezout.gcd x y) (GCDMonoid.gcd x y)
Full source 
theorem associated_gcd_gcd [IsDomain R] [GCDMonoid R] :
    Associated (IsBezout.gcd x y) (GCDMonoid.gcd x y) :=
  gcd_greatest_associated (gcd_dvd_left _ _ ) (gcd_dvd_right _ _) (fun _ => dvd_gcd)
Equivalence of Bézout GCD and GCD Monoid GCD in a Domain
Informal description
Let $R$ be a Bézout domain with a GCD monoid structure. For any elements $x, y \in R$, the greatest common divisor $\text{gcd}(x, y)$ defined via the Bézout property is associated to the greatest common divisor $\text{gcd}(x, y)$ defined via the GCD monoid structure.
IsPrime.to_maximal_ideal theorem
[CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : IsPrime S] (hS : S ≠ ⊥) : IsMaximal S
Full source 
theorem to_maximal_ideal [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R}
    [hpi : IsPrime S] (hS : S ≠ ⊥) : IsMaximal S :=
  isMaximal_iff.2
    ⟨(ne_top_iff_one S).1 hpi.1, by
      intro T x hST hxS hxT
      obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)
      cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
      | inl h =>
        have hTS : T ≤ S := by
          rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
        exact (hxS <| hTS hxT).elim
      | inr h =>
        obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
        have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
        rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
        exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)⟩
Nonzero Prime Ideals are Maximal in Principal Ideal Domains
Informal description
Let $R$ be a commutative principal ideal domain and $S$ a nonzero prime ideal of $R$. Then $S$ is a maximal ideal of $R$.
mod_mem_iff theorem
{S : Ideal R} {x y : R} (hy : y ∈ S) : x % y ∈ S ↔ x ∈ S
Full source 
theorem mod_mem_iff {S : Ideal R} {x y : R} (hy : y ∈ S) : x % y ∈ Sx % y ∈ S ↔ x ∈ S :=
  ⟨fun hxy => div_add_mod x y ▸ S.add_mem (S.mul_mem_right _ hy) hxy, fun hx =>
    (mod_eq_sub_mul_div x y).symm ▸ S.sub_mem hx (S.mul_mem_right _ hy)⟩
Membership Criterion via Remainder in Ideal
Informal description
Let $R$ be a ring, $S$ an ideal of $R$, and $x, y \in R$ with $y \in S$. Then the remainder $x \% y$ is in $S$ if and only if $x$ is in $S$.
EuclideanDomain.to_principal_ideal_domain instance
: IsPrincipalIdealRing R
Full source 
instance (priority := 100) EuclideanDomain.to_principal_ideal_domain : IsPrincipalIdealRing R where
  principal S := by classical exact
    ⟨if h : { x : R | x ∈ S ∧ x ≠ 0 }.Nonempty then
        have wf : WellFounded (EuclideanDomain.r : R → R → Prop) := EuclideanDomain.r_wellFounded
        have hmin : WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∈ S ∧
            WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ≠ 0 :=
          WellFounded.min_mem wf { x : R | x ∈ S ∧ x ≠ 0 } h
        ⟨WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h,
          Submodule.ext fun x => ⟨fun hx =>
            div_add_mod x (WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h) ▸
              (Ideal.mem_span_singleton.2 <| dvd_add (dvd_mul_right _ _) <| by
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h h₁ (mod_lt x hmin.2)
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
                simp [*]),
              fun hx =>
                let ⟨y, hy⟩ := Ideal.mem_span_singleton.1 hx
                hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
      else ⟨0, Submodule.ext fun a => by
            rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
            exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩⟩⟩
Euclidean Domains are Principal Ideal Rings
Informal description
Every Euclidean domain is a principal ideal ring.
PrincipalIdealRing.isMaximal_of_irreducible theorem
[CommSemiring R] [IsPrincipalIdealRing R] {p : R} (hp : Irreducible p) : Ideal.IsMaximal (span R ({ p } : Set R))
Full source 
theorem isMaximal_of_irreducible [CommSemiring R] [IsPrincipalIdealRing R] {p : R}
    (hp : Irreducible p) : Ideal.IsMaximal (span R ({p} : Set R)) :=
  ⟨⟨mt Ideal.span_singleton_eq_top.1 hp.1, fun I hI => by
      rcases principal I with ⟨a, rfl⟩
      rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]
      rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
      refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_lt hI))
      rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]⟩⟩
Maximality of Ideals Generated by Irreducible Elements in Principal Ideal Rings
Informal description
Let $R$ be a commutative semiring that is a principal ideal ring. For any irreducible element $p \in R$, the ideal generated by $p$ is maximal, i.e., $\langle p \rangle$ is a maximal ideal in $R$.
PrincipalIdealRing.factors definition
(a : R) : Multiset R
Full source 
/-- `factors a` is a multiset of irreducible elements whose product is `a`, up to units -/
noncomputable def factors (a : R) : Multiset R :=
  if h : a = 0 then ∅ else Classical.choose (WfDvdMonoid.exists_factors a h)
Factorization into irreducibles in a principal ideal ring
Informal description
For a nonzero element \( a \) in a principal ideal ring \( R \), the function `factors a` returns a multiset of irreducible elements whose product is associated to \( a \). If \( a = 0 \), the empty multiset is returned.
PrincipalIdealRing.factors_spec theorem
(a : R) (h : a ≠ 0) : (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a
Full source 
theorem factors_spec (a : R) (h : a ≠ 0) :
    (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a := by
  unfold factors; rw [dif_neg h]
  exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)
Factorization into Irreducibles in Principal Ideal Rings
Informal description
For any nonzero element $a$ in a principal ideal ring $R$, the multiset $\text{factors}(a)$ consists entirely of irreducible elements, and the product of these factors is associated to $a$. That is, every element $b \in \text{factors}(a)$ is irreducible, and there exists a unit $u \in R$ such that $u \cdot \prod_{b \in \text{factors}(a)} b = a$.
PrincipalIdealRing.ne_zero_of_mem_factors theorem
{R : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} (ha : a ≠ 0) (hb : b ∈ factors a) : b ≠ 0
Full source 
theorem 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 :=
  Irreducible.ne_zero ((factors_spec a ha).1 b hb)
Nonzero Irreducible Factors in Principal Ideal Domains
Informal description
Let $R$ be a principal ideal domain, and let $a \in R$ be a nonzero element. If $b$ is an irreducible factor in the factorization of $a$ (i.e., $b \in \text{factors}(a)$), then $b$ is nonzero.
PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset theorem
(s : Submonoid R) {a : R} (ha : a ≠ 0) (hfac : ∀ b ∈ factors a, b ∈ s) (hunit : ∀ c : Rˣ, (c : R) ∈ s) : a ∈ s
Full source 
theorem mem_submonoid_of_factors_subset_of_units_subset (s : Submonoid R) {a : R} (ha : a ≠ 0)
    (hfac : ∀ b ∈ factors a, b ∈ s) (hunit : ∀ c : Rˣ, (c : R) ∈ s) : a ∈ s := by
  rcases (factors_spec a ha).2 with ⟨c, hc⟩
  rw [← hc]
  exact mul_mem (multiset_prod_mem _ hfac) (hunit _)
Submonoid Membership via Factorization in Principal Ideal Domains
Informal description
Let $R$ be a principal ideal domain and $s$ a submonoid of $R$. For any nonzero element $a \in R$, if all irreducible factors of $a$ belong to $s$ and all units of $R$ belong to $s$, then $a$ itself belongs to $s$.
PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset theorem
{R S : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [NonAssocSemiring S] (f : R →+* S) (s : Submonoid S) (a : R) (ha : a ≠ 0) (h : ∀ b ∈ factors a, f b ∈ s) (hf : ∀ c : Rˣ, f c ∈ s) : f a ∈ s
Full source 
/-- 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. -/
theorem ringHom_mem_submonoid_of_factors_subset_of_units_subset {R S : Type*} [CommRing R]
    [IsDomain R] [IsPrincipalIdealRing R] [NonAssocSemiring S] (f : R →+* S) (s : Submonoid S)
    (a : R) (ha : a ≠ 0) (h : ∀ b ∈ factors a, f b ∈ s) (hf : ∀ c : Rˣ, f c ∈ s) : f a ∈ s :=
  mem_submonoid_of_factors_subset_of_units_subset (s.comap f.toMonoidHom) ha h hf
Ring Homomorphism Preserves Submonoid Membership via Factorization in Principal Ideal Domains
Informal description
Let $R$ be a principal ideal domain and $S$ a non-associative semiring. Given a ring homomorphism $f \colon R \to S$, a submonoid $s$ of $S$, and a nonzero element $a \in R$, if $f$ maps all irreducible factors of $a$ into $s$ and all units of $R$ into $s$, then $f(a) \in s$.
Submodule.IsPrincipal.map theorem
(f : M →ₗ[R] N) {S : Submodule R M} (hI : IsPrincipal S) : IsPrincipal (map f S)
Full source 
theorem Submodule.IsPrincipal.map (f : M →ₗ[R] N) {S : Submodule R M}
    (hI : IsPrincipal S) : IsPrincipal (map f S) :=
  ⟨⟨f (IsPrincipal.generator S), by
      rw [← Set.image_singleton, ← map_span, span_singleton_generator]⟩⟩
Image of a Principal Submodule under a Linear Map is Principal
Informal description
Let $f : M \to N$ be a linear map between modules over a ring $R$, and let $S$ be a principal submodule of $M$. Then the image of $S$ under $f$, denoted by $f(S)$, is also a principal submodule of $N$.
Submodule.IsPrincipal.of_comap theorem
(f : M →ₗ[R] N) (hf : Function.Surjective f) (S : Submodule R N) [hI : IsPrincipal (S.comap f)] : IsPrincipal S
Full source 
theorem Submodule.IsPrincipal.of_comap (f : M →ₗ[R] N) (hf : Function.Surjective f)
    (S : Submodule R N) [hI : IsPrincipal (S.comap f)] : IsPrincipal S := by
  rw [← Submodule.map_comap_eq_of_surjective hf S]
  exact hI.map f
Principal Submodule Property via Surjective Linear Map Preimage
Informal description
Let $f : M \to N$ be a surjective linear map between modules over a ring $R$, and let $S$ be a submodule of $N$. If the preimage of $S$ under $f$ is a principal submodule of $M$, then $S$ itself is a principal submodule of $N$.
Submodule.IsPrincipal.map_ringHom theorem
(f : F) {I : Ideal R} (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I)
Full source 
theorem Submodule.IsPrincipal.map_ringHom (f : F) {I : Ideal R}
    (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I) :=
  ⟨⟨f (IsPrincipal.generator I), by
      rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]⟩⟩
Image of a Principal Ideal under a Ring Homomorphism is Principal
Informal description
Let $f : R \to S$ be a ring homomorphism and $I$ be a principal ideal in $R$. Then the image of $I$ under $f$, denoted by $f(I)$, is a principal ideal in $S$.
Ideal.IsPrincipal.of_comap theorem
(f : F) (hf : Function.Surjective f) (I : Ideal S) [hI : IsPrincipal (I.comap f)] : IsPrincipal I
Full source 
theorem Ideal.IsPrincipal.of_comap (f : F) (hf : Function.Surjective f) (I : Ideal S)
    [hI : IsPrincipal (I.comap f)] : IsPrincipal I := by
  rw [← map_comap_of_surjective f hf I]
  exact hI.map_ringHom f
Principal Ideal Property via Surjective Ring Homomorphism Preimage
Informal description
Let $f : R \to S$ be a surjective ring homomorphism and $I$ be an ideal of $S$. If the preimage of $I$ under $f$ is a principal ideal of $R$, then $I$ is a principal ideal of $S$.
IsPrincipalIdealRing.of_surjective theorem
[IsPrincipalIdealRing R] (f : F) (hf : Function.Surjective f) : IsPrincipalIdealRing S
Full source 
/-- The surjective image of a principal ideal ring is again a principal ideal ring. -/
theorem IsPrincipalIdealRing.of_surjective [IsPrincipalIdealRing R] (f : F)
    (hf : Function.Surjective f) : IsPrincipalIdealRing S :=
  ⟨fun I => Ideal.IsPrincipal.of_comap f hf I⟩
Surjective Image of a Principal Ideal Ring is Principal
Informal description
Let $R$ be a principal ideal ring and $f : R \to S$ be a surjective ring homomorphism. Then $S$ is also a principal ideal ring.
isCoprime_of_dvd theorem
(x y : R) (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y
Full source 
theorem isCoprime_of_dvd (x y : R) (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
  (isRelPrime_of_no_nonunits_factors nonzero H).isCoprime
Coprimality Condition via Non-Divisibility of Non-Units
Informal description
Let $x$ and $y$ be elements of a ring $R$ such that not both are zero. If for every non-zero non-unit $z \in R$, $z$ divides $x$ implies $z$ does not divide $y$, then $x$ and $y$ are coprime (i.e., there exist $a, b \in R$ such that $a x + b y = 1$).
Irreducible.coprime_iff_not_dvd theorem
{p n : R} (hp : Irreducible p) : IsCoprime p n ↔ ¬p ∣ n
Full source 
/-- See also `Irreducible.isRelPrime_iff_not_dvd`. -/
theorem Irreducible.coprime_iff_not_dvd {p n : R} (hp : Irreducible p) :
    IsCoprimeIsCoprime p n ↔ ¬p ∣ n := by rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]
Coprimality of Irreducible Element and Another Element is Equivalent to Non-Divisibility
Informal description
Let $p$ be an irreducible element in a ring $R$ and let $n$ be any element of $R$. Then $p$ and $n$ are coprime (i.e., there exist $a, b \in R$ such that $a p + b n = 1$) if and only if $p$ does not divide $n$.
Irreducible.dvd_iff_not_isCoprime theorem
{p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n
Full source 
/-- See also `Irreducible.coprime_iff_not_dvd'`. -/
theorem Irreducible.dvd_iff_not_isCoprime {p n : R} (hp : Irreducible p) : p ∣ np ∣ n ↔ ¬IsCoprime p n :=
  iff_not_comm.2 hp.coprime_iff_not_dvd
Divisibility by Irreducible Element is Equivalent to Non-Coprimality
Informal description
Let $p$ be an irreducible element in a ring $R$ and let $n$ be any element of $R$. Then $p$ divides $n$ if and only if $p$ and $n$ are not coprime.
Irreducible.coprime_pow_of_not_dvd theorem
{p a : R} (m : ℕ) (hp : Irreducible p) (h : ¬p ∣ a) : IsCoprime a (p ^ m)
Full source 
theorem Irreducible.coprime_pow_of_not_dvd {p a : R} (m : ℕ) (hp : Irreducible p) (h : ¬p ∣ a) :
    IsCoprime a (p ^ m) :=
  (hp.coprime_iff_not_dvd.2 h).symm.pow_right
Coprimality of Element with Power of Irreducible Element: $\text{IsCoprime}(a, p^m)$ when $p \nmid a$
Informal description
Let $p$ be an irreducible element in a ring $R$ and let $a \in R$ be such that $p$ does not divide $a$. Then for any natural number $m$, the elements $a$ and $p^m$ are coprime, i.e., $\text{IsCoprime}(a, p^m)$ holds.
IsBezout.span_gcd_eq_span_gcd theorem
(x y : R) : span {GCDMonoid.gcd x y} = span {IsBezout.gcd x y}
Full source 
theorem IsBezout.span_gcd_eq_span_gcd (x y : R) :
    span {GCDMonoid.gcd x y} = span {IsBezout.gcd x y} := by
  rw [Ideal.span_singleton_eq_span_singleton]
  exact associated_of_dvd_dvd
    (IsBezout.dvd_gcd (GCDMonoid.gcd_dvd_left _ _) <| GCDMonoid.gcd_dvd_right _ _)
    (GCDMonoid.dvd_gcd (IsBezout.gcd_dvd_left _ _) <| IsBezout.gcd_dvd_right _ _)
Equality of GCD-Generated Ideals in Bézout Rings: $\text{span}\{\gcd_{\text{GCDMonoid}}(x,y)\} = \text{span}\{\gcd_{\text{IsBezout}}(x,y)\}$
Informal description
For any elements $x$ and $y$ in a Bézout ring $R$, the ideal generated by the greatest common divisor $\gcd(x,y)$ (as defined in the `GCDMonoid` structure) is equal to the ideal generated by the greatest common divisor $\gcd(x,y)$ (as defined in the `IsBezout` structure).
span_gcd theorem
(x y : R) : span {gcd x y} = span { x, y }
Full source 
theorem span_gcd (x y : R) : span {gcd x y} = span {x, y} := by
  rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]
GCD-Generated Ideal Equals Ideal Generated by Pair in Bézout Ring
Informal description
For any two elements $x$ and $y$ in a Bézout ring $R$, the ideal generated by their greatest common divisor $\gcd(x,y)$ is equal to the ideal generated by the set $\{x, y\}$, i.e., $\text{span}_R \{\gcd(x,y)\} = \text{span}_R \{x, y\}$.
gcd_dvd_iff_exists theorem
(a b : R) {z} : gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
Full source 
theorem gcd_dvd_iff_exists (a b : R) {z} : gcdgcd a b ∣ zgcd a b ∣ z ↔ ∃ x y, z = a * x + b * y := by
  simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
Bézout's Identity: $\gcd(a,b) \mid z \iff \exists x y, z = a x + b y$
Informal description
Let $R$ be a Bézout ring. For any elements $a, b, z \in R$, the greatest common divisor $\gcd(a,b)$ divides $z$ if and only if there exist elements $x, y \in R$ such that $z = a x + b y$.
exists_gcd_eq_mul_add_mul theorem
(a b : R) : ∃ x y, gcd a b = a * x + b * y
Full source 
/-- **Bézout's lemma** -/
theorem exists_gcd_eq_mul_add_mul (a b : R) : ∃ x y, gcd a b = a * x + b * y := by
  rw [← gcd_dvd_iff_exists]
Bézout's Identity: $\gcd(a,b) = a x + b y$ for some $x,y$
Informal description
Let $R$ be a Bézout ring. For any elements $a, b \in R$, there exist elements $x, y \in R$ such that the greatest common divisor $\gcd(a,b)$ can be expressed as $a x + b y$.
gcd_isUnit_iff theorem
(x y : R) : IsUnit (gcd x y) ↔ IsCoprime x y
Full source 
theorem gcd_isUnit_iff (x y : R) : IsUnitIsUnit (gcd x y) ↔ IsCoprime x y := by
  rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
$\gcd(x,y)$ is a unit if and only if $x$ and $y$ are coprime
Informal description
For any elements $x$ and $y$ in a Bézout ring $R$, the greatest common divisor $\gcd(x,y)$ is a unit if and only if $x$ and $y$ are coprime (i.e., $\text{span}_R\{x,y\} = R$).
Prime.coprime_iff_not_dvd theorem
{p n : R} (hp : Prime p) : IsCoprime p n ↔ ¬p ∣ n
Full source 
theorem Prime.coprime_iff_not_dvd {p n : R} (hp : Prime p) : IsCoprimeIsCoprime p n ↔ ¬p ∣ n :=
  hp.irreducible.coprime_iff_not_dvd
Coprimality of Prime Element and Another Element is Equivalent to Non-Divisibility
Informal description
Let $p$ be a prime element in a ring $R$ and let $n$ be any element of $R$. Then $p$ and $n$ are coprime (i.e., $\text{span}_R\{p,n\} = R$) if and only if $p$ does not divide $n$.
exists_associated_pow_of_mul_eq_pow' theorem
{a b c : R} (hab : IsCoprime a b) {k : ℕ} (h : a * b = c ^ k) : ∃ d : R, Associated (d ^ k) a
Full source 
theorem exists_associated_pow_of_mul_eq_pow' {a b c : R} (hab : IsCoprime a b) {k : ℕ}
    (h : a * b = c ^ k) : ∃ d : R, Associated (d ^ k) a := by
  classical
  letI := IsBezout.toGCDDomain R
  exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h
Existence of Associated $k$-th Power in Bézout Rings for Coprime Elements
Informal description
Let $R$ be a Bézout ring. For any elements $a, b, c \in R$ such that $a$ and $b$ are coprime, and for any natural number $k$, if $a \cdot b = c^k$, then there exists an element $d \in R$ such that $d^k$ is associated to $a$.
exists_associated_pow_of_associated_pow_mul theorem
{a b c : R} (hab : IsCoprime a b) {k : ℕ} (h : Associated (c ^ k) (a * b)) : ∃ d : R, Associated (d ^ k) a
Full source 
theorem exists_associated_pow_of_associated_pow_mul {a b c : R} (hab : IsCoprime a b) {k : ℕ}
    (h : Associated (c ^ k) (a * b)) : ∃ d : R, Associated (d ^ k) a := by
  obtain ⟨u, hu⟩ := h.symm
  exact exists_associated_pow_of_mul_eq_pow'
    ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu
Existence of Associated $k$-th Power in Bézout Rings for Coprime Elements under Associated Product Condition
Informal description
Let $R$ be a Bézout ring. For any elements $a, b, c \in R$ such that $a$ and $b$ are coprime, and for any natural number $k$, if $c^k$ is associated to $a \cdot b$, then there exists an element $d \in R$ such that $d^k$ is associated to $a$.
isCoprime_of_irreducible_dvd theorem
{x y : R} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z : R, Irreducible z → z ∣ x → ¬z ∣ y) : IsCoprime x y
Full source 
theorem isCoprime_of_irreducible_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z : R, Irreducible z → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
  (WfDvdMonoid.isRelPrime_of_no_irreducible_factors nonzero H).isCoprime
Irreducible Divisibility Condition Implies Coprimality in Bézout Rings
Informal description
For any elements $x$ and $y$ in a Bézout ring $R$ such that not both $x$ and $y$ are zero, if every irreducible element $z$ that divides $x$ does not divide $y$, then $x$ and $y$ are coprime.
isCoprime_of_prime_dvd theorem
{x y : R} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z : R, Prime z → z ∣ x → ¬z ∣ y) : IsCoprime x y
Full source 
theorem isCoprime_of_prime_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z : R, Prime z → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
  isCoprime_of_irreducible_dvd nonzero fun z zi ↦ H z zi.prime
Coprimality from Prime Divisibility in Bézout Rings
Informal description
For any elements $x$ and $y$ in a Bézout ring $R$ such that not both $x$ and $y$ are zero, if every prime element $z$ that divides $x$ does not divide $y$, then $x$ and $y$ are coprime.
nonPrincipals definition
Full source 
/-- `nonPrincipals R` is the set of all ideals of `R` that are not principal ideals. -/
def nonPrincipals :=
  { I : Ideal R | ¬I.IsPrincipal }
Set of non-principal ideals
Informal description
The set `nonPrincipals R` consists of all ideals \( I \) of the ring \( R \) that are not principal ideals, i.e., ideals that cannot be generated by a single element.
nonPrincipals_eq_empty_iff theorem
: nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R
Full source 
theorem nonPrincipals_eq_empty_iff : nonPrincipalsnonPrincipals R = ∅ ↔ IsPrincipalIdealRing R := by
  simp [Set.eq_empty_iff_forall_not_mem, isPrincipalIdealRing_iff, nonPrincipals_def]
Characterization of Principal Ideal Rings via Non-Principal Ideals
Informal description
The set of non-principal ideals of a ring $R$ is empty if and only if $R$ is a principal ideal ring. In other words, $R$ is a principal ideal ring precisely when every ideal of $R$ is principal.
nonPrincipals_zorn theorem
(c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R) (hchain : IsChain (· ≤ ·) c) {K : Ideal R} (hKmem : K ∈ c) : ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
Full source 
/-- 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 nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R)
    (hchain : IsChain (· ≤ ·) c) {K : Ideal R} (hKmem : K ∈ c) :
    ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I := by
  refine ⟨sSup c, ?_, fun J hJ => le_sSup hJ⟩
  rintro ⟨x, hx⟩
  have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
  obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
  have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
  specialize hs hJc
  rw [← hsSupJ, hx, nonPrincipals_def] at hs
  exact hs ⟨⟨x, rfl⟩⟩
Existence of Upper Bound for Chains of Non-Principal Ideals
Informal description
Let $R$ be a ring and let $c$ be a chain of non-principal ideals in $R$ (i.e., $c \subseteq \text{nonPrincipals}(R)$ and $c$ is totally ordered by inclusion). For any ideal $K \in c$, there exists a non-principal ideal $I$ in $R$ such that $I$ is an upper bound for $c$, meaning that $J \leq I$ for all $J \in c$.