Documentation

LeanPool.MarkoffModP.RiemannRoch.LocalResidue

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

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

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

Equations
Instances For
    source
    theorem MarkoffRiemannRoch.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 : IsDedekindDomain.HeightOneSpectrum R) (z : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)) :
    (residueHom v) z = 0 ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑z < 1

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

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

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MarkoffRiemannRoch.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 : IsDedekindDomain.HeightOneSpectrum R) (n : R) (d : ↥v.asIdeal.primeCompl) :
      (residueHom v) (IsLocalization.mk' (↥(IsDedekindDomain.HeightOneSpectrum.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 MarkoffRiemannRoch.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 : IsDedekindDomain.HeightOneSpectrum R) (n : R) (d : ↥v.asIdeal.primeCompl) :
      (residueHom v) (IsLocalization.mk' (↥(IsDedekindDomain.HeightOneSpectrum.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 MarkoffRiemannRoch.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 : IsDedekindDomain.HeightOneSpectrum R) (x : Localization.AtPrime v.asIdeal) :
      (residueHom v) ((localizationAlgEquiv v) x) = (IsLocalRing.residue (Localization.AtPrime v.asIdeal)) x

      residueHom agrees with the residue map on the localization model.