Documentation

TauCeti.RingTheory.DedekindDomain.FiniteAdeleRing.Away

Finite ideles and fractional ideals away from a finite set #

Let R be a Dedekind domain with fraction field K, and let S be a finite set of height one primes of R. The finite-idele valuation adicOrd records the multiplicity of every height one prime in the fractional ideal attached to a finite idele by FiniteAdeleRing.toFractionalIdeal. This file restricts that dictionary to the prime-to carrier NumberFieldArithmetic.idealsAway K S used by ray classes: vanishing of the orders on S is exactly membership in idealsAway K S, so the finite ideles that are local units at every place of S map onto idealsAway K S, with kernel the everywhere-integral units.

This is the fractional counterpart of TauCeti.toIntegralIdealsAway, which does the same for integral finite ideles and the integral prime-to monoid integralIdealsAway S. The two maps agree after passing from integral to fractional ideals, so adelic constructions can move between local valuations and the single prime-to ideal carrier, integrally or fractionally, without introducing a second notion of an ideal prime to S.

Main definitions #

Main results #

References #

source
theorem TauCeti.toFractionalIdeal_mem_idealsAway_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : (IsDedekindDomain.FiniteAdeleRing R K)หฃ) :
IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal x โˆˆ NumberFieldArithmetic.idealsAway K S โ†” โˆ€ v โˆˆ S, IsDedekindDomain.FiniteAdeleRing.adicOrd x v = 0

A finite idele defines an ideal away from S exactly when its orders vanish on S.

source
noncomputable def TauCeti.finiteIdelesAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) :
Subgroup (IsDedekindDomain.FiniteAdeleRing R K)หฃ

The finite ideles whose orders vanish at every place of S, that is, the finite ideles that are local units at every place of S.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_finiteIdelesAway_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : (IsDedekindDomain.FiniteAdeleRing R K)หฃ) :
    x โˆˆ finiteIdelesAway K S โ†” โˆ€ v โˆˆ S, IsDedekindDomain.FiniteAdeleRing.adicOrd x v = 0

    Membership in finiteIdelesAway K S means vanishing orders at every place of S.

    source
    noncomputable def TauCeti.toIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) :
    โ†ฅ(finiteIdelesAway K S) โ†’* โ†ฅ(NumberFieldArithmetic.idealsAway K S)

    The ideal away from S attached to a finite idele that is a local unit at every place of S.

    Instances For
      source
      @[simp]
      theorem TauCeti.coe_toIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : โ†ฅ(finiteIdelesAway K S)) :
      โ†‘((toIdealsAway K S) x) = IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal โ†‘x

      toIdealsAway is the restriction of the fractional-ideal map of finite ideles.

      source
      theorem TauCeti.ker_toIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) :
      (toIdealsAway K S).ker = Subgroup.comap (finiteIdelesAway K S).subtype (IsDedekindDomain.FiniteAdeleRing.integralUnits R K)

      The kernel of toIdealsAway consists of the everywhere-integral units.

      source
      @[simp]
      theorem TauCeti.toIdealsAway_eq_one_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : โ†ฅ(finiteIdelesAway K S)) :
      (toIdealsAway K S) x = 1 โ†” โ†‘x โˆˆ IsDedekindDomain.FiniteAdeleRing.integralUnits R K

      A finite idele that is a local unit on S defines the unit ideal exactly when it is an everywhere-integral unit.

      source
      @[simp]
      theorem TauCeti.toIdealsAway_eq_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x y : โ†ฅ(finiteIdelesAway K S)) :
      (toIdealsAway K S) x = (toIdealsAway K S) y โ†” โ†‘x / โ†‘y โˆˆ IsDedekindDomain.FiniteAdeleRing.integralUnits R K

      Two finite ideles that are local units on S define the same ideal away from S exactly when their quotient is an everywhere-integral unit.

      source
      theorem TauCeti.toIdealsAway_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) :
      Function.Surjective โ‡‘(toIdealsAway K S)

      Every fractional ideal away from S is the ideal of a finite idele that is a local unit at every place of S.

      source
      @[simp]
      theorem TauCeti.integralIdealsAwayHom_toIntegralIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (x : โ†ฅ(integralFiniteIdelesAway S)) :
      (NumberFieldArithmetic.integralIdealsAwayHom K S) ((toIntegralIdealsAway S) x) = (toIdealsAway K S) โŸจโ†‘โ†‘x, โ‹ฏโŸฉ

      Passing from integral to fractional prime-to ideals turns the integral finite-idele map toIntegralIdealsAway into toIdealsAway.