Nontriviality survives restriction along an integral algebra

A valuation of L restricts along algebraMap K L to a valuation of K, and this file records that the restriction of a nontrivial valuation is again nontrivial as soon as L is integral over K.

Integrality is what makes this true, and it is sharp: without it the restriction can collapse. The valuation of K(t) reading the t-adic order restricts to the trivial valuation on K.

This is restriction of the domain, along a ring map. It is unrelated to Valuation.RankOne.isNontrivial_restrict, which restricts the value group of a valuation to its value subgroup and leaves the domain alone.

Main results

• Valuation.isNontrivial_comap_algebraMap: the restriction of a nontrivial valuation along an integral algebra is nontrivial.

References

• A. J. Engler and A. Prestel, Valued Fields.

theorem Valuation.isNontrivial_comap_algebraMap {K : Type u_1} {L : Type u_2} {Γ₀ : Type u_3} [CommRing K] [Field L] [Algebra K L] [LinearOrderedCommGroupWithZero Γ₀] [Algebra.IsIntegral K L] (v : Valuation L Γ₀) [v.IsNontrivial] : (comap (algebraMap K L) v).IsNontrivial

The restriction of a nontrivial valuation along an integral algebra is nontrivial.