Documentation

TauCeti.NumberTheory.NumberField.Global.Orders.Basic

Orders in number fields #

An order in a number field K is a subalgebra over โ„ค that is finite as a โ„ค-module and spans K over โ„š. The spanning condition ensures that K is the fraction field of the order; this file installs that instance, so fractional ideals and Picard groups can be formed directly over an order.

Every order consists of algebraic integers, because module-finiteness implies integrality. Thus it embeds canonically in the maximal order ๐“ž K; in particular it is never the whole field. The maximal order itself is packaged as maximalNumberFieldOrder K.

Main definitions #

Main results #

References #

source
structure TauCeti.GlobalNumberFields.NumberFieldOrder (K : Type u) [Field K] [NumberField K] :
Type u

An order in a number field K: a subring containing โ„ค, finite as a โ„ค-module, whose โ„š-span is all of K.

Instances For
    source
    def TauCeti.GlobalNumberFields.NumberFieldOrder.ofIsFractionRing (R : Type u_1) (K : Type u) [CommRing R] [IsDomain R] [Field K] [NumberField K] [Module.Finite โ„ค R] [Algebra R K] [IsFractionRing R K] :
    NumberFieldOrder K

    A domain finite over โ„ค is an order in its fraction field when that field is a number field.

    Instances For
      source
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_ofIsFractionRing (R : Type u_1) (K : Type u) [CommRing R] [IsDomain R] [Field K] [NumberField K] [Module.Finite โ„ค R] [Algebra R K] [IsFractionRing R K] {x : K} :
      x โˆˆ (ofIsFractionRing R K).toSubalgebra โ†” โˆƒ (r : R), (algebraMap R K) r = x

      Membership in this order means being the image of an element of the original domain.

      source
      noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.ofIsFractionRingEquiv (R : Type u_1) (K : Type u) [CommRing R] [IsDomain R] [Field K] [NumberField K] [Module.Finite โ„ค R] [Algebra R K] [IsFractionRing R K] :
      R โ‰ƒ+* โ†ฅ(ofIsFractionRing R K).toSubalgebra

      A finite integer algebra is isomorphic to its image order in its fraction field.

      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_ofIsFractionRingEquiv (R : Type u_1) (K : Type u) [CommRing R] [IsDomain R] [Field K] [NumberField K] [Module.Finite โ„ค R] [Algebra R K] [IsFractionRing R K] (r : R) :
        โ†‘((ofIsFractionRingEquiv R K) r) = (algebraMap R K) r

        The order isomorphism sends each element to its image in the fraction field.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.ext {K : Type u} [Field K] [NumberField K] {O O' : NumberFieldOrder K} (h : O.toSubalgebra = O'.toSubalgebra) :
        O = O'

        Two orders in the same number field are equal when their underlying subalgebras are equal.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.ext_iff {K : Type u} [Field K] [NumberField K] {O O' : NumberFieldOrder K} :
        O = O' โ†” O.toSubalgebra = O'.toSubalgebra
        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isIntegral {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : โ†ฅO.toSubalgebra) :
        IsIntegral โ„ค โ†‘x

        Every element of an order is integral over โ„ค.

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.le_ringOfIntegers {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        O.toSubalgebra โ‰ค integralClosure โ„ค K

        Every order in a number field is contained in its ring of integers.

        source
        def TauCeti.GlobalNumberFields.NumberFieldOrder.toRingOfIntegers {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        Subalgebra โ„ค (NumberField.RingOfIntegers K)

        An order O, viewed as a โ„ค-subalgebra of the maximal order ๐“ž K.

        Instances For
          source
          @[simp]
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_toRingOfIntegers {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) {x : NumberField.RingOfIntegers K} :
          x โˆˆ O.toRingOfIntegers โ†” โ†‘x โˆˆ O.toSubalgebra

          An algebraic integer lies in the copy of O inside ๐“ž K exactly when it lies in O.

          source
          def TauCeti.GlobalNumberFields.NumberFieldOrder.toRingOfIntegersEquiv {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
          โ†ฅO.toRingOfIntegers โ‰ƒ+* โ†ฅO.toSubalgebra

          The copy O.toRingOfIntegers of an order inside ๐“ž K is isomorphic to the order itself. This moves ideals of the order between the two models: comparisons with ideals of ๐“ž K use the former, fractional ideals and Picard groups the latter.

          Instances For
            source
            @[simp]
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_toRingOfIntegersEquiv {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) (x : โ†ฅO.toRingOfIntegers) :
            โ†‘(O.toRingOfIntegersEquiv x) = โ†‘โ†‘x

            The isomorphism toRingOfIntegersEquiv does not change the underlying element of K.

            source
            @[simp]
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_toRingOfIntegersEquiv_symm {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) (y : โ†ฅO.toSubalgebra) :
            โ†‘โ†‘(O.toRingOfIntegersEquiv.symm y) = โ†‘y

            The inverse of toRingOfIntegersEquiv does not change the underlying element of K.

            source
            @[simp]
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.toRingOfIntegers_le_toRingOfIntegers_iff {K : Type u} [Field K] [NumberField K] {O O' : NumberFieldOrder K} :
            O.toRingOfIntegers โ‰ค O'.toRingOfIntegers โ†” O.toSubalgebra โ‰ค O'.toSubalgebra

            One order is contained in another exactly when their copies inside the maximal order are.

            source
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.toRingOfIntegers_injective {K : Type u} [Field K] [NumberField K] :
            Function.Injective toRingOfIntegers

            An order is determined by its copy inside the maximal order.

            source
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.toSubalgebra_ne_top {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
            O.toSubalgebra โ‰  โŠค

            An order is a proper subring of its number field.

            source
            instance TauCeti.GlobalNumberFields.NumberFieldOrder.isFractionRing {K : Type u} [Field K] [NumberField K] (O : NumberFieldOrder K) :
            IsFractionRing (โ†ฅO.toSubalgebra) K

            The ambient number field is the fraction field of each of its orders.

            Ideals of an order and of the maximal order #

            source
            theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_coeIdeal_map_toRingOfIntegersEquiv {K : Type u} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : Ideal โ†ฅO.toRingOfIntegers} {y : K} :
            y โˆˆ โ†‘(Ideal.map O.toRingOfIntegersEquiv I) โ†” โˆƒ x โˆˆ I, โ†‘โ†‘x = y

            An element of K lies in the fractional ideal of O attached to an ideal I of O.toRingOfIntegers exactly when it is an element of I.

            source
            theorem Ideal.restrictScalars_coeIdeal_map_toRingOfIntegersEquiv_mul_one {K : Type u} [Field K] [NumberField K] {O : TauCeti.GlobalNumberFields.NumberFieldOrder K} (I : Ideal โ†ฅO.toRingOfIntegers) :
            Submodule.restrictScalars โ„ค โ†‘โ†‘(map O.toRingOfIntegersEquiv I) * Submodule.restrictScalars โ„ค 1 = Submodule.restrictScalars โ„ค โ†‘โ†‘(map (โ†‘O.toRingOfIntegers.val) I)

            Over โ„ค, the product of an ideal I of the order with ๐“ž K is the extension of I to ๐“ž K.

            source
            def TauCeti.GlobalNumberFields.maximalNumberFieldOrder (K : Type u) [Field K] [NumberField K] :
            NumberFieldOrder K

            The maximal order of a number field, namely its ring of integers.

            Instances For
              source
              @[simp]
              theorem TauCeti.GlobalNumberFields.maximalNumberFieldOrder_toSubalgebra (K : Type u) [Field K] [NumberField K] :
              (maximalNumberFieldOrder K).toSubalgebra = integralClosure โ„ค K