Documentation

TauCeti.NumberTheory.NumberField.Global.Orders.AwayConductor.Basic

Ideals of an order away from its conductor #

Let O be an order in a number field K with conductor ๐”ฃ. Extension I โ†ฆ I ๐“ž K and contraction J โ†ฆ J โˆฉ O are inverse monoid isomorphisms between the nonzero ideals of O coprime to ๐”ฃ and the nonzero ideals of ๐“ž K coprime to ๐”ฃ. On the maximal-order side the carrier is the integral prime-to monoid integralIdealsPrimeTo of the conductor viewed as a modulus, NumberFieldOrder.conductorModulus, the same monoid the ray class group is built on.

Every nonzero ideal of O coprime to ๐”ฃ is invertible, even though O need not be a Dedekind domain. These ideals therefore map injectively to the group of invertible fractional ideals of O, whose classes modulo principal ideals form the Picard group Pic O (via mkPic); they are the order-side ideals used to describe Pic O by ideals prime to the conductor. Here O is represented by its copy O.toRingOfIntegers inside ๐“ž K, and an ideal of O is coprime to ๐”ฃ when it is coprime to the contraction O.conductor.comap (O.toRingOfIntegers.val : O.toRingOfIntegers โ†’+* ๐“ž K) of ๐”ฃ to O. Every class of Pic O is the class of such an ideal, because that contraction is a nonzero ideal of O, so it has finite quotient and lies in only finitely many maximal ideals of O (ClassGroup.exists_mk_eq_and_sup_eq_top).

Main definitions #

Main results #

References #

The conductor as a modulus #

source
def TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
Modulus K

The conductor of an order as a modulus of K, with no real places. Its integral prime-to monoid consists of the nonzero ideals of ๐“ž K coprime to the conductor.

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus_finitePart {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    O.conductorModulus.finitePart = O.conductor
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus_infinitePart {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    O.conductorModulus.infinitePart = โˆ…
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus_maximalNumberFieldOrder {K : Type u_1} [Field K] [NumberField K] :
    (maximalNumberFieldOrder K).conductorModulus = Modulus.one K

    The conductor modulus of the maximal order is the trivial modulus.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.conductorModulus_dvd_conductorModulus {K : Type u_1} [Field K] [NumberField K] {O O' : NumberFieldOrder K} (h : O.toSubalgebra โ‰ค O'.toSubalgebra) :
    O'.conductorModulus โˆฃ O.conductorModulus

    Enlarging an order makes its conductor modulus a divisor of the conductor modulus of the smaller order.

    source
    theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_integralIdealsPrimeTo_conductorModulus_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {J : Ideal (NumberField.RingOfIntegers K)} :
    J โˆˆ integralIdealsPrimeTo O.conductorModulus โ†” J โ‰  โŠฅ โˆง J โŠ” O.conductor = โŠค

    An ideal of ๐“ž K is prime to the conductor modulus exactly when it is nonzero and coprime to the conductor.

    Ideals of the order coprime to the conductor #

    source
    def TauCeti.GlobalNumberFields.NumberFieldOrder.integralIdealsAwayConductor {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
    Submonoid (Ideal โ†ฅO.toRingOfIntegers)

    The monoid of nonzero ideals of an order coprime to its conductor. The order is represented by its copy O.toRingOfIntegers inside ๐“ž K, and the conductor by its contraction to it.

    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mem_integralIdealsAwayConductor_iff {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) {I : Ideal โ†ฅO.toRingOfIntegers} :
      I โˆˆ O.integralIdealsAwayConductor โ†” I โ‰  โŠฅ โˆง I โŠ” Ideal.comap (โ†‘O.toRingOfIntegers.val) O.conductor = โŠค
      source
      def TauCeti.GlobalNumberFields.NumberFieldOrder.integralIdealsAwayConductorEquiv {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
      โ†ฅO.integralIdealsAwayConductor โ‰ƒ* โ†ฅ(integralIdealsPrimeTo O.conductorModulus)

      Extension and contraction away from the conductor. Extending ideals from an order to ๐“ž K is a monoid isomorphism from the nonzero ideals of the order coprime to the conductor onto the nonzero ideals of ๐“ž K coprime to the conductor, whose inverse is contraction.

      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_integralIdealsAwayConductorEquiv_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : โ†ฅO.integralIdealsAwayConductor) :
        โ†‘(O.integralIdealsAwayConductorEquiv I) = Ideal.map โ†‘O.toRingOfIntegers.val โ†‘I

        The isomorphism integralIdealsAwayConductorEquiv extends an ideal of the order to ๐“ž K.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_integralIdealsAwayConductorEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (J : โ†ฅ(integralIdealsPrimeTo O.conductorModulus)) :
        โ†‘(O.integralIdealsAwayConductorEquiv.symm J) = Ideal.comap โ†‘O.toRingOfIntegers.val โ†‘J

        The inverse of integralIdealsAwayConductorEquiv contracts an ideal of ๐“ž K to the order.

        Invertibility #

        source
        theorem TauCeti.GlobalNumberFields.NumberFieldOrder.isUnit_coeIdeal_of_mem_integralIdealsAwayConductor {K : Type u_1} [Field K] [NumberField K] {O : NumberFieldOrder K} {I : Ideal โ†ฅO.toRingOfIntegers} (hI : I โˆˆ O.integralIdealsAwayConductor) :
        IsUnit โ†‘(Ideal.map O.toRingOfIntegersEquiv I)

        Ideals coprime to the conductor are invertible. A nonzero ideal of an order coprime to its conductor is an invertible fractional ideal of the order.

        source
        noncomputable def TauCeti.GlobalNumberFields.NumberFieldOrder.integralIdealsAwayConductorToInvertible {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
        โ†ฅO.integralIdealsAwayConductor โ†’* O.invertibleProperFractionalIdeals

        The invertible fractional ideal of an order attached to a nonzero ideal coprime to the conductor.

        Instances For
          source
          @[simp]
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.coe_integralIdealsAwayConductorToInvertible_apply {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) (I : โ†ฅO.integralIdealsAwayConductor) :
          โ†‘(O.integralIdealsAwayConductorToInvertible I) = โ†‘(Ideal.map O.toRingOfIntegersEquiv โ†‘I)

          The invertible fractional ideal attached to I is I itself, as a fractional ideal of the order.

          source
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.integralIdealsAwayConductorToInvertible_injective {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
          Function.Injective โ‡‘O.integralIdealsAwayConductorToInvertible

          Distinct ideals coprime to the conductor give distinct invertible fractional ideals.

          Picard classes away from the conductor #

          source
          theorem TauCeti.GlobalNumberFields.NumberFieldOrder.mkPic_comp_integralIdealsAwayConductorToInvertible_surjective {K : Type u_1} [Field K] [NumberField K] (O : NumberFieldOrder K) :
          Function.Surjective โ‡‘(O.mkPic.comp O.integralIdealsAwayConductorToInvertible)

          Every Picard class has a representative coprime to the conductor. Every class in the wide Picard group Pic O is the class of a nonzero ideal of O coprime to its conductor.