ValuationSubring.exists_eq_valuationSubringAtPrime_of_forall_algebraMap_mem
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_eq_valuationSubringAtPrime_of_forall_algebraMap_mem
open IsDedekindDomainLean source · statement
theorem _root_.ValuationSubring.exists_eq_valuationSubringAtPrime_of_forall_algebraMap_mem
{R K : Type*} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K]
(V : ValuationSubring K) (hRV : ∀ r : R, algebraMap R K r ∈ V) (hV : V ≠ ⊤) :
∃ v : HeightOneSpectrum R, V = v.valuationSubringAtPrime K ∧
∀ r : R, r ∈ v.asIdeal ↔ algebraMap R K r ∈ V.nonunits