English
The coarsening of a valuation subring associated to a prime ideal P is constructed by localizing at P and pulling back to A.
Русский
Упрощение валюационного подкольца, связанного с простым идеалом P, строится через локализацию и последующее обратное включение.
LaTeX
$$def ofPrime (A : ValuationSubring K) (P : Ideal (Subtype fun x => SetLike.instMembership.mem A x)) [P.IsPrime] : ValuationSubring K := ofLE A (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors).toSubring ...$$
Lean4
/-- The coarsening of a valuation ring associated to a prime ideal. -/
def ofPrime (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] : ValuationSubring K :=
ofLE A (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors).toSubring fun a ha =>
Subalgebra.mem_toSubring.mpr <|
Subalgebra.algebraMap_mem (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors) (⟨a, ha⟩ : A)
