Fractional ideals away from finitely many primes

For a Dedekind domain R with fraction field K and a finite set S of height-one primes, this file defines the subgroup idealsAway K 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 K S is the restriction of Mathlib's FractionalIdeal.mk0. Every fractional ideal away from S is a quotient of two such integral ideals, and integralIdealsAwayLocalizationMap packages this as the universal property of localization at all elements of the integral monoid.

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 K S is generated by the primes outside S.
• NumberFieldArithmetic.idealsAway_hom_ext, NumberFieldArithmetic.integralIdealsAway_hom_ext: a monoid homomorphism out of idealsAway K S or integralIdealsAway S is determined by its values on the primes outside S.
• NumberFieldArithmetic.exists_integralIdealsAway_div: every fractional ideal away from S has an integral numerator and denominator away from S.
• NumberFieldArithmetic.integralIdealsAwayLocalizationMap: the fractional ideal group is the localization of the integral ideal monoid at all of its elements.

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 {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 (FractionalIdeal (nonZeroDivisors R) K)ˣ

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

@[simp]

theorem TauCeti.NumberFieldArithmetic.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)} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} : I ∈ idealsAway K S ↔ ∀ v ∈ S, FractionalIdeal.count K v ↑I = 0

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

theorem TauCeti.NumberFieldArithmetic.notMem_of_coe_eq_asIdeal {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)} {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ} (hI : I ∈ idealsAway K S) {v : IsDedekindDomain.HeightOneSpectrum R} (h : ↑I = ↑v.asIdeal) : v ∉ S

A prime ideal that is an element of idealsAway K S is not in S: it has multiplicity one at itself, while the elements of idealsAway K S have multiplicity zero on S.

def TauCeti.NumberFieldArithmetic.idealsAwayEmptyEquiv {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : ↥(idealsAway K ∅) ≃* (FractionalIdeal (nonZeroDivisors R) K)ˣ

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

@[simp]

theorem TauCeti.NumberFieldArithmetic.idealsAwayEmptyEquiv_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : ↥(idealsAway K ∅)) : (idealsAwayEmptyEquiv K) 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 {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : ↑((idealsAwayEmptyEquiv K).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 {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Antitone (idealsAway K)

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

def TauCeti.NumberFieldArithmetic.idealsAwayInclusion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {S S' : Finset (IsDedekindDomain.HeightOneSpectrum R)} (h : S ⊆ S') : ↥(idealsAway K S') →* ↥(idealsAway K S)

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

@[simp]

theorem TauCeti.NumberFieldArithmetic.coe_idealsAwayInclusion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {S S' : Finset (IsDedekindDomain.HeightOneSpectrum R)} (h : S ⊆ S') (I : ↥(idealsAway K S')) : ↑((idealsAwayInclusion K 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 {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)) : idealsAway K S = Subgroup.closure {I : (FractionalIdeal (nonZeroDivisors R) K)ˣ | ∃ v ∉ S, ↑I = ↑v.asIdeal}

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

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

Homomorphisms out of idealsAway K 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 {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : Submonoid (Ideal R)

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

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

Membership in integralIdealsAway S is being prime to S.

@[simp]

theorem TauCeti.NumberFieldArithmetic.mem_integralIdealsAway_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {I : Ideal R} : 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 {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : integralIdealsAway S ≤ nonZeroDivisors (Ideal R)

The members of integralIdealsAway S are nonzero ideals.

@[instance_reducible]

instance TauCeti.NumberFieldArithmetic.instCancelCommMonoidSubtypeIdealMemSubmonoidIntegralIdealsAway {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) : CancelCommMonoid ↥(integralIdealsAway S)

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

theorem TauCeti.NumberFieldArithmetic.integralIdealsAway_hom_ext {R : Type u_1} [CommRing R] [IsDedekindDomain R] {M : Type u_3} [MulOne M] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {f g : ↥(integralIdealsAway S) →* M} (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum R) (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 {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Finset (IsDedekindDomain.HeightOneSpectrum R)} {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 {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)} {I : Ideal R} : 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 {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)) : ↥(integralIdealsAway S) →* ↥(idealsAway K S)

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

@[simp]

theorem TauCeti.NumberFieldArithmetic.coe_integralIdealsAwayHom {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)) (I : ↥(integralIdealsAway S)) : ↑↑((integralIdealsAwayHom K S) I) = ↑↑I

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

theorem TauCeti.NumberFieldArithmetic.integralIdealsAwayHom_injective {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.Injective ⇑(integralIdealsAwayHom K S)

The integral-to-fractional ideal map is injective.

theorem TauCeti.NumberFieldArithmetic.exists_integralIdealsAway_div {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)) (I : ↥(idealsAway K S)) : ∃ (A : ↥(integralIdealsAway S)) (B : ↥(integralIdealsAway S)), I = (integralIdealsAwayHom K S) A / (integralIdealsAwayHom K S) B

Every fractional ideal away from S is a quotient of two integral ideals away from S.

noncomputable def TauCeti.NumberFieldArithmetic.integralIdealsAwayLocalizationMap {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)) : ⊤.LocalizationMap ↥(idealsAway K S)

The group of fractional ideals away from S is the localization of its integral ideal monoid at all its elements. This supplies the universal property for extending multiplicative maps on integral ideals to fractional ideals.

@[simp]

theorem TauCeti.NumberFieldArithmetic.integralIdealsAwayLocalizationMap_apply {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)) (I : ↥(integralIdealsAway S)) : (integralIdealsAwayLocalizationMap K S) I = (integralIdealsAwayHom K S) I

The localization map is the canonical integral-to-fractional ideal map.