Different and discriminant ideals

TheoremIdeals below the different#✓fully proved

Let \(A\) be an integrally closed domain with fraction field \(K\), let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\); assume that \(B\) is a Dedekind domain with fraction field \(L\) and is torsion-free as an \(A\)-module. Write \(B^\vee = \{x \in L : \operatorname{Tr}_{L/K}(xB) \subseteq A\}\) for the trace dual of \(B\) and \(\mathfrak{D}_{B/A}\) for the different ideal of \(B\) over \(A\). Then an ideal \(I\) of \(B\) satisfies \(I \subseteq \mathfrak{D}_{B/A}\) if and only if \(I B^\vee \subseteq B\), where the product is taken in the fractional ideals of \(B\) in \(L\).

theorem le_differentIdeal_iff_mul_dual_le_one (I : Ideal B) :
    I ≤ differentIdeal A B ↔
      (I : FractionalIdeal B⁰ L) * FractionalIdeal.dual A K
          (1 : FractionalIdeal B⁰ L) ≤ 1

TheoremThe trace dual commutes with localization#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\), a Dedekind domain with fraction field \(L\). Let \(S \subseteq A\) be a multiplicative set of nonzerodivisors, let \(A_S \subseteq K\) be the localization of \(A\) at \(S\) inside \(K\), and let \(B_S\) be a localization of \(B\) at the image of \(S\) that is also an \(A_S\)-algebra, with a map \(B_S \to L\) such that all composite maps from \(A\), \(A_S\), \(B\), \(B_S\) and \(K\) into \(L\) agree. Assume that \(B_S\) is a Dedekind domain with fraction field \(L\), torsion-free over \(B\), and the integral closure of \(A_S\) in \(L\). Write \(B^\vee = \{x \in L : \operatorname{Tr}_{L/K}(xB) \subseteq A\}\) and \(B_S^\vee = \{x \in L : \operatorname{Tr}_{L/K}(xB_S) \subseteq A_S\}\) for the trace duals. Then the fractional ideal of \(B_S\) generated by \(B^\vee\) is \(B_S^\vee\).

theorem extendedHom_dual_one_eq_dual_one_ofField :
    extendedHom L SB (dual A K (1 : FractionalIdeal (nonZeroDivisors B) L)) =
      dual Aₛ K (1 : FractionalIdeal (nonZeroDivisors SB) L)

Sources

• ATLAS N241, canonical-localization scope; transport to an arbitrary base localization is deferred.

Uses 1 · Used by 1

Proof usesDual submodules commute with localization

Used byThe different commutes with localization

TheoremThe different commutes with localization#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\), a Dedekind domain with fraction field \(L\) that is torsion-free as an \(A\)-module. Let \(S \subseteq A\) be a multiplicative set of nonzerodivisors, let \(A_S \subseteq K\) be the localization of \(A\) at \(S\) inside \(K\), and let \(B_S\) be a localization of \(B\) at the image of \(S\) that is also an \(A_S\)-algebra, with a map \(B_S \to L\) such that all composite maps from \(A\), \(A_S\), \(B\), \(B_S\) and \(K\) into \(L\) agree. Assume that \(B_S\) is a Dedekind domain with fraction field \(L\), torsion-free over \(A_S\) and over \(B\), and the integral closure of \(A_S\) in \(L\). Then the ideal of \(B_S\) generated by the image of the different ideal \(\mathfrak{D}_{B/A}\) is the different ideal \(\mathfrak{D}_{B_S/A_S}\).

theorem Ideal.map_differentIdeal_eq_localization_ofField [IsFractionRing B L] :
    Ideal.map (algebraMap B SB) (differentIdeal A B) = differentIdeal Aₛ SB

Sources

• ATLAS N241, canonical-localization scope; transport to an arbitrary base localization is deferred.

Uses 1 · Used by 1

Proof usesThe trace dual commutes with localization

Used byThe norm of the different commutes with localization

DefinitionDiscriminant ideal of a Dedekind extension#✓fully proved

Let \(A\) and \(B\) be Dedekind domains, with \(B\) an \(A\)-algebra that is finite and torsion-free as an \(A\)-module. The discriminant ideal \(\mathfrak{d}_{B/A}\) is the ideal of \(A\) generated by the norms \(N_{B/A}(x)\) of the elements \(x\) of the different ideal \(\mathfrak{D}_{B/A}\) of \(B\) over \(A\).

noncomputable def discriminantIdeal (A B : Type*) [CommRing A]
    [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [Module.IsTorsionFree A B] : Ideal A :=
  Ideal.spanNorm A (differentIdeal A B)

Used by 8

Used byAbsolute norm of the discriminant ideal of a number field · The discriminant ideal is the norm of the different · Tower formula for discriminant ideals · Height-one form of the discriminant ramification criterion · Not dividing the discriminant implies unramified at a prime · Unramified primes are those not dividing the discriminant · The discriminant commutes with localization · Unramified at a height-one prime implies not dividing discriminant

TheoremThe discriminant ideal is the norm of the different#✓fully proved

Let \(A\) and \(B\) be Dedekind domains, with \(B\) an \(A\)-algebra that is finite and torsion-free as an \(A\)-module. Then the discriminant ideal \(\mathfrak{d}_{B/A}\) is the ideal of \(A\) generated by the norms \(N_{B/A}(x)\) of the elements \(x\) of the different ideal \(\mathfrak{D}_{B/A}\) of \(B\) over \(A\); this holds by definition.

theorem discriminantIdeal_eq_spanNorm (A B : Type*) [CommRing A]
    [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [Module.IsTorsionFree A B] :
    discriminantIdeal A B = Ideal.spanNorm A (differentIdeal A B)

Uses 1 · Used by 3

Statement usesDiscriminant ideal of a Dedekind extension

Used byAbsolute norm of the discriminant ideal of a number field · Unramified primes are those not dividing the discriminant · The discriminant commutes with localization

TheoremTower formula for discriminant ideals#✓fully proved

Let \(A\), \(B\), \(C\) be Dedekind domains with algebra maps \(A \to B \to C\) whose composite is the algebra map \(A \to C\), such that \(B\) is finite and torsion-free over \(A\), \(C\) is finite and torsion-free over \(A\) and over \(B\), and the fraction field of \(C\) is separable over the fraction field of \(A\). Write \(\mathfrak{d}_{B/A}\), \(\mathfrak{d}_{C/A}\) and \(\mathfrak{d}_{C/B}\) for the discriminant ideals of \(B\) over \(A\), of \(C\) over \(A\) and of \(C\) over \(B\), let \(n = [\operatorname{Frac} C : \operatorname{Frac} B]\), and for an ideal \(I\) of \(B\) let \(N_{B/A}(I)\) be the ideal of \(A\) generated by the norms of the elements of \(I\). Then \(\mathfrak{d}_{C/A} = \mathfrak{d}_{B/A}^{\,n} \, N_{B/A}(\mathfrak{d}_{C/B})\).

theorem discriminantIdeal_tower (A B C : Type*) [CommRing A]
    [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [CommRing C]
    [IsDedekindDomain C] [Algebra A B] [Algebra B C] [Algebra A C]
    [IsScalarTower A B C] [Module.Finite A B] [Module.Finite A C]
    [Module.Finite B C] [Module.IsTorsionFree A B]
    [Module.IsTorsionFree A C] [Module.IsTorsionFree B C]
    [Algebra.IsSeparable (FractionRing A) (FractionRing C)] :
    discriminantIdeal A C =
      (discriminantIdeal A B) ^
          Module.finrank (FractionRing B) (FractionRing C) *
        Ideal.spanNorm A (discriminantIdeal B C)

Sources

• ATLAS NumberTheoryI Proposition 12.28, second half.

Uses 1

Statement usesDiscriminant ideal of a Dedekind extension

TheoremThe norm of the different commutes with localization#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\), a Dedekind domain with fraction field \(L\) that is finite and torsion-free as an \(A\)-module. Let \(S \subseteq A\) be a multiplicative set of nonzerodivisors, let \(A_S \subseteq K\) be the localization of \(A\) at \(S\) inside \(K\), and let \(B_S\) be a localization of \(B\) at the image of \(S\) that is also an \(A\)-algebra and an \(A_S\)-algebra, with a map \(B_S \to L\), such that all composite maps among \(A\), \(A_S\), \(B\), \(B_S\), \(K\) and \(L\) agree. Assume that \(B_S\) is a Dedekind domain with fraction field \(L\), finite and torsion-free over \(A_S\), torsion-free over \(B\), and the integral closure of \(A_S\) in \(L\). For an extension \(R \to T\) of Dedekind domains, write \(\mathfrak{D}_{T/R}\) for its different ideal and, for an ideal \(I\) of \(T\), write \(N_{T/R}(I)\) for the ideal of \(R\) generated by the norms of the elements of \(I\). Then the ideal of \(A_S\) generated by the image of \(N_{B/A}(\mathfrak{D}_{B/A})\) is \(N_{B_S/A_S}(\mathfrak{D}_{B_S/A_S})\).

theorem Ideal.map_spanNorm_differentIdeal_eq_localization_ofField [IsFractionRing B L] :
    Ideal.map (algebraMap A Aₛ) (Ideal.spanNorm A (differentIdeal A B)) =
      Ideal.spanNorm Aₛ (differentIdeal Aₛ SB)

Sources

• ATLAS NumberTheoryI Proposition 12.15 (norm-of-the-different form), canonical-localization scope; transport to an arbitrary base localization is deferred.

Uses 1 · Used by 1

Proof usesThe different commutes with localization

Used byThe discriminant commutes with localization

TheoremThe discriminant commutes with localization#✓fully proved

Let \(A\) be a Dedekind domain with fraction field \(K\), let \(L/K\) be a finite separable extension, and let \(B\) be the integral closure of \(A\) in \(L\), a Dedekind domain with fraction field \(L\) that is finite and torsion-free as an \(A\)-module. Let \(S \subseteq A\) be a multiplicative set of nonzerodivisors, let \(A_S \subseteq K\) be the localization of \(A\) at \(S\) inside \(K\), and let \(B_S\) be a localization of \(B\) at the image of \(S\) that is also an \(A\)-algebra and an \(A_S\)-algebra, with a map \(B_S \to L\), such that all composite maps among \(A\), \(A_S\), \(B\), \(B_S\), \(K\) and \(L\) agree. Assume that \(B_S\) is a Dedekind domain with fraction field \(L\), finite and torsion-free over \(A_S\), torsion-free over \(B\), and the integral closure of \(A_S\) in \(L\). Write \(\mathfrak{d}_{B/A}\) and \(\mathfrak{d}_{B_S/A_S}\) for the discriminant ideals of \(B\) over \(A\) and of \(B_S\) over \(A_S\). Then the ideal of \(A_S\) generated by the image of \(\mathfrak{d}_{B/A}\) is \(\mathfrak{d}_{B_S/A_S}\).

theorem Ideal.map_discriminantIdeal_eq_localization_ofField [IsFractionRing B L] :
    Ideal.map (algebraMap A Aₛ) (Ideal.discriminantIdeal A B) =
      Ideal.discriminantIdeal Aₛ SB

Sources

• ATLAS NumberTheoryI Proposition 12.15, canonical-localization scope; transport to an arbitrary base localization is deferred.

Uses 3

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesThe discriminant ideal is the norm of the different · The norm of the different commutes with localization

DefinitionElement different#✓fully proved

Let \(A\) be a commutative ring, \(B\) a commutative \(A\)-algebra, \(L\) a field that is a \(B\)-algebra, and \(K\) a field with \(L\) a \(K\)-algebra. For \(\alpha \in B\), let \(f \in A[X]\) be the minimal polynomial of \(\alpha\) over \(A\) (taken to be \(0\) when \(\alpha\) is not integral over \(A\)). The element different \(\delta_{B/A}(\alpha) \in B\) is \(f'(\alpha)\) when the image of \(\alpha\) in \(L\) generates \(L\) as a \(K\)-algebra, and \(0\) otherwise.

noncomputable def elementDifferent (α : B) : B :=
  if Algebra.adjoin K {algebraMap B L α} = ⊤ then
    Polynomial.aeval α (Polynomial.derivative (minpoly A α))
  else 0

Used by 4

Used byVanishing of the element different · The element different lies in the different · Element different of a generator · Element different of a non-generator

TheoremElement different of a generator#✓fully proved

Let \(A\) be a commutative ring, \(B\) a commutative \(A\)-algebra, \(L\) a field that is a \(B\)-algebra, and \(K\) a field with \(L\) a \(K\)-algebra. Let \(\alpha \in B\) and let \(f\) be the minimal polynomial of \(\alpha\) over \(A\) (taken to be \(0\) when \(\alpha\) is not integral over \(A\)). If the image of \(\alpha\) in \(L\) generates \(L\) as a \(K\)-algebra, then the element different \(\delta_{B/A}(\alpha)\) equals \(f'(\alpha)\).

@[simp]
theorem elementDifferent_of_adjoin_eq_top (α : B)
    (hα : Algebra.adjoin K {algebraMap B L α} = ⊤) :
    elementDifferent A K L α =
      Polynomial.aeval α (Polynomial.derivative (minpoly A α))

Uses 1 · Used by 1

Statement usesElement different

Used byThe element different lies in the different

TheoremElement different of a non-generator#✓fully proved

Let \(A\) be a commutative ring, \(B\) a commutative \(A\)-algebra, \(L\) a field that is a \(B\)-algebra, and \(K\) a field with \(L\) a \(K\)-algebra. If \(\alpha \in B\) and the image of \(\alpha\) in \(L\) does not generate \(L\) as a \(K\)-algebra, then the element different \(\delta_{B/A}(\alpha)\) is \(0\).

@[simp]
theorem elementDifferent_of_adjoin_ne_top (α : B)
    (hα : Algebra.adjoin K {algebraMap B L α} ≠ ⊤) :
    elementDifferent A K L α = 0

Uses 1

Statement usesElement different

TheoremVanishing of the element different#✓fully proved

Let \(A\) be a commutative ring, \(B\) a commutative \(A\)-algebra, \(L\) a field that is a \(B\)-algebra, and \(K\) a field with \(L\) a \(K\)-algebra. Let \(\alpha \in B\) and let \(f\) be the minimal polynomial of \(\alpha\) over \(A\) (taken to be \(0\) when \(\alpha\) is not integral over \(A\)). Then the element different \(\delta_{B/A}(\alpha)\) is \(0\) if and only if the image of \(\alpha\) in \(L\) does not generate \(L\) as a \(K\)-algebra or \(f'(\alpha) = 0\).

theorem elementDifferent_eq_zero_iff (α : B) :
    elementDifferent A K L α = 0 ↔
      Algebra.adjoin K {algebraMap B L α} ≠ ⊤ ∨
        Polynomial.aeval α (Polynomial.derivative (minpoly A α)) = 0

Uses 1

Statement usesElement different

TheoremThe element different lies in the different#✓fully proved

Let \(A\) be an integrally closed domain with fraction field \(K\), let \(L\) be a finite separable extension of \(K\), and let \(B\) be the integral closure of \(A\) in \(L\), assumed to be a Dedekind domain with fraction field \(L\) that is torsion-free as an \(A\)-module, with compatible algebra maps \(A \to K \to L\) and \(A \to B \to L\). If \(\alpha \in B\) and the image of \(\alpha\) in \(L\) generates \(L\) as a \(K\)-algebra, then the element different \(\delta_{B/A}(\alpha)\) lies in the different ideal \(\mathfrak{D}_{B/A}\) of \(B\) over \(A\).

theorem elementDifferent_mem_differentIdeal
    [Algebra A K] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L]
    [IsDomain A] [IsFractionRing A K]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L]
    [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B]
    [Module.IsTorsionFree A B]
    (α : B) (hα : Algebra.adjoin K {algebraMap B L α} = ⊤) :
    elementDifferent A K L α ∈ differentIdeal A B

Uses 2

Statement usesElement different

Proof usesElement different of a generator

TheoremThe different of a monogenic extension#✓fully proved

Let \(A\) be an integrally closed domain with fraction field \(K\), let \(L\) be a finite separable extension of \(K\), and let \(B\) be the integral closure of \(A\) in \(L\), assumed to be a Dedekind domain with fraction field \(L\) that is torsion-free as an \(A\)-module, with compatible algebra maps \(A \to K \to L\) and \(A \to B \to L\). If \(\alpha \in B\) generates \(B\) as an \(A\)-algebra, that is \(B = A[\alpha]\), and \(f\) is the minimal polynomial of \(\alpha\) over \(A\), then the different ideal \(\mathfrak{D}_{B/A}\) is the principal ideal \((f'(\alpha))\) of \(B\).

theorem differentIdeal_eq_span_derivative_of_adjoin_eq_top
    [Algebra A K] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L]
    [IsDomain A] [IsFractionRing A K]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L]
    [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B]
    [Module.IsTorsionFree A B]
    (α : B) (hα : Algebra.adjoin A {α} = ⊤) :
    differentIdeal A B =
      Ideal.span {Polynomial.aeval α (Polynomial.derivative (minpoly A α))}

Sources

• Andrew V. Sutherland, 18.785 Number Theory I, Lecture 12, Proposition 12.24.

TheoremOnly finitely many primes of the extension ramify#✓fully proved

Let \(A\) and \(B\) be Dedekind domains, where \(B\) is an \(A\)-algebra that is finitely generated and torsion-free as an \(A\)-module and the field of fractions of \(B\) is separable over the field of fractions of \(A\). Then only finitely many nonzero prime ideals \(\mathfrak P\) of \(B\) are ramified over \(A\). Here \(\mathfrak P\) is unramified over \(A\) when the localization \(B_{\mathfrak P}\) is formally unramified over \(A\).

theorem Ideal.finite_ramified_primes :
    {P : HeightOneSpectrum B | ¬ Algebra.IsUnramifiedAt A P.asIdeal}.Finite

Sources

• ATLAS NumberTheoryI Corollary 12.20, the statement for primes of \(B\).

Used by 1

Used byOnly finitely many primes of the base ramify

TheoremOnly finitely many primes of the base ramify#✓fully proved

Let \(A\) and \(B\) be Dedekind domains, where \(B\) is an \(A\)-algebra that is finitely generated and torsion-free as an \(A\)-module and the field of fractions of \(B\) is separable over the field of fractions of \(A\). Then only finitely many nonzero prime ideals \(\mathfrak p\) of \(A\) are ramified in \(B\). Here \(\mathfrak p\) is unramified in \(B\) when every prime ideal \(\mathfrak P\) of \(B\) lying over \(\mathfrak p\) is unramified over \(A\), that is, the localization \(B_{\mathfrak P}\) is formally unramified over \(A\).

theorem Ideal.finite_ramified_primes_below :
    {p : HeightOneSpectrum A | ¬ Algebra.IsUnramifiedIn B p.asIdeal}.Finite

Sources

• ATLAS NumberTheoryI Corollary 12.20, the statement for primes of \(A\).

Uses 1

Proof usesOnly finitely many primes of the extension ramify

TheoremUnramified primes are those not dividing the discriminant#✓fully proved

Theorem 12.19, discriminant half, in Mathlib's standard predicate: 𝔭 is unramified in B exactly when it does not divide the discriminant ideal.

theorem isUnramifiedIn_iff_not_dvd_discriminantIdeal
    (𝔭 : IsDedekindDomain.HeightOneSpectrum A) :
    Algebra.IsUnramifiedIn B 𝔭.asIdeal ↔
      ¬ (𝔭.asIdeal ∣ discriminantIdeal A B)

Uses 2 · Used by 3

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesThe discriminant ideal is the norm of the different

Used byHeight-one form of the discriminant ramification criterion · Not dividing the discriminant implies unramified at a prime · Unramified at a height-one prime implies not dividing discriminant

TheoremUnramified at a height-one prime implies not dividing discriminant#✓fully proved

Height-one compatibility: derive nondivisibility from the standard unramified-in criterion after converting the original height-one premise.

theorem not_dvd_discriminantIdeal_of_isUnramifiedAt
    (𝔭 : IsDedekindDomain.HeightOneSpectrum A)
    (hall : ∀ 𝔮 : IsDedekindDomain.HeightOneSpectrum B, 𝔮.asIdeal.LiesOver 𝔭.asIdeal →
      Algebra.IsUnramifiedAt A 𝔮.asIdeal) :
    ¬ (𝔭.asIdeal ∣ discriminantIdeal A B)

Uses 2

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesUnramified primes are those not dividing the discriminant

TheoremNot dividing the discriminant implies unramified at a prime#✓fully proved

Height-one compatibility: evaluate the standard unramified-in conclusion at the particular height-one prime supplied by an original client.

theorem isUnramifiedAt_of_not_dvd_discriminantIdeal
    (𝔭 : IsDedekindDomain.HeightOneSpectrum A)
    (hndvd : ¬ (𝔭.asIdeal ∣ discriminantIdeal A B))
    (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (hlies : 𝔮.asIdeal.LiesOver 𝔭.asIdeal) :
    Algebra.IsUnramifiedAt A 𝔮.asIdeal

Uses 2

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesUnramified primes are those not dividing the discriminant

TheoremHeight-one form of the discriminant ramification criterion#✓fully proved

The original height-one formulation, derived from the standard primary criterion.

theorem isUnramifiedAt_iff_not_dvd_discriminantIdeal
    (𝔭 : IsDedekindDomain.HeightOneSpectrum A) :
    (∀ 𝔮 : IsDedekindDomain.HeightOneSpectrum B, 𝔮.asIdeal.LiesOver 𝔭.asIdeal →
      Algebra.IsUnramifiedAt A 𝔮.asIdeal) ↔
    ¬ (𝔭.asIdeal ∣ discriminantIdeal A B)

Uses 2

Statement usesDiscriminant ideal of a Dedekind extension

Proof usesUnramified primes are those not dividing the discriminant

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.