Ramification theory for valuations

• A is a Dedekind domain with field of fractions K.
• B is a Dedekind domain with field of fractions L.
• L is a field extension of K.
• v is a height one prime ideal of A.
• w is a height one prime ideal of B lying over v.

This file establishes the relationship between the adic valuation on K associated to v and the adic valuation on L associated to w, in terms of the ramification index.

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_liesOver {A : Type u_1} {B : Type u_4} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : A) : v.intValuation x ^ w.asIdeal.ramificationIdx A = w.intValuation ((algebraMap A B) x)

theorem IsDedekindDomain.HeightOneSpectrum.valuation_liesOver {A : Type u_1} {K : Type u_2} (L : Type u_3) {B : Type u_4} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower A B L] (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : K) : (valuation K v) x ^ w.asIdeal.ramificationIdx A = (valuation L w) ((algebraMap K L) x)

theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver {A : Type u_1} (K : Type u_2) (L : Type u_3) {B : Type u_4} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower A B L] (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : UniformContinuous ⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))