The residue map on v-integral elements of the fraction field

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

Let R be a Dedekind domain with fraction field K and let v be a height-one prime of R. An element of K of v-adic valuation at most 1 is congruent to an element of R modulo elements of valuation < 1 (exists_valuation_sub_lt_of_integer), and the class in R ⧸ v.asIdeal of such an approximant does not depend on its choice. This file packages the resulting residue map as a ring homomorphism residueHom : (v.valuation K).integer →+* R ⧸ v.asIdeal on the subring of v-integral elements of K, extending Ideal.Quotient.mk v.asIdeal (residueHom_algebraMap); an unfolding requires only some approximant (residueHom_eq).

It also provides the R-algebra structure on (v.valuation K).integer and the Field instance on R ⧸ v.asIdeal (the ideal is maximal).

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instFieldQuotientHeightOneIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : HeightOneSpectrum R) : Field (R ⧸ v.asIdeal)

Equations

• v.instFieldQuotientHeightOneIdeal = Ideal.Quotient.field v.asIdeal

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instAlgebraIntegerValuationSubring {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Algebra R ↥(valuation K v).integer

Equations

• v.instAlgebraIntegerValuationSubring = ((algebraMap R K).codRestrict (IsDedekindDomain.HeightOneSpectrum.valuation K v).integer ⋯).toAlgebra

instance IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation_ellipticCurves {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsScalarTower R (↥(valuation K v).integer) K

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_integer {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (r : R) : ↑((algebraMap R ↥(valuation K v).integer) r) = (algebraMap R K) r

noncomputable def IsDedekindDomain.HeightOneSpectrum.residueAux {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : ↥(valuation K v).integer) : R

The distinguished R-approximant of a v-integral element of K (an element of R congruent to it modulo valuation < 1). Implementation detail of residueHom; use that (and residueHom_eq) instead.

Equations

• v.residueAux x = ⋯.choose

noncomputable def IsDedekindDomain.HeightOneSpectrum.residueHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ↥(valuation K v).integer →+* R ⧸ v.asIdeal

The residue map on the v-integral elements of K, with values in the residue field R ⧸ v.asIdeal: the class of any R-approximant within valuation < 1. It extends Ideal.Quotient.mk v.asIdeal (residueHom_algebraMap).

Equations

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

theorem IsDedekindDomain.HeightOneSpectrum.residueHom_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : ↥(valuation K v).integer} {a : R} (h : (valuation K v) ((algebraMap R K) a - ↑x) < 1) : v.residueHom x = (Ideal.Quotient.mk v.asIdeal) a

Unfolding lemma for residueHom: the residue of x is the class of any R-approximant of x within valuation < 1.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.residueHom_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (r : R) : v.residueHom ((algebraMap R ↥(valuation K v).integer) r) = (Ideal.Quotient.mk v.asIdeal) r