Invertible fractional ideals

TheoremThe multiplication dual is a colon quotient#✓fully proved

Let \(A\) be a commutative ring and \(K\) a field that is an \(A\)-algebra, and write \(1\) for the \(A\)-submodule \(A \cdot 1\) of \(K\). For every \(A\)-submodule \(M\) of \(K\), the dual submodule of \(M\) with respect to the multiplication form \((x, y) \mapsto xy\) on \(K\) equals the quotient \(1 / M\), the set of \(x \in K\) with \(xy \in A \cdot 1\) for all \(y \in M\).

theorem dualSubmodule_mul_eq_div (M : Submodule A K) :
    LinearMap.BilinForm.dualSubmodule (LinearMap.mul K K : LinearMap.BilinForm K K) M =
      (1 : Submodule A K) / M

TheoremFunctionals on a submodule of the fraction field are multiplications#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(M\) be a nonzero \(A\)-submodule of \(K\). For every \(A\)-linear map \(f \colon M \to A\) there is \(x \in K\) such that the image of \(f(m)\) in \(K\) equals \(xm\) for every \(m \in M\).

theorem Submodule.exists_mul_rep (M : Submodule A K) (hM : M ≠ ⊥)
    (f : Module.Dual A M) :
    ∃ x : K, ∀ m : M, algebraMap A K (f m) = x * m
Used by 1
Used byEvery functional comes from the multiplication dual

TheoremMultiplication is a nondegenerate bilinear form#✓fully proved

For every field \(K\), the \(K\)-bilinear form \((x, y) \mapsto xy\) on \(K\) is nondegenerate: if \(xy = 0\) for all \(y \in K\) then \(x = 0\), and if \(xy = 0\) for all \(x \in K\) then \(y = 0\).

theorem LinearMap.BilinForm.mul_nondegenerate :
    (LinearMap.mul K K : LinearMap.BilinForm K K).Nondegenerate
Used by 1
Used byDual of a nonzero submodule of the fraction field

TheoremA nonzero submodule spans the field#✓fully proved

Let \(A\) be a commutative ring and \(K\) a field that is an \(A\)-algebra. Then every nonzero \(A\)-submodule \(M\) of \(K\) spans \(K\) as a \(K\)-vector space.

theorem Submodule.span_coe_eq_top (M : Submodule A K) (hM : M ≠ ⊥) :
    Submodule.span K (M : Set K) = ⊤
Used by 1
Used byDual of a nonzero submodule of the fraction field

TheoremEvery functional comes from the multiplication dual#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), identify \(A\) with its image in \(K\), and let \(M\) be a nonzero \(A\)-submodule of \(K\). Let \(M^\vee = \{x \in K : xy \in A \text{ for all } y \in M\}\) be the dual submodule of \(M\) for the multiplication form \((x, y) \mapsto xy\) on \(K\). Then the \(A\)-linear map \(M^\vee \to \operatorname{Hom}_A(M, A)\) sending \(x\) to the functional \(y \mapsto xy\) on \(M\) is surjective.

theorem Submodule.mul_dualSubmoduleToDual_surjective (M : Submodule A K) (hM : M ≠ ⊥) :
    Function.Surjective (LinearMap.BilinForm.dualSubmoduleToDual
      (LinearMap.mul K K : LinearMap.BilinForm K K) M)
Uses 1 · Used by 1
Proof usesFunctionals on a submodule of the fraction field are multiplications
Used byDual of a nonzero submodule of the fraction field

DefinitionDual of a nonzero submodule of the fraction field#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), identify \(A\) with its image in \(K\), and let \(M\) be a nonzero \(A\)-submodule of \(K\). Let \(M^\vee = \{x \in K : xy \in A \text{ for all } y \in M\}\) be the dual submodule of \(M\) for the multiplication form \((x, y) \mapsto xy\) on \(K\). This is the \(A\)-linear isomorphism \(\operatorname{Hom}_A(M, A) \to M^\vee\) inverse to the map sending \(x \in M^\vee\) to the functional \(y \mapsto xy\) on \(M\); it sends \(f\) to the unique \(x \in M^\vee\) with \(f(y) = xy\) for all \(y \in M\).

noncomputable def Submodule.dualEquivMulDualSubmodule (M : Submodule A K) (hM : M ≠ ⊥) :
    Module.Dual A M ≃ₗ[A] LinearMap.BilinForm.dualSubmodule
      (LinearMap.mul K K : LinearMap.BilinForm K K) M :=
  (LinearEquiv.ofBijective (LinearMap.BilinForm.dualSubmoduleToDual
      (LinearMap.mul K K : LinearMap.BilinForm K K) M)
    ⟨LinearMap.BilinForm.dualSubmoduleToDual_injective _
      LinearMap.BilinForm.mul_nondegenerate M
      (Submodule.span_coe_eq_top M hM),
      Submodule.mul_dualSubmoduleToDual_surjective M hM⟩).symm
Uses 3 · Used by 2
Statement usesMultiplication is a nondegenerate bilinear form · Every functional comes from the multiplication dual · A nonzero submodule spans the field
Used byDual of a nonzero fractional ideal is its inverse · Formula for the isomorphism onto the multiplication dual

TheoremFormula for the isomorphism onto the multiplication dual#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(M\) be a nonzero \(A\)-submodule of \(K\), and let \(\varphi \colon \operatorname{Hom}_A(M, A) \to M^\vee\) be the isomorphism onto the dual submodule \(M^\vee\) of \(M\) for the multiplication form \((x, y) \mapsto xy\) on \(K\). Then for every \(f \in \operatorname{Hom}_A(M, A)\) and every \(m \in M\), the image of \(f(m)\) in \(K\) equals \(\varphi(f) \, m\).

theorem Submodule.dualEquivMulDualSubmodule_spec (M : Submodule A K) (hM : M ≠ ⊥)
    (f : Module.Dual A M) (m : M) :
    algebraMap A K (f m) = (Submodule.dualEquivMulDualSubmodule M hM f : K) * (m : K)
Uses 1
Statement usesDual of a nonzero submodule of the fraction field

TheoremThe inverse of a nonzero fractional ideal is its multiplication dual#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), and let \(I\) be a nonzero fractional ideal of \(A\) in \(K\). Then \(I^{-1}\), viewed as an \(A\)-submodule of \(K\), equals the dual submodule of \(I\) with respect to the multiplication form \((x, y) \mapsto xy\) on \(K\), namely the set \(\{x \in K : xy \in A \text{ for all } y \in I\}\), where \(A\) is identified with its image in \(K\).

theorem FractionalIdeal.coe_inv_eq_mul_dualSubmodule
    (I : FractionalIdeal A⁰ K) (hI : I ≠ 0) :
    ((I⁻¹ : FractionalIdeal A⁰ K) : Submodule A K) =
      LinearMap.BilinForm.dualSubmodule
        (LinearMap.mul K K : LinearMap.BilinForm K K)
        (I : Submodule A K)
Used by 1
Used byDual of a nonzero fractional ideal is its inverse

DefinitionDual of a nonzero fractional ideal is its inverse#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(I\) be a nonzero fractional ideal of \(A\) in \(K\). This is the \(A\)-linear isomorphism \(\operatorname{Hom}_A(I, A) \to I^{-1}\), with \(I^{-1}\) viewed as an \(A\)-submodule of \(K\), sending \(f\) to the unique \(x \in I^{-1}\) such that \(f(y) = xy\) in \(K\) for all \(y \in I\) (where \(A\) is identified with its image in \(K\)).

noncomputable def FractionalIdeal.dualEquivInv
    (I : FractionalIdeal A⁰ K) (hI : I ≠ 0) :
    Module.Dual A (I : Submodule A K) ≃ₗ[A]
      ((I⁻¹ : FractionalIdeal A⁰ K) : Submodule A K) := by
  have hM : (I : Submodule A K) ≠ ⊥ :=
    FractionalIdeal.coeToSubmodule_ne_bot.mpr hI
  exact (Submodule.dualEquivMulDualSubmodule (I : Submodule A K) hM).trans
    (LinearEquiv.ofEq _ _
      (FractionalIdeal.coe_inv_eq_mul_dualSubmodule I hI).symm)
Uses 2
Statement usesThe inverse of a nonzero fractional ideal is its multiplication dual · Dual of a nonzero submodule of the fraction field

DefinitionDouble dual of an invertible fractional ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\) and let \(I\) be an invertible fractional ideal of \(A\) in \(K\). This is the \(A\)-linear isomorphism \(\operatorname{Hom}_A(\operatorname{Hom}_A(I, A), A) \to I\) inverse to the canonical evaluation map \(I \to \operatorname{Hom}_A(\operatorname{Hom}_A(I, A), A)\), \(x \mapsto (f \mapsto f(x))\).

noncomputable def FractionalIdeal.doubleDualEquivOfIsUnit
    (I : FractionalIdeal A⁰ K) (hI : IsUnit I) :
    Module.Dual A (Module.Dual A (I : Submodule A K)) ≃ₗ[A]
      (I : Submodule A K) := by
  haveI : Module.Finite A (I : Submodule A K) :=
    Module.Finite.of_fg (FractionalIdeal.fg_of_isUnit I hI)
  have hcoe : IsUnit (I : Submodule A K) :=
    hI.map (FractionalIdeal.coeSubmoduleHom A⁰ K)
  haveI : Module.Projective A (I : Submodule A K) := by
    apply Submodule.projective_of_isUnit
    exact hcoe
  exact (Module.evalEquiv A (I : Submodule A K)).symm

LemmaLocalization commutes with division by a finitely generated submodule#✓fully proved

Let \(R\), \(S\) and \(K\) be commutative rings with algebra maps \(R \to S \to K\) forming a scalar tower, let \(p\) be a submonoid of \(R\) such that \(S\) is the localization of \(R\) at \(p\), and suppose the identity map of \(K\) is a localization of the \(R\)-module \(K\) at \(p\). For an \(R\)-submodule \(M\) of \(K\) write \(M_p = \{x/s : x \in M,\ s \in p\}\) for its localization, an \(S\)-submodule of \(K\), where \(x/s\) is the element \(y \in K\) with \(s y = x\). For submodules write \(M/N = \{x \in K : xN \subseteq M\}\). Then for \(R\)-submodules \(I\) and \(J\) of \(K\) with \(J\) finitely generated, \((I/J)_p = I_p/J_p\).

lemma localized'_div_of_fg (I J : Submodule R K) (hJ : J.FG) :
    (I / J).localized' S p (.id : K →ₗ[R] K) =
      I.localized' S p (.id : K →ₗ[R] K) /
        J.localized' S p (.id : K →ₗ[R] K)
Used by 1
Used byExtension to a localization commutes with division by a finitely generated ideal

LemmaExtension to a localization is localization#✓fully proved

Let \(A\) and \(B\) be integral domains with \(B\) a torsion-free \(A\)-algebra, and let \(K\) be a field that is a fraction field of both \(A\) and \(B\), compatibly with \(A \to B \to K\). Let \(S\) be a submonoid of \(A\) such that \(B\) is the localization of \(A\) at \(S\) and the identity map of \(K\) is a localization of the \(A\)-module \(K\) at \(S\). Then for every fractional ideal \(I\) of \(A\) in \(K\), the \(B\)-submodule of \(K\) underlying the extension of \(I\) to a fractional ideal of \(B\) (the \(B\)-submodule generated by \(I\)) equals the localization \(S^{-1}I = \{x/s : x \in I,\ s \in S\}\) of \(I\), viewed as a \(B\)-submodule of \(K\).

lemma coe_extendedHom_eq_localized' (S : Submonoid A) [IsLocalization S B]
    [IsLocalizedModule S (.id : K →ₗ[A] K)] (I : FractionalIdeal A⁰ K) :
    ((extendedHom K B I : FractionalIdeal B⁰ K) : Submodule B K) =
      (I : Submodule A K).localized' B S (.id : K →ₗ[A] K)
Used by 1
Used byExtension to a localization commutes with division by a finitely generated ideal

TheoremExtension to a localization commutes with division by a finitely generated ideal#✓fully proved

Let \(A\) and \(B\) be integral domains with \(B\) a torsion-free \(A\)-algebra, and let \(K\) be a field that is a fraction field of both \(A\) and \(B\), compatibly with \(A \to B \to K\). Let \(S\) be a submonoid of \(A\) such that \(B\) is the localization of \(A\) at \(S\). Let \(I\) and \(J\) be fractional ideals of \(A\) in \(K\) with \(J \ne 0\) and \(J\) finitely generated as an \(A\)-module, and write \(IB\) for the extension of \(I\) to a fractional ideal of \(B\). Then \((I/J)B = IB/JB\), where for a nonzero denominator the quotient of fractional ideals is \(I/J = \{x \in K : xJ \subseteq I\}\).

theorem extendedHom_div_of_fg (S : Submonoid A) [IsLocalization S B]
    (I J : FractionalIdeal A⁰ K) (hJ0 : J ≠ 0) (hJ : (J : Submodule A K).FG) :
    extendedHom K B (I / J) = extendedHom K B I / extendedHom K B J
Uses 2 · Used by 1
Proof usesExtension to a localization is localization · Localization commutes with division by a finitely generated submodule
Used byOver a Noetherian domain, extension to a localization commutes with division

TheoremOver a Noetherian domain, extension to a localization commutes with division#✓fully proved

Let \(A\) be a Noetherian integral domain, \(B\) an integral domain that is a torsion-free \(A\)-algebra, and \(K\) a field that is a fraction field of both \(A\) and \(B\), compatibly with \(A \to B \to K\). Let \(S\) be a submonoid of \(A\) such that \(B\) is the localization of \(A\) at \(S\). Let \(I\) and \(J\) be fractional ideals of \(A\) in \(K\) with \(J \ne 0\), and write \(IB\) for the extension of \(I\) to a fractional ideal of \(B\). Then \((I/J)B = IB/JB\), where for a nonzero denominator the quotient of fractional ideals is \(I/J = \{x \in K : xJ \subseteq I\}\).

theorem extendedHom_div [IsNoetherianRing A]
    (S : Submonoid A) [IsLocalization S B] (I J : FractionalIdeal A⁰ K) (hJ : J ≠ 0) :
    extendedHom K B (I / J) = extendedHom K B I / extendedHom K B J
Uses 1 · Used by 1
Proof usesExtension to a localization commutes with division by a finitely generated ideal
Used byLocalization commutes with inverting fractional ideals

TheoremInvertible fractional ideals of a Noetherian local domain are principal#✓fully proved

Let \(A\) be a Noetherian local integral domain with fraction field \(K\), and let \(I\) be a nonzero fractional ideal of \(A\) in \(K\). Then \(I\) is invertible if and only if \(I\) is principal.

theorem fractionalIdeal_isUnit_iff_isPrincipal
    (A : Type*) [CommRing A] [IsDomain A] [IsLocalRing A] [IsNoetherianRing A]
    (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
    (I : FractionalIdeal A⁰ K) (hI : I ≠ 0) :
    IsUnit I ↔ (I : Submodule A K).IsPrincipal
Sources
  • ATLAS NumberTheoryI, Section 3.1, Lemma 3.4.
Used by 1
Used byCorollary 3.5

DefinitionLocalization of a fractional ideal at a prime#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\), let \(\mathfrak p\) be a prime ideal of \(A\), and write \(A_{\mathfrak p}\) for the localization of \(A\) at \(\mathfrak p\). The localization \(I_{\mathfrak p}\) of a fractional ideal \(I\) of \(A\) in \(K\) is the fractional ideal of \(A_{\mathfrak p}\) in \(K\) obtained by extending \(I\) along \(A \to A_{\mathfrak p}\), that is, the \(A_{\mathfrak p}\)-submodule of \(K\) generated by \(I\).

noncomputable def localizeAtPrime
    (𝔪 : Ideal A) [𝔪.IsPrime]
    (I : FractionalIdeal A⁰ (FractionRing A)) :
    FractionalIdeal (Localization.AtPrime 𝔪)⁰ (FractionRing A) :=
  extendedHom (FractionRing A) (Localization.AtPrime 𝔪) I
Used by 6
Used byInverse of a localized fractional ideal is bounded by localization · Locally principal fractional ideal · Corollary 3.5 · Theorem 3.2 · Theorem 3.2 · Localization commutes with inverting fractional ideals

DefinitionLocally principal fractional ideal#✓fully proved

Let \(A\) be an integral domain with fraction field \(K\). For a maximal ideal \(\mathfrak m\) of \(A\), write \(A_{\mathfrak m}\) for the localization of \(A\) at \(\mathfrak m\) and \(I_{\mathfrak m}\) for the localization of a fractional ideal \(I\) of \(A\) in \(K\), the \(A_{\mathfrak m}\)-submodule of \(K\) generated by \(I\). A fractional ideal \(I\) of \(A\) in \(K\) is locally principal if for every maximal ideal \(\mathfrak m\) of \(A\) the localization \(I_{\mathfrak m}\), as an \(A_{\mathfrak m}\)-submodule of \(K\), is principal.

def IsLocallyPrincipal (I : FractionalIdeal A⁰ (FractionRing A)) : Prop :=
  ∀ (𝔪 : Ideal A) [𝔪.IsMaximal],
    ((I.localizeAtPrime 𝔪 :
      Submodule (Localization.AtPrime 𝔪) (FractionRing A)).IsPrincipal)
Uses 1 · Used by 1
Statement usesLocalization of a fractional ideal at a prime
Used byCorollary 3.5

TheoremLocalization commutes with inverting fractional ideals#✓fully proved

Localization commutes with inversion of fractional ideals.

@[simp] theorem localizeAtPrime_inv
    [IsNoetherianRing A]
    (𝔪 : Ideal A) [𝔪.IsPrime]
    (I : FractionalIdeal A⁰ (FractionRing A)) :
    localizeAtPrime 𝔪 (I⁻¹) = (localizeAtPrime 𝔪 I)⁻¹
Uses 2 · Used by 1
Statement usesLocalization of a fractional ideal at a prime
Proof usesOver a Noetherian domain, extension to a localization commutes with division
Used byInverse of a localized fractional ideal is bounded by localization

TheoremInverse of a localized fractional ideal is bounded by localization#✓fully proved

The inverse/localization inequality follows from equality.

theorem inv_localizeAtPrime_le
    [IsNoetherianRing A]
    (𝔪 : Ideal A) [𝔪.IsPrime]
    (I : FractionalIdeal A⁰ (FractionRing A)) :
    (localizeAtPrime 𝔪 I)⁻¹ ≤ localizeAtPrime 𝔪 (I⁻¹)
Uses 2 · Used by 1
Statement usesLocalization of a fractional ideal at a prime
Proof usesLocalization commutes with inverting fractional ideals
Used byTheorem 3.2

TheoremTheorem 3.2#✓fully proved

Theorem 3.2 (maximal-ideal form). A fractional ideal of a Noetherian domain is invertible iff its localization at every maximal ideal is invertible.

theorem isUnit_iff_isUnit_localizeAtPrime
    [IsNoetherianRing A]
    (I : FractionalIdeal A⁰ (FractionRing A)) :
    IsUnit I ↔ ∀ (𝔪 : Ideal A) [𝔪.IsMaximal], IsUnit (I.localizeAtPrime 𝔪)
Uses 2 · Used by 2
Statement usesLocalization of a fractional ideal at a prime
Proof usesInverse of a localized fractional ideal is bounded by localization
Used byCorollary 3.5 · Theorem 3.2

TheoremTheorem 3.2#✓fully proved

Theorem 3.2 (prime-ideal form). A fractional ideal of a Noetherian domain is invertible iff its localization at every prime ideal is invertible.

theorem isUnit_iff_isUnit_localizeAtPrime_all_primes
    [IsNoetherianRing A]
    (I : FractionalIdeal A⁰ (FractionRing A)) :
    IsUnit I ↔ ∀ (𝔭 : Ideal A) [𝔭.IsPrime], IsUnit (localizeAtPrime 𝔭 I)
Uses 2
Statement usesLocalization of a fractional ideal at a prime
Proof usesTheorem 3.2

TheoremCorollary 3.5#✓fully proved

A nonzero fractional ideal of a Noetherian domain is invertible iff it is locally principal.

theorem isUnit_iff_isLocallyPrincipal
    [IsNoetherianRing A]
    (I : FractionalIdeal A⁰ (FractionRing A)) (hI : I ≠ 0) :
    IsUnit I ↔ I.IsLocallyPrincipal
Uses 4
Statement usesLocally principal fractional ideal
Proof usesTheorem 3.2 · Localization of a fractional ideal at a prime · Invertible fractional ideals of a Noetherian local domain are principal
22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.