Extension of Valuation

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

• IsValExtension 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 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

The class IsValExtension R A states that the valuation of A is an extension of the valuation on R. More precisely, the valuation on R is equivlent to the comap of the valuation on A.

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

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

theorem IsValExtension.val_isEquiv_comap {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} [self : IsValExtension vR vA] : vR.IsEquiv (Valuation.comap (algebraMap R A) vA)

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

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) (y : R) : vA ((algebraMap R A) x) ≤ vA ((algebraMap R A) y) ↔ vR x ≤ vR y

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) (y : R) : vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) (y : R) : vA ((algebraMap R A) x) = vA ((algebraMap R A) y) ↔ vR x = vR y

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) : vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) : vA ((algebraMap R A) x) < 1 ↔ vR x < 1

theorem IsValExtension.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) [IsValExtension vR vA] (x : R) : vA ((algebraMap R A) x) = 1 ↔ vR x = 1

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

Equations

• ⋯ = ⋯

theorem IsValExtension.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) : IsValExtension vK 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 IsValExtension.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} [IsValExtension vR vA] : Algebra { x : R // x ∈ vR.integer } { x : A // x ∈ vA.integer }

Equations

• IsValExtension.instAlgebraInteger = Algebra.mk ((algebraMap R A).restrict vR.integer vA.integer ⋯) ⋯ ⋯

@[simp]

theorem IsValExtension.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} [IsValExtension vR vA] (r : { x : R // x ∈ vR.integer }) (a : { x : A // x ∈ vA.integer }) : ↑(r • a) = ↑r • ↑a

@[simp]

theorem IsValExtension.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} [IsValExtension vR vA] (r : { x : R // x ∈ vR.integer }) : ↑((algebraMap { x : R // x ∈ vR.integer } { x : A // x ∈ vA.integer }) r) = (algebraMap R A) ↑r

instance IsValExtension.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} [IsValExtension vR vA] : IsScalarTower { x : R // x ∈ vR.integer } { x : A // x ∈ vA.integer } A

Equations

• ⋯ = ⋯

instance IsValExtension.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} [IsValExtension vR vA] [NoZeroSMulDivisors R A] : NoZeroSMulDivisors { x : R // x ∈ vR.integer } { x : A // x ∈ vA.integer }

Equations

• ⋯ = ⋯

theorem IsValExtension.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} [IsValExtension vK vA] [Nontrivial A] : Function.Injective ⇑(algebraMap { x : K // x ∈ vK.integer } { x : A // x ∈ vA.integer })

instance IsValExtension.instIsLocalRingHomValuationInteger {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] [IsLocalRingHom (algebraMap R S)] {vS : Valuation S ΓS} [IsValExtension vR vS] : IsLocalRingHom (algebraMap { x : R // x ∈ vR.integer } { x : S // x ∈ vS.integer })

Equations

• ⋯ = ⋯