Extension of Valuations

In this file, we define the typeclass for valuation extensions and prove basic facts about the extension of valuations. Let A be an R algebra, equipped with valuations vA and vR respectively. Here, the extension of a valuation means that the pullback of valuation vA to R is equivalent to the valuation vR on R. We only require equivalence, not equality, of valuations here.

Note that we do not require the ring map from R to A to be injective. This holds automatically when R is a division ring and A is nontrivial.

A motivation for choosing the more flexible Valuation.Equiv rather than strict equality here is to allow for possible normalization. As an example, consider a finite extension K of ℚ_[p], which is a discretely valued field. We may choose the valuation on K to be either:

1. the valuation where the uniformizer is mapped to one (more precisely, -1 in ℤₘ₀) or

2. the valuation where p is mapped to one.

For the algebraic closure of ℚ_[p], if we choose the valuation of p to be one, then the restriction of this valuation to K equals the second valuation, but is only equivalent to the first valuation. The flexibility of equivalence here allows us to develop theory for both cases without first determining the normalizations once and for all.

Main Definition

• Valuation.HasExtension vR vA : The valuation vA on A is an extension of the valuation vR on R.

References

• [Bourbaki, Nicolas. Commutative algebra] Chapter VI §3, Valuations.
• https://en.wikipedia.org/wiki/Valuation_(algebra)#Extension_of_valuations

Tags

Valuation, Extension of Valuations

class Valuation.HasExtension {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) : Prop

The class Valuation.HasExtension vR vA states that the valuation vA on A is an extension of the valuation vR on R. More precisely, vR is equivalent to the comap of the valuation vA.

• val_isEquiv_comap : vR.IsEquiv (comap (algebraMap R A) vA)

  The valuation vR on R is equivalent to the comap of the valuation vA on A

@[deprecated Valuation.HasExtension (since := "2025-04-02")]

def IsValExtension {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) : Prop

Alias of Valuation.HasExtension.

---

The class Valuation.HasExtension vR vA states that the valuation vA on A is an extension of the valuation vR on R. More precisely, vR is equivalent to the comap of the valuation vA.

Equations

• @IsValExtension = @Valuation.HasExtension

theorem Valuation.HasExtension.val_map_le_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R) : vA ((algebraMap R A) x) ≤ vA ((algebraMap R A) y) ↔ vR x ≤ vR y

theorem Valuation.HasExtension.val_map_lt_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R) : vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y

theorem Valuation.HasExtension.val_map_eq_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x y : R) : vA ((algebraMap R A) x) = vA ((algebraMap R A) y) ↔ vR x = vR y

theorem Valuation.HasExtension.val_map_le_one_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R) : vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1

theorem Valuation.HasExtension.val_map_lt_one_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R) : vA ((algebraMap R A) x) < 1 ↔ vR x < 1

theorem Valuation.HasExtension.val_map_eq_one_iff {R : Type u_1} {A : Type u_2} {ΓR : Type u_3} {ΓA : Type u_4} [CommRing R] [Ring A] [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] [Algebra R A] (vR : Valuation R ΓR) (vA : Valuation A ΓA) [vR.HasExtension vA] (x : R) : vA ((algebraMap R A) x) = 1 ↔ vR x = 1

instance Valuation.HasExtension.id {R : Type u_1} {ΓR : Type u_3} [CommRing R] [LinearOrderedCommMonoidWithZero ΓR] (vR : Valuation R ΓR) : vR.HasExtension vR

theorem Valuation.HasExtension.ofComapInteger {A : Type u_2} [Ring A] {K : Type u_5} [Field K] [Algebra K A] {ΓA : Type u_7} {ΓK : Type u_8} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓA] {vK : Valuation K ΓK} {vA : Valuation A ΓA} (h : Subring.comap (algebraMap K A) vA.integer = vK.integer) : vK.HasExtension vA

When K is a field, if the preimage of the valuation integers of A equals to the valuation integers of K, then the valuation on A is an extension of the valuation on K.

instance Valuation.HasExtension.instAlgebraInteger {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {ΓR : Type u_6} {ΓA : Type u_7} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] {vR : Valuation R ΓR} {vA : Valuation A ΓA} [vR.HasExtension vA] : Algebra ↥vR.integer ↥vA.integer

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Valuation.HasExtension.val_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {ΓR : Type u_6} {ΓA : Type u_7} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] {vR : Valuation R ΓR} {vA : Valuation A ΓA} [vR.HasExtension vA] (r : ↥vR.integer) (a : ↥vA.integer) : ↑(r • a) = ↑r • ↑a

@[simp]

theorem Valuation.HasExtension.val_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {ΓR : Type u_6} {ΓA : Type u_7} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] {vR : Valuation R ΓR} {vA : Valuation A ΓA} [vR.HasExtension vA] (r : ↥vR.integer) : ↑((algebraMap ↥vR.integer ↥vA.integer) r) = (algebraMap R A) ↑r

instance Valuation.HasExtension.instIsScalarTowerInteger {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {ΓR : Type u_6} {ΓA : Type u_7} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] {vR : Valuation R ΓR} {vA : Valuation A ΓA} [vR.HasExtension vA] : IsScalarTower (↥vR.integer) (↥vA.integer) A

instance Valuation.HasExtension.instNoZeroSMulDivisorsInteger {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {ΓR : Type u_6} {ΓA : Type u_7} [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] {vR : Valuation R ΓR} {vA : Valuation A ΓA} [vR.HasExtension vA] [NoZeroSMulDivisors R A] : NoZeroSMulDivisors ↥vR.integer ↥vA.integer

theorem Valuation.HasExtension.algebraMap_injective {A : Type u_2} [Ring A] {K : Type u_5} [Field K] [Algebra K A] {ΓA : Type u_7} {ΓK : Type u_8} [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓA] {vK : Valuation K ΓK} {vA : Valuation A ΓA} [vK.HasExtension vA] [Nontrivial A] : Function.Injective ⇑(algebraMap ↥vK.integer ↥vA.integer)

instance Valuation.HasExtension.instIsLocalHomValuationInteger {R : Type u_1} [CommRing R] {ΓR : Type u_6} [LinearOrderedCommGroupWithZero ΓR] {vR : Valuation R ΓR} {S : Type u_9} {ΓS : Type u_10} [CommRing S] [LinearOrderedCommGroupWithZero ΓS] [Algebra R S] [IsLocalHom (algebraMap R S)] {vS : Valuation S ΓS} [vR.HasExtension vS] : IsLocalHom (algebraMap ↥vR.integer ↥vS.integer)