def
ExtendsValuation
(A : Type u_1)
[CommRing A]
[IsDedekindDomain A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
(w : Valuation L (WithZero (Multiplicative ℤ)))
:
Instances For
def
primesAbove
(A : Type u_1)
[CommRing A]
(B : Type u_4)
[CommRing B]
[Algebra A B]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
:
Instances For
theorem
mem_of_liesOver
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDedekindDomain A]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDedekindDomain B]
[Algebra A B]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
(𝔮 : IsDedekindDomain.HeightOneSpectrum B)
(hlo : 𝔮.asIdeal.LiesOver 𝔭.asIdeal)
(a : A)
:
theorem
valuation_extends_of_liesOver
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDedekindDomain A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDedekindDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
(𝔮 : IsDedekindDomain.HeightOneSpectrum B)
(hlo : 𝔮.asIdeal.LiesOver 𝔭.asIdeal)
:
ExtendsValuation A K L 𝔭 (IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮)
theorem
dvr_overring_equiv
{B' : Type u_5}
[CommRing B']
[IsDomain B']
[IsDedekindDomain B']
{L' : Type u_6}
[Field L']
[Algebra B' L']
[IsFractionRing B' L']
(𝔮 : IsDedekindDomain.HeightOneSpectrum B')
(w : Valuation L' (WithZero (Multiplicative ℤ)))
(hB : ∀ (b : B'), w ((algebraMap B' L') b) ≤ 1)
(hIdeal : ∀ (b : B'), b ∈ 𝔮.asIdeal ↔ w ((algebraMap B' L') b) < 1)
:
theorem
valuation_surjective_of_extends
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDedekindDomain A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDedekindDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
(w : Valuation L (WithZero (Multiplicative ℤ)))
(hw : ExtendsValuation A K L 𝔭 w)
:
∃ 𝔮 ∈ primesAbove A B 𝔭, (IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮).IsEquiv w
theorem
extending_valuation_bijection_primes_above
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDedekindDomain A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDedekindDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
[IsFractionRing B L]
(𝔭 : IsDedekindDomain.HeightOneSpectrum A)
:
(∀ (𝔮₁ 𝔮₂ : IsDedekindDomain.HeightOneSpectrum B),
𝔮₁ ∈ primesAbove A B 𝔭 →
𝔮₂ ∈ primesAbove A B 𝔭 →
(IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮₁).IsEquiv
(IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮₂) →
𝔮₁ = 𝔮₂) ∧ ∀ (w : Valuation L (WithZero (Multiplicative ℤ))),
ExtendsValuation A K L 𝔭 w → ∃ 𝔮 ∈ primesAbove A B 𝔭, (IsDedekindDomain.HeightOneSpectrum.valuation L 𝔮).IsEquiv w