Yamaguchi26AbfaithfulGalois.exists_discreteValuationSubring_preserving_nonunit
A nonzero base-ring element which is a nonunit in a valuation ring remains a nonunit in a discrete valuation ring of the finitely generated field.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u v wLean source · statement
theorem exists_discreteValuationSubring_preserving_nonunit
(R : Type u) (F : Type v) (E : Type w)
[CommRing R] [IsDomain R] [IsNoetherianRing R] [Field F] [Field E]
[Algebra R F] [IsFractionRing R F] [Algebra F E] [Algebra R E]
[IsScalarTower R F E] [Algebra.EssFiniteType F E]
(V : ValuationSubring E) (hR : ∀ r : R, algebraMap R E r ∈ V)
(r : R) (hr0 : algebraMap R E r ≠ 0) (hr : algebraMap R E r ∈ V.nonunits) :
∃ W : ValuationSubring E, IsDiscreteValuationRing W ∧ algebraMap R E r ∈ W.nonunits