Basic lemmas on valuations that are trivial over a base ring

This file contains additional results about Valuation.IsTrivialOn which is defined in Mathlib.RingTheory.Valuation.Basic.

In what follows, we consider a A-algebra B and a valuation v over B which is trivial on A.

Main results

• valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X: Let p be a polynomial over A evaluated at an element w of B for which 1 < v w. We have the equality v (p.aeval w) = v w ^ p.natDegree.
• Valuation.transcendental_of_ne_one: If y : B is such that y ≠ 0 and v y ≠ 1, then it is transcendental over A. Note that, in particular, this means that any non zero element of the maximal ideal of v.valuationSubring is transcendental over A.

theorem Polynomial.valuation_aeval_monomial_eq_valuation_pow {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [CommSemiring A] {B : Type u_3} [Ring B] [Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B) (n : ℕ) {a : A} (ha : a ≠ 0) : v ((aeval w) ((monomial n) a)) = v w ^ n

theorem Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [CommSemiring A] {B : Type u_3} [Ring B] [Algebra A B] {v : Valuation B Γ} [hv : Valuation.IsTrivialOn A v] (w : B) (hpos : 1 < v w) {p : Polynomial A} (hp : p ≠ 0) : v ((aeval w) p) = v w ^ p.natDegree

theorem Valuation.transcendental_of_ne_one {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (A : Type u_2) [CommRing A] {K : Type u_3} [Field K] [Algebra A K] {v : Valuation K Γ} [hv : IsTrivialOn A v] (y : K) (h0 : y ≠ 0) (hy : v y ≠ 1) : Transcendental A y

For an A-algebra K and a valuation v over K which is trivial on A. If y : K is such that y ≠ 0 and v y ≠ 1, then it is transcendental over A.