Valuations trivial on a base ring

A valuation trivial on a base ring stays trivial on that base when restricted along a map of algebras over it. The restriction changes where the valuation is evaluated but not what it does to constants, because an algebra map fixes them.

A valuation trivial on a base ring also sees the base as scalars of size one, so a family of elements with pairwise distinct nonzero valuations is linearly independent over the base: in a linear combination with a nonzero coefficient, the summand of largest valuation dominates and the combination cannot vanish.

Main results

• Valuation.IsTrivialOn.comap: restriction preserves triviality on the base, for a valuation on any algebra restricted along any algebra map over that base.
• Valuation.linearIndependent_of_injective: elements of pairwise distinct nonzero valuations are linearly independent over a base ring on which the valuation is trivial.

References

• T. Wedhorn, Adic Spaces, for valuations, their restriction along a ring map, and triviality on a base ring.

instance Valuation.IsTrivialOn.comap {Γ₀ : Type u_1} [LinearOrderedCommMonoidWithZero Γ₀] {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring A] [Ring B] [Ring C] [Algebra A B] [Algebra A C] (v : Valuation C Γ₀) (f : B →ₐ[A] C) [IsTrivialOn A v] : IsTrivialOn A (Valuation.comap f.toRingHom v)

Restricting a valuation along an algebra map preserves triviality on the base. An algebra map fixes the base, so the restricted valuation takes the same values on constants.

theorem Valuation.linearIndependent_of_injective {Γ₀ : Type u_1} [LinearOrderedCommMonoidWithZero Γ₀] {A : Type u_2} {B : Type u_3} [CommRing A] [Ring B] [Algebra A B] (v : Valuation B Γ₀) [IsTrivialOn A v] {ι : Type u_4} {f : ι → B} (hf : ∀ (i : ι), v (f i) ≠ 0) (hinj : Function.Injective (⇑v ∘ f)) : LinearIndependent A f

Elements of pairwise distinct nonzero valuations are linearly independent over a base ring on which the valuation is trivial. A nontrivial linear combination has, among its summands with nonzero coefficient, a unique one of largest valuation, and that summand dictates the valuation of the sum, which is therefore nonzero.