Normalized height-one valuations under ring equivalences #
Identity-on-fraction-field ring equivalences identify corresponding valuation rings. Surjectivity then identifies their integer-valued normalizations.
theorem
BGS.HasseWeil.heightOneValuation_le_one_of_ringEquiv
{R : Type u_1}
{S : Type u_2}
{F : Type u_3}
[CommRing R]
[CommRing S]
[Field F]
[Algebra R F]
[Algebra S F]
[IsFractionRing R F]
[IsFractionRing S F]
[IsDedekindDomain R]
[IsDedekindDomain S]
(e : R ≃+* S)
(halg : ∀ (r : R), (algebraMap S F) (e r) = (algebraMap R F) r)
(q : IsDedekindDomain.HeightOneSpectrum R)
(q' : IsDedekindDomain.HeightOneSpectrum S)
(hideal : q'.asIdeal = Ideal.comap e.symm q.asIdeal)
{x : F}
(hx : (IsDedekindDomain.HeightOneSpectrum.valuation F q) x ≤ 1)
:
Transport the condition of belonging to a height-one valuation ring across an identity-on-fraction-field ring equivalence.
theorem
BGS.HasseWeil.heightOneValuation_isEquiv_of_ringEquiv
{R : Type u_1}
{S : Type u_2}
{F : Type u_3}
[CommRing R]
[CommRing S]
[Field F]
[Algebra R F]
[Algebra S F]
[IsFractionRing R F]
[IsFractionRing S F]
[IsDedekindDomain R]
[IsDedekindDomain S]
(e : R ≃+* S)
(halg : ∀ (r : R), (algebraMap S F) (e r) = (algebraMap R F) r)
(q : IsDedekindDomain.HeightOneSpectrum R)
(q' : IsDedekindDomain.HeightOneSpectrum S)
(hideal : q'.asIdeal = Ideal.comap e.symm q.asIdeal)
:
Identity-on-fraction-field equivalences identify the valuation rings of corresponding height-one primes.
theorem
BGS.HasseWeil.normalizedIntValuation_eq_of_isEquiv_of_surjective
{F : Type u_1}
[Field F]
(v w : Valuation F (WithZero (Multiplicative ℤ)))
(hvw : v.IsEquiv w)
(hv : Function.Surjective ⇑v)
(hw : Function.Surjective ⇑w)
:
Equivalent surjective valuations with value group ℤᵐ⁰ have the same
normalization.
theorem
BGS.HasseWeil.heightOneValuation_eq_of_ringEquiv
{R : Type u_1}
{S : Type u_2}
{F : Type u_3}
[CommRing R]
[CommRing S]
[Field F]
[Algebra R F]
[Algebra S F]
[IsFractionRing R F]
[IsFractionRing S F]
[IsDedekindDomain R]
[IsDedekindDomain S]
(e : R ≃+* S)
(halg : ∀ (r : R), (algebraMap S F) (e r) = (algebraMap R F) r)
(q : IsDedekindDomain.HeightOneSpectrum R)
(q' : IsDedekindDomain.HeightOneSpectrum S)
(hideal : q'.asIdeal = Ideal.comap e.symm q.asIdeal)
:
Corresponding height-one primes have exactly the same normalized
ℤᵐ⁰-valued valuation under an identity-on-fraction-field equivalence.