Documentation

TauCeti.NumberTheory.NumberField.Global.Orders.ProperIdeal

Proper fractional ideals of a number-field order #

The multiplier ring of a fractional ideal consists of the field elements preserving that ideal under multiplication. A fractional ideal is proper when its multiplier ring is exactly the order. An invertible fractional ideal is proper; the converse can fail for non-Gorenstein orders.

This distinction is needed when forming the Picard group from invertible ideals while keeping noninvertible proper ideals in the ideal class monoid.

References #

source
def TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
Subring K

The subring of K consisting of elements that preserve a fractional O-ideal under multiplication.

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_multiplierRing_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) (x : K) :
    x ∈ O.multiplierRing I ↔ ∀ y ∈ I, x * y ∈ I

    Membership in the multiplier ring means preservation of every element of the ideal.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.order_le_multiplierRing {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
    O.toSubalgebra.toSubring ≤ O.multiplierRing I

    The order acts on each of its fractional ideals, so it lies in the multiplier ring.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing_le_multiplierRing_mul {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I J : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
    O.multiplierRing I ≤ O.multiplierRing (I * J)

    An element preserving I also preserves every product I * J.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing_mul_isUnit {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I J : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) (hJ : IsUnit J) :
    O.multiplierRing (I * J) = O.multiplierRing I

    Multiplication by an invertible fractional ideal preserves the multiplier ring.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing_mul_spanSingleton {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) {x : K} (hx : x ≠ 0) :
    O.multiplierRing (I * (FractionalIdeal.spanSingleton (nonZeroDivisors ↥O.toSubalgebra)) x) = O.multiplierRing I

    Scaling a fractional ideal by a nonzero field element preserves its multiplier ring.

    source
    def TauCeti.GlobalNumberFields.NumberFieldOrder.IsProperFractionalIdeal {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
    Prop

    A fractional ideal is proper when its multiplier ring equals the order.

    Instances For
      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_def {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
      O.IsProperFractionalIdeal I ↔ O.multiplierRing I = O.toSubalgebra.toSubring

      Properness is equality of the multiplier ring with the order.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.multiplierRing_zero {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      O.multiplierRing 0 = ⊤

      Every field element preserves the zero ideal, so its multiplier ring is the whole field.

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

      A proper fractional ideal is nonzero, so proper ideals enter the monoid of nonzero fractional ideals without a separate nonvanishing hypothesis.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) :
      O.IsProperFractionalIdeal I ↔ ∀ (x : K), (∀ y ∈ I, x * y ∈ I) → x ∈ O.toSubalgebra

      Properness says exactly that any field element stabilizing the ideal belongs to the order.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_mul_isUnit {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I J : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) (hJ : IsUnit J) :
      O.IsProperFractionalIdeal (I * J) ↔ O.IsProperFractionalIdeal I

      Properness is unchanged by multiplication by an invertible fractional ideal.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_mul_spanSingleton {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K) {x : K} (hx : x ≠ 0) :
      O.IsProperFractionalIdeal (I * (FractionalIdeal.spanSingleton (nonZeroDivisors ↥O.toSubalgebra)) x) ↔ O.IsProperFractionalIdeal I

      Properness is unchanged by nonzero principal scaling.

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

      The unit fractional ideal has precisely the order as its multiplier ring.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_one {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      O.IsProperFractionalIdeal 1

      The unit fractional ideal is proper.

      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_of_isUnit {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hI : IsUnit I) :
      O.IsProperFractionalIdeal I

      Units of the fractional-ideal monoid, namely invertible fractional ideals, are proper.

      source
      @[reducible, inline]
      abbrev TauCeti.GlobalNumberFields.NumberFieldOrder.invertibleProperFractionalIdeals {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      Type u_1

      The group of invertible fractional ideals of an order. Its elements are proper fractional ideals, by NumberFieldOrder.isProperFractionalIdeal_of_isUnit.

      Instances For
        source
        @[reducible, inline]
        abbrev TauCeti.GlobalNumberFields.NumberFieldOrder.properFractionalIdeals {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        Type u_1

        The proper fractional ideals of an order. Every invertible fractional ideal is proper, but for a non-Gorenstein order some proper fractional ideals are not invertible, so this carrier is larger than NumberFieldOrder.invertibleProperFractionalIdeals.

        Instances For
          source
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.invertible_isProper {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : O.invertibleProperFractionalIdeals) :
          O.IsProperFractionalIdeal ↑I

          Every invertible fractional ideal of an order is proper.

          source
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isProperFractionalIdeal_of_mul_eq_one {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I J : FractionalIdeal (nonZeroDivisors ↥O.toSubalgebra) K} (hIJ : I * J = 1) :
          O.IsProperFractionalIdeal I

          A fractional ideal with a multiplicative inverse is proper.