Fractional ideals prime to an ideal

TheoremNon-zero-divisors stay non-zero-divisors in a localization at a prime#✓fully proved

Let \(A\) be a commutative ring and \(\mathfrak p\) a prime ideal of \(A\). Every non-zero-divisor of \(A\) maps to a non-zero-divisor of the localization \(A_{\mathfrak p}\).

theorem nonZeroDivisors_le_comap_algebraMap_atPrime
    (p : Ideal A) [p.IsPrime] :
    A⁰ ≤ Submonoid.comap (algebraMap A (Localization.AtPrime p))
      (Localization.AtPrime p)⁰

Used by 5

Used byInverses of invertible fractional ideals prime to an ideal · Fractional ideals prime to an ideal · The unit fractional ideal is prime to every ideal · Products of fractional ideals prime to an ideal · Every invertible fractional ideal is prime to the unit ideal

DefinitionFractional ideals prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(I\) be a fractional ideal of \(A\) in \(K\) and let \(J\) be an ideal of \(A\). Then \(I\) is prime to \(J\) if for every prime ideal \(\mathfrak p\) of \(A\) with \(J \subseteq \mathfrak p\), the extension \(I A_{\mathfrak p}\) of \(I\) to the localization \(A_{\mathfrak p}\), a fractional ideal of \(A_{\mathfrak p}\) in \(K\), is the unit fractional ideal \(A_{\mathfrak p}\).

def IsPrimeTo (I : FractionalIdeal A⁰ (FractionRing A)) (J : Ideal A) : Prop :=
  ∀ (p : Ideal A) [p.IsPrime], J ≤ p →
    FractionalIdeal.extended (FractionRing A)
      (nonZeroDivisors_le_comap_algebraMap_atPrime p) I = 1

Uses 1 · Used by 7

Statement usesNon-zero-divisors stay non-zero-divisors in a localization at a prime

Used byInverses of invertible fractional ideals prime to an ideal · The unit fractional ideal is prime to every ideal · Membership in the subgroup of units prime to an ideal · Prime to an ideal implies prime to every larger ideal · Products of fractional ideals prime to an ideal · Invertible fractional ideals prime to an ideal · Every invertible fractional ideal is prime to the unit ideal

TheoremThe unit fractional ideal is prime to every ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\). For every ideal \(J\) of \(A\), the unit fractional ideal \(A\) of \(A\) in \(K\) is prime to \(J\).

@[simp]
theorem isPrimeTo_one (J : Ideal A) :
    IsPrimeTo (1 : FractionalIdeal A⁰ (FractionRing A)) J

Uses 2 · Used by 1

Statement usesFractional ideals prime to an ideal

Proof usesNon-zero-divisors stay non-zero-divisors in a localization at a prime

Used byInvertible fractional ideals prime to an ideal

TheoremProducts of fractional ideals prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(J\) be an ideal of \(A\). If fractional ideals \(I\) and \(I'\) of \(A\) in \(K\) are both prime to \(J\), then their product \(I I'\) is prime to \(J\).

theorem IsPrimeTo.mul {I K : FractionalIdeal A⁰ (FractionRing A)}
    {J : Ideal A} (hI : I.IsPrimeTo J) (hK : K.IsPrimeTo J) :
    (I * K).IsPrimeTo J

Uses 2 · Used by 1

Statement usesFractional ideals prime to an ideal

Proof usesNon-zero-divisors stay non-zero-divisors in a localization at a prime

Used byInvertible fractional ideals prime to an ideal

TheoremInverses of invertible fractional ideals prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(J\) be an ideal of \(A\). If an invertible fractional ideal \(I\) of \(A\) in \(K\) is prime to \(J\), then its inverse \(I^{-1}\) is prime to \(J\).

theorem IsPrimeTo.inv_unit
    {u : (FractionalIdeal A⁰ (FractionRing A))ˣ} {J : Ideal A}
    (hu : (u : FractionalIdeal A⁰ (FractionRing A)).IsPrimeTo J) :
    ((u⁻¹ : (FractionalIdeal A⁰ (FractionRing A))ˣ) :
      FractionalIdeal A⁰ (FractionRing A)).IsPrimeTo J

Uses 2 · Used by 1

Statement usesFractional ideals prime to an ideal

Proof usesNon-zero-divisors stay non-zero-divisors in a localization at a prime

Used byInvertible fractional ideals prime to an ideal

DefinitionInvertible fractional ideals prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(J\) be an ideal of \(A\). The invertible fractional ideals of \(A\) in \(K\) that are prime to \(J\) form a subgroup of the group of invertible fractional ideals of \(A\) in \(K\).

def unitsPrimeTo (J : Ideal A) :
    Subgroup (FractionalIdeal A⁰ (FractionRing A))ˣ where
  carrier := {u | (u : FractionalIdeal A⁰ (FractionRing A)).IsPrimeTo J}
  one_mem' := isPrimeTo_one J
  mul_mem' := fun ha hb => ha.mul hb
  inv_mem' := fun hu => hu.inv_unit

Uses 4 · Used by 3

Statement usesFractional ideals prime to an ideal · Inverses of invertible fractional ideals prime to an ideal · Products of fractional ideals prime to an ideal · The unit fractional ideal is prime to every ideal

Used byMembership in the subgroup of units prime to an ideal · Monotonicity of the subgroups of units prime to an ideal · Every invertible fractional ideal is prime to the unit ideal

TheoremMembership in the subgroup of units prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(J\) be an ideal of \(A\). An invertible fractional ideal \(I\) of \(A\) in \(K\) lies in the subgroup of invertible fractional ideals prime to \(J\) if and only if \(I\) is prime to \(J\).

@[simp]
theorem mem_unitsPrimeTo_iff {J : Ideal A}
    {u : (FractionalIdeal A⁰ (FractionRing A))ˣ} :
    u ∈ unitsPrimeTo J ↔
      (u : FractionalIdeal A⁰ (FractionRing A)).IsPrimeTo J

Uses 2 · Used by 1

Statement usesFractional ideals prime to an ideal · Invertible fractional ideals prime to an ideal

Used byEvery invertible fractional ideal is prime to the unit ideal

TheoremPrime to an ideal implies prime to every larger ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(I\) be a fractional ideal of \(A\) in \(K\) and let \(J \subseteq J'\) be ideals of \(A\). If \(I\) is prime to \(J\), then \(I\) is prime to \(J'\).

theorem IsPrimeTo.mono {I : FractionalIdeal A⁰ (FractionRing A)}
    {J K : Ideal A} (hI : I.IsPrimeTo J) (hJK : J ≤ K) :
    I.IsPrimeTo K

Uses 1 · Used by 1

Statement usesFractional ideals prime to an ideal

Used byMonotonicity of the subgroups of units prime to an ideal

TheoremMonotonicity of the subgroups of units prime to an ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(J \subseteq J'\) be ideals of \(A\). Then the subgroup of invertible fractional ideals of \(A\) in \(K\) prime to \(J\) is contained in the subgroup of invertible fractional ideals of \(A\) in \(K\) prime to \(J'\).

theorem unitsPrimeTo_mono {J K : Ideal A} (hJK : J ≤ K) :
    unitsPrimeTo J ≤ unitsPrimeTo K

Uses 2

Statement usesInvertible fractional ideals prime to an ideal

Proof usesPrime to an ideal implies prime to every larger ideal

TheoremEvery invertible fractional ideal is prime to the unit ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\). The subgroup of invertible fractional ideals of \(A\) in \(K\) prime to the unit ideal \(A\) is the whole group of invertible fractional ideals of \(A\) in \(K\).

@[simp]
theorem unitsPrimeTo_top : unitsPrimeTo (⊤ : Ideal A) = ⊤

Uses 4

Statement usesInvertible fractional ideals prime to an ideal

Proof usesFractional ideals prime to an ideal · Membership in the subgroup of units prime to an ideal · Non-zero-divisors stay non-zero-divisors in a localization at a prime

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.