Documentation

Mathlib.RingTheory.Valuation.Extension

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 #

References #

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) :

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

Instances
    @[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) :

    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
    Instances For
      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) :
      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) :

      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
      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] :