Documentation

LeanPool.RiemannRochFunctionFields.LocalResidue

Local residue maps for height-one primes of Dedekind domains.

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

The residue map from the valuation ring at a height-one prime.

Equations
Instances For
    source
    theorem IsDedekindDomain.HeightOneSpectrum.residueHom_eq_zero_iff {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (z : ↥(valuationSubringAtPrime K v)) :
    v.residueHom z = 0 ↔ (valuation K v) ↑z < 1

    An element has zero residue exactly when its valuation is strictly less than one.

    source
    noncomputable def IsDedekindDomain.HeightOneSpectrum.localizationAlgEquiv {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) :
    Localization.AtPrime v.asIdeal ≃ₐ[R] ↥(valuationSubringAtPrime K v)

    The localization at a height-one prime is algebra-equivalent to its valuation subring.

    Equations
    Instances For
      source
      theorem IsDedekindDomain.HeightOneSpectrum.residueHom_mk' {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : R) (d : ↥v.asIdeal.primeCompl) :
      v.residueHom (IsLocalization.mk' (↥(valuationSubringAtPrime K v)) n d) = (algebraMap R v.asIdeal.ResidueField) n * ((algebraMap R v.asIdeal.ResidueField) ↑d)⁻¹

      residueHom on a localized fraction agrees with the quotient map.

      source
      theorem IsDedekindDomain.HeightOneSpectrum.residueHom_mk'_residue {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (n : R) (d : ↥v.asIdeal.primeCompl) :
      v.residueHom (IsLocalization.mk' (↥(valuationSubringAtPrime K v)) n d) = (IsLocalRing.residue (Localization.AtPrime v.asIdeal)) (IsLocalization.mk' (Localization.AtPrime v.asIdeal) n d)

      residueHom on a localized fraction agrees with the residue map on AtPrime.

      source
      theorem IsDedekindDomain.HeightOneSpectrum.residueHom_apply_localizationAlgEquiv {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : Localization.AtPrime v.asIdeal) :
      v.residueHom (v.localizationAlgEquiv x) = (IsLocalRing.residue (Localization.AtPrime v.asIdeal)) x

      residueHom agrees with the residue map on the localization model.