Fractional ideals away from finitely many primes

For a number field K and a finite set S of its finite places, this file defines the subgroup idealsAway S of invertible fractional ideals whose multiplicity vanishes at every member of S. It proves that this subgroup is generated by the prime ideals outside S, so that a homomorphism out of it is determined by its values on those primes, and supplies the inclusion induced by enlarging S.

The integral counterpart integralIdealsAway S consists of the nonzero integral ideals divisible by no prime in S, that is, the ideals that are Ideal.IsPrimeTo S. Its map to idealsAway S is the restriction of Mathlib's FractionalIdeal.mk0.

Generation comes from FractionalIdeal.mem_closure_unitOfPrime_of_count_eq_zero, the unit-level form of Mathlib's unique factorization of a nonzero fractional ideal.

Main definitions

• NumberFieldArithmetic.idealsAway: unit fractional ideals trivial at the primes in S.
• NumberFieldArithmetic.idealsAwayEmptyEquiv: ideals away from no primes are all invertible fractional ideals.
• NumberFieldArithmetic.idealsAwayInclusion: inclusion obtained from S ⊆ S'.
• NumberFieldArithmetic.integralIdealsAway: nonzero integral ideals prime to S.
• NumberFieldArithmetic.integralIdealsAwayHom: the map from integral to fractional ideals.

Main results

• NumberFieldArithmetic.idealsAway_eq_closure_primes: idealsAway S is generated by the primes outside S.
• NumberFieldArithmetic.idealsAway_hom_ext, NumberFieldArithmetic.integralIdealsAway_hom_ext: a monoid homomorphism out of idealsAway S or integralIdealsAway S is determined by its values on the primes outside S.

References

The unit-level factorization behind the generation statement is adapted from Michael Stoll's EllipticCurves/Mathlib/FractionalIdeal.lean at commit 66889eada51a of the MichaelStollBayreuth/EllipticCurves repository (Apache 2.0).

def TauCeti.NumberFieldArithmetic.idealsAway {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Subgroup (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

The subgroup of invertible fractional ideals whose multiplicity vanishes at every prime in S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.NumberFieldArithmetic.mem_idealsAway_iff {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ} : I ∈ idealsAway S ↔ ∀ v ∈ S, FractionalIdeal.count K v ↑I = 0

Membership in idealsAway S means vanishing multiplicity at every prime in S.

def TauCeti.NumberFieldArithmetic.idealsAwayEmptyEquiv {K : Type u_1} [Field K] [NumberField K] : ↥(idealsAway ∅) ≃* (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ

Ideals away from the empty set are canonically all invertible fractional ideals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.NumberFieldArithmetic.idealsAwayEmptyEquiv_apply {K : Type u_1} [Field K] [NumberField K] (I : ↥(idealsAway ∅)) : idealsAwayEmptyEquiv I = ↑I

The equivalence from ideals away from the empty set does not change the underlying fractional ideal unit.

@[simp]

theorem TauCeti.NumberFieldArithmetic.coe_idealsAwayEmptyEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ↑(idealsAwayEmptyEquiv.symm I) = I

The inverse equivalence regards every invertible fractional ideal as an ideal away from the empty set, without changing its underlying value.

theorem TauCeti.NumberFieldArithmetic.idealsAway_antitone {K : Type u_1} [Field K] [NumberField K] : Antitone idealsAway

Enlarging the excluded set of primes shrinks the group of fractional ideals away from it.

def TauCeti.NumberFieldArithmetic.idealsAwayInclusion {K : Type u_1} [Field K] [NumberField K] {S S' : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (h : S ⊆ S') : ↥(idealsAway S') →* ↥(idealsAway S)

The inclusion of fractional ideals away from S' into those away from S, for S ⊆ S'.

Equations

• TauCeti.NumberFieldArithmetic.idealsAwayInclusion h = Subgroup.inclusion ⋯

@[simp]

theorem TauCeti.NumberFieldArithmetic.coe_idealsAwayInclusion {K : Type u_1} [Field K] [NumberField K] {S S' : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (h : S ⊆ S') (I : ↥(idealsAway S')) : ↑((idealsAwayInclusion h) I) = ↑I

The inclusion between groups of ideals away from finite sets does not change the underlying fractional ideal.

theorem TauCeti.NumberFieldArithmetic.idealsAway_eq_closure_primes {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : idealsAway S = Subgroup.closure {I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ | ∃ v ∉ S, ↑I = ↑v.asIdeal}

idealsAway S is generated by the height-one prime ideals outside S.

theorem TauCeti.NumberFieldArithmetic.idealsAway_hom_ext {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [Monoid M] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {f g : ↥(idealsAway S) →* M} (h : ∀ (I : ↥(idealsAway S)), ∀ v ∉ S, ↑↑I = ↑v.asIdeal → f I = g I) : f = g

Homomorphisms out of idealsAway S are determined on the primes. Two monoid homomorphisms from the fractional ideals away from S agree as soon as they agree on every prime outside S.

def TauCeti.NumberFieldArithmetic.integralIdealsAway {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Submonoid (Ideal (NumberField.RingOfIntegers K))

The monoid of nonzero integral ideals divisible by no prime in S.

Equations

• TauCeti.NumberFieldArithmetic.integralIdealsAway S = { carrier := {I : Ideal (NumberField.RingOfIntegers K) | I.IsPrimeTo ↑S}, mul_mem' := ⋯, one_mem' := ⋯ }

theorem TauCeti.NumberFieldArithmetic.mem_integralIdealsAway_iff_isPrimeTo {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {I : Ideal (NumberField.RingOfIntegers K)} : I ∈ integralIdealsAway S ↔ I.IsPrimeTo ↑S

Membership in integralIdealsAway S is being prime to S.

@[simp]

theorem TauCeti.NumberFieldArithmetic.mem_integralIdealsAway_iff {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {I : Ideal (NumberField.RingOfIntegers K)} : I ∈ integralIdealsAway S ↔ I ≠ ⊥ ∧ ∀ v ∈ S, ¬v.asIdeal ∣ I

Membership in integralIdealsAway S is nonvanishing together with divisibility by no prime in S.

theorem TauCeti.NumberFieldArithmetic.integralIdealsAway_le_nonZeroDivisors {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : integralIdealsAway S ≤ nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))

The members of integralIdealsAway S are nonzero ideals.

@[instance_reducible]

instance TauCeti.NumberFieldArithmetic.instCancelCommMonoidSubtypeIdealRingOfIntegersMemSubmonoidIntegralIdealsAway {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : CancelCommMonoid ↥(integralIdealsAway S)

Members of integralIdealsAway S are nonzero ideals of a Dedekind domain, so they cancel.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.NumberFieldArithmetic.integralIdealsAway_hom_ext {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [MulOne M] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {f g : ↥(integralIdealsAway S) →* M} (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hv : v.asIdeal ∈ integralIdealsAway S), f ⟨v.asIdeal, hv⟩ = g ⟨v.asIdeal, hv⟩) : f = g

Homomorphisms out of integralIdealsAway S are determined on the primes. Two monoid homomorphisms from the integral ideals prime to S agree as soon as they agree on every prime outside S.

theorem TauCeti.NumberFieldArithmetic.integralIdealsAway_dvd_iff_dvd_coe {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {I J : ↥(integralIdealsAway S)} : I ∣ J ↔ ↑I ∣ ↑J

Divisibility in integralIdealsAway S is divisibility of the underlying ideals: a cofactor of two ideals prime to S is itself prime to S.

theorem TauCeti.NumberFieldArithmetic.mem_integralIdealsAway_iff_count_eq_zero {K : Type u_1} [Field K] [NumberField K] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {I : Ideal (NumberField.RingOfIntegers K)} : I ∈ integralIdealsAway S ↔ I ≠ ⊥ ∧ ∀ v ∈ S, FractionalIdeal.count K v ↑I = 0

Membership in integralIdealsAway S is equivalently nonvanishing and vanishing fractional ideal multiplicity at every prime in S.

noncomputable def TauCeti.NumberFieldArithmetic.integralIdealsAwayHom {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : ↥(integralIdealsAway S) →* ↥(idealsAway S)

Map a nonzero integral ideal away from S to its invertible fractional ideal.

Equations

• TauCeti.NumberFieldArithmetic.integralIdealsAwayHom S = ((FractionalIdeal.mk0 K).comp (Submonoid.inclusion ⋯)).codRestrict (TauCeti.NumberFieldArithmetic.idealsAway S) ⋯

@[simp]

theorem TauCeti.NumberFieldArithmetic.coe_integralIdealsAwayHom {K : Type u_1} [Field K] [NumberField K] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (I : ↥(integralIdealsAway S)) : ↑↑((integralIdealsAwayHom S) I) = ↑↑I

The integral-to-fractional map does not change the underlying ideal.