Documentation

TauCeti.NumberTheory.NumberField.Global.Orders.Gorenstein

Gorenstein orders and the trace dual #

For a nonzero fractional ideal I of an order O in a number field K, the trace dual Iᵛ = {x ∈ K | Tr_{K/ℚ}(x I) ⊆ ℤ} is again a nonzero fractional ideal of O, and Iᵛᵛ = I. The multiplier ring of I is the trace dual of I Iᵛ, so I is proper exactly when I Iᵛ = Oᵛ. The trace dual of the zero ideal is all of K, which is not fractional, so the packaged dual NumberFieldOrder.dual assigns the junk value 0 to the zero ideal.

The order O is Gorenstein when its trace dual Oᵛ, the codifferent, is an invertible fractional ideal. The criterion above then shows that a fractional ideal of a Gorenstein order is proper if and only if it is invertible. Conversely Oᵛ is always proper, so this equivalence characterizes Gorenstein orders.

The maximal order is Gorenstein, since all its nonzero fractional ideals are invertible. So is every monogenic order ℤ[x]: by Euler's formula its trace dual is generated by f'(x)⁻¹, where f is the minimal polynomial of x. In particular, every quadratic order is Gorenstein.

Main definitions #

Main results #

Implementation notes #

The underlying submodule of traceDual is Mathlib's Submodule.traceDual ℤ ℚ 1 (see coe_traceDual), so Mathlib's general trace-dual API applies to it directly.

References #

The trace dual of a fractional ideal #

source
theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isFractional_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) :
IsFractional (nonZeroDivisors ↥O.toSubalgebra) (Submodule.traceDual ℤ ℚ ↑I)

The trace dual of a nonzero fractional ideal of an order is a fractional ideal.

source
noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K

The trace dual (or complementary module) of an order O: the fractional ideal of x : K such that Tr_{K/ℚ}(xy) is an integer for every y ∈ O.

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    ↑O.traceDual = Submodule.traceDual ℤ ℚ 1
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_traceDual_iff {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : K) :
    x ∈ O.traceDual ↔ ∀ (y : ↥O.toSubalgebra), (Algebra.trace ℚ K) (x * ↑y) ∈ (algebraMap ℤ ℚ).range

    Membership in the trace dual means that the trace pairing against every element of the order is integral.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.one_le_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    1 ≤ O.traceDual

    The order, viewed as the unit fractional ideal, is contained in its trace dual.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.one_mem_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    1 ∈ O.traceDual

    The unit element belongs to the trace dual of every number-field order.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_ne_zero {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    O.traceDual ≠ 0

    The trace dual of an order is nonzero.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    Submodule.traceDual ℤ ℚ ↑O.traceDual = 1

    Taking the trace dual twice recovers the original order.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    O.multiplierRing O.traceDual = O.toSubalgebra.toSubring

    The multiplier ring of the trace dual is the order itself. Thus the trace dual is always a proper fractional ideal, whether or not it is invertible.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    O.IsProperFractionalIdeal O.traceDual

    The trace dual is a proper fractional ideal.

    source
    noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.dual {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
    FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K

    The trace dual Iᵛ = {x ∈ K | Tr_{K/ℚ}(x I) ⊆ ℤ} of a fractional ideal I of an order, as a fractional ideal. For I = 0 the trace dual is all of K, which is not fractional, and the junk value 0 is used instead.

    Instances For
      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_dual {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) :
      ↑(dual I) = Submodule.traceDual ℤ ℚ ↑I

      The trace dual of a nonzero fractional ideal is Mathlib's Submodule.traceDual over ℤ ⊆ ℚ.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_dual {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) {x : K} :
      x ∈ dual I ↔ ∀ y ∈ I, (Algebra.trace ℚ K) (x * y) ∈ (algebraMap ℤ ℚ).range

      An element lies in the trace dual of a nonzero fractional ideal I exactly when its products with the elements of I have integral trace.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_zero {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      dual 0 = 0

      The junk value of the trace dual at the zero ideal is zero.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_ne_zero {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) :
      dual I ≠ 0

      The trace dual of a nonzero fractional ideal is nonzero.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_eq_zero_iff {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} :
      dual I = 0 ↔ I = 0

      The trace dual of a fractional ideal vanishes exactly when the ideal does.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_dual {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
      dual (dual I) = I

      Trace duality is perfect: the trace dual of the trace dual of a fractional ideal of an order is the ideal itself.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_involutive {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      Function.Involutive dual

      The trace dual is an involution on the fractional ideals of an order.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_injective {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      Function.Injective dual

      The trace dual is injective on the fractional ideals of an order.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.dual_one_eq_traceDual {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      dual 1 = O.traceDual

      The trace dual of the unit fractional ideal agrees with the trace dual of the order.

      Proper ideals and the trace dual #

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_multiplierRing_iff_mem_dual {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : I ≠ 0) {x : K} :
      x ∈ O.multiplierRing I ↔ x ∈ dual (I * dual I)

      The multiplier ring of a nonzero fractional ideal I is the trace dual of I Iᵛ.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_iff_mul_dual_eq_dual_one {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} :
      O.IsProperFractionalIdeal I ↔ I * dual I = dual 1

      A fractional ideal I is proper exactly when I Iᵛ = Oᵛ.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_dual_one {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      O.IsProperFractionalIdeal (dual 1)

      The trace dual Oᵛ of an order, its codifferent, is a proper fractional ideal.

      Gorenstein orders #

      source
      structure TauCeti.GlobalNumberFields.NumberFieldOrder.IsGorenstein {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      Prop

      A number-field order is Gorenstein when its trace-dual fractional ideal is invertible.

      • isUnit_traceDual : IsUnit O.traceDual

        The trace dual of a Gorenstein order is invertible.

      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_iff {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        O.IsGorenstein ↔ IsUnit O.traceDual
        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.IsGorenstein.isUnit_of_isProperFractionalIdeal {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} (hO : O.IsGorenstein) {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : O.IsProperFractionalIdeal I) :
        IsUnit I

        In a Gorenstein order every proper fractional ideal is invertible.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_iff_isUnit_of_isGorenstein {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} (hO : O.IsGorenstein) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
        O.IsProperFractionalIdeal I ↔ IsUnit I

        In a Gorenstein order a fractional ideal is proper exactly when it is invertible.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_iff_forall_isUnit {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        O.IsGorenstein ↔ ∀ (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K), O.IsProperFractionalIdeal I → IsUnit I

        An order is Gorenstein exactly when all of its proper fractional ideals are invertible.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_of_isDedekindDomain {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) [IsDedekindDomain ↥O.toSubalgebra] :
        O.IsGorenstein

        An order that is a Dedekind domain is Gorenstein, since every nonzero fractional ideal of a Dedekind domain is invertible.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_maximalNumberFieldOrder {K : Type u} [Field K] [NumberField K] :
        (maximalNumberFieldOrder K).IsGorenstein

        The maximal order of a number field is Gorenstein.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.traceDual_eq_spanSingleton_of_toSubalgebra_eq_adjoin {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {x : K} (hx : O.toSubalgebra = ℤ[x]) :
        O.traceDual = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥O.toSubalgebra)) ((Polynomial.aeval x) (Polynomial.derivative (minpoly ℚ x)))⁻¹

        Euler's formula: the trace dual of a monogenic order ℤ[x] is generated by the inverse of the derivative of the minimal polynomial of x, evaluated at x.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_of_toSubalgebra_eq_adjoin {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {x : K} (hx : O.toSubalgebra = ℤ[x]) :
        O.IsGorenstein

        A monogenic order ℤ[x] is Gorenstein, since by Euler's formula its trace dual is principal.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isGorenstein_of_finrank_eq_two {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) (hK : Module.finrank ℚ K = 2) :
        O.IsGorenstein

        Every order in a quadratic number field is Gorenstein.