Yamaguchi26AbfaithfulGalois.finiteType_model_in_valuation
A finitely generated extension of a fraction field admits a finite type integral model inside any valuation ring containing the base ring.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u v wLean source · statement
theorem finiteType_model_in_valuation
(R : Type u) (F : Type v) (E : Type w)
[CommRing R] [IsDomain 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) :
∃ A : Subalgebra R E, Algebra.FiniteType R A ∧ IsFractionRing A E ∧
A.toSubring ≤ V.toSubring