Valuation subrings of a field #

Projects #

The order structure on ValuationSubring K.

source

structure ValuationSubring (K : Type u) [Field K] extends Subring :

Type u

carrier : Set K
mul_mem' : ∀ {a b : K}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
one_mem' : 1 ∈ s.carrier
add_mem' : ∀ {a b : K}, a ∈ s.carrier → b ∈ s.carrier → a + b ∈ s.carrier
zero_mem' : 0 ∈ s.carrier
neg_mem' : ∀ {x : K}, x ∈ s.carrier → -x ∈ s.carrier
mem_or_inv_mem' : ∀ (x : K), x ∈ s.carrier ∨ x⁻¹ ∈ s.carrier

A valuation subring of a field K is a subring A such that for every x : K, either x ∈ A or x⁻¹ ∈ A.

Instances For

source

instance ValuationSubring.instSetLikeValuationSubring {K : Type u} [Field K] :

SetLike (ValuationSubring K) K

source

@[simp]

theorem ValuationSubring.mem_carrier {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :

x ∈ A.carrier ↔ x ∈ A

source

@[simp]

theorem ValuationSubring.mem_toSubring {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :

x ∈ A.toSubring ↔ x ∈ A

source

theorem ValuationSubring.ext {K : Type u} [Field K] (A : ValuationSubring K) (B : ValuationSubring K) (h : ∀ (x : K), x ∈ A ↔ x ∈ B) :

A = B

source

theorem ValuationSubring.zero_mem {K : Type u} [Field K] (A : ValuationSubring K) :

0 ∈ A

source

theorem ValuationSubring.one_mem {K : Type u} [Field K] (A : ValuationSubring K) :

1 ∈ A

source

theorem ValuationSubring.add_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :

x ∈ A → y ∈ A → x + y ∈ A

source

theorem ValuationSubring.mul_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :

x ∈ A → y ∈ A → x * y ∈ A

source

theorem ValuationSubring.neg_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :

x ∈ A → -x ∈ A

source

theorem ValuationSubring.mem_or_inv_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :

x ∈ A ∨ x⁻¹ ∈ A

source

instance ValuationSubring.instSubringClassValuationSubringToRingToDivisionRingInstSetLikeValuationSubring {K : Type u} [Field K] :

SubringClass (ValuationSubring K) K

source

theorem ValuationSubring.toSubring_injective {K : Type u} [Field K] :

Function.Injective ValuationSubring.toSubring

source

instance ValuationSubring.instCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubring {K : Type u} [Field K] (A : ValuationSubring K) :

CommRing { x // x ∈ A }

source

instance ValuationSubring.instIsDomainSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToSemiringToSemiringToRingToDivisionRingToSubsemiringToSubring {K : Type u} [Field K] (A : ValuationSubring K) :

IsDomain { x // x ∈ A }

source

instance ValuationSubring.instTopValuationSubring {K : Type u} [Field K] :

Top (ValuationSubring K)

source

theorem ValuationSubring.mem_top {K : Type u} [Field K] (x : K) :

x ∈ ⊤

source

theorem ValuationSubring.le_top {K : Type u} [Field K] (A : ValuationSubring K) :

A ≤ ⊤

source

instance ValuationSubring.instOrderTopValuationSubringToLEToPreorderInstPartialOrderInstSetLikeValuationSubring {K : Type u} [Field K] :

OrderTop (ValuationSubring K)

source

instance ValuationSubring.instInhabitedValuationSubring {K : Type u} [Field K] :

Inhabited (ValuationSubring K)

source

instance ValuationSubring.instValuationRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringInstCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringInstIsDomainSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToSemiringToSemiringToRingToDivisionRingToSubsemiringToSubring {K : Type u} [Field K] (A : ValuationSubring K) :

ValuationRing { x // x ∈ A }

source

instance ValuationSubring.instAlgebraSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToCommSemiringToCommSemiringToSemifieldToSubsemiringToRingToDivisionRingToSubringToSemiringToDivisionSemiring {K : Type u} [Field K] (A : ValuationSubring K) :

Algebra { x // x ∈ A } K

source

instance ValuationSubring.localRing {K : Type u} [Field K] (A : ValuationSubring K) :

LocalRing { x // x ∈ A }

source

@[simp]

theorem ValuationSubring.algebraMap_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }) :

↑(algebraMap { x // x ∈ A } K) a = ↑a

source

instance ValuationSubring.instIsFractionRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringInstCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToCommRingToEuclideanDomainInstAlgebraSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToCommSemiringToCommSemiringToSemifieldToSubsemiringToRingToDivisionRingToSubringToSemiringToDivisionSemiring {K : Type u} [Field K] (A : ValuationSubring K) :

IsFractionRing { x // x ∈ A } K

source

def ValuationSubring.ValueGroup {K : Type u} [Field K] (A : ValuationSubring K) :

Type u

The value group of the valuation associated to A. Note: it is actually a group with zero.

Instances For

source

instance ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup {K : Type u} [Field K] (A : ValuationSubring K) :

LinearOrderedCommGroupWithZero (ValuationSubring.ValueGroup A)

source

def ValuationSubring.valuation {K : Type u} [Field K] (A : ValuationSubring K) :

Valuation K (ValuationSubring.ValueGroup A)

Any valuation subring of K induces a natural valuation on K.

Instances For

source

instance ValuationSubring.inhabitedValueGroup {K : Type u} [Field K] (A : ValuationSubring K) :

Inhabited (ValuationSubring.ValueGroup A)

source

theorem ValuationSubring.valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }) :

↑(ValuationSubring.valuation A) ↑a ≤ 1

source

theorem ValuationSubring.mem_of_valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (h : ↑(ValuationSubring.valuation A) x ≤ 1) :

x ∈ A

source

theorem ValuationSubring.valuation_le_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :

↑(ValuationSubring.valuation A) x ≤ 1 ↔ x ∈ A

source

theorem ValuationSubring.valuation_eq_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :

↑(ValuationSubring.valuation A) x = ↑(ValuationSubring.valuation A) y ↔ ∃ a, ↑↑a * y = x

source

theorem ValuationSubring.valuation_le_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :

↑(ValuationSubring.valuation A) x ≤ ↑(ValuationSubring.valuation A) y ↔ ∃ a, ↑a * y = x

source

theorem ValuationSubring.valuation_surjective {K : Type u} [Field K] (A : ValuationSubring K) :

Function.Surjective ↑(ValuationSubring.valuation A)

source

theorem ValuationSubring.valuation_unit {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }ˣ) :

↑(ValuationSubring.valuation A) ↑↑a = 1

source

theorem ValuationSubring.valuation_eq_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }) :

IsUnit a ↔ ↑(ValuationSubring.valuation A) ↑a = 1

source

theorem ValuationSubring.valuation_lt_one_or_eq_one {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }) :

↑(ValuationSubring.valuation A) ↑a < 1 ∨ ↑(ValuationSubring.valuation A) ↑a = 1

source

theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }) :

a ∈ LocalRing.maximalIdeal { x // x ∈ A } ↔ ↑(ValuationSubring.valuation A) ↑a < 1

source

def ValuationSubring.ofSubring {K : Type u} [Field K] (R : Subring K) (hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) :

ValuationSubring K

A subring R of K such that for all x : K either x ∈ R or x⁻¹ ∈ R is a valuation subring of K.

Instances For

source

@[simp]

theorem ValuationSubring.mem_ofSubring {K : Type u} [Field K] (R : Subring K) (hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) (x : K) :

x ∈ ValuationSubring.ofSubring R hR ↔ x ∈ R

source

def ValuationSubring.ofLE {K : Type u} [Field K] (R : ValuationSubring K) (S : Subring K) (h : R.toSubring ≤ S) :

ValuationSubring K

An overring of a valuation ring is a valuation ring.

Instances For

source

instance ValuationSubring.instSemilatticeSupValuationSubring {K : Type u} [Field K] :

SemilatticeSup (ValuationSubring K)

source

def ValuationSubring.inclusion {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

{ x // x ∈ R } →+* { x // x ∈ S }

The ring homomorphism induced by the partial order.

Instances For

source

def ValuationSubring.subtype {K : Type u} [Field K] (R : ValuationSubring K) :

{ x // x ∈ R } →+* K

The canonical ring homomorphism from a valuation ring to its field of fractions.

Instances For

source

def ValuationSubring.mapOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

ValuationSubring.ValueGroup R →*₀ ValuationSubring.ValueGroup S

The canonical map on value groups induced by a coarsening of valuation rings.

Instances For

source

theorem ValuationSubring.monotone_mapOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

Monotone ↑(ValuationSubring.mapOfLE R S h)

source

@[simp]

theorem ValuationSubring.mapOfLE_comp_valuation {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

↑(ValuationSubring.mapOfLE R S h) ∘ ↑(ValuationSubring.valuation R) = ↑(ValuationSubring.valuation S)

source

@[simp]

theorem ValuationSubring.mapOfLE_valuation_apply {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) (x : K) :

↑(ValuationSubring.mapOfLE R S h) (↑(ValuationSubring.valuation R) x) = ↑(ValuationSubring.valuation S) x

source

def ValuationSubring.idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

Ideal { x // x ∈ R }

The ideal corresponding to a coarsening of a valuation ring.

Instances For

source

instance ValuationSubring.prime_idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

Ideal.IsPrime (ValuationSubring.idealOfLE R S h)

source

def ValuationSubring.ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

ValuationSubring K

The coarsening of a valuation ring associated to a prime ideal.

Instances For

source

instance ValuationSubring.ofPrimeAlgebra {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

Algebra { x // x ∈ A } { x // x ∈ ValuationSubring.ofPrime A P }

source

instance ValuationSubring.ofPrime_scalar_tower {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

IsScalarTower { x // x ∈ A } { x // x ∈ ValuationSubring.ofPrime A P } K

source

instance ValuationSubring.ofPrime_localization {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

IsLocalization.AtPrime { x // x ∈ ValuationSubring.ofPrime A P } P

source

theorem ValuationSubring.le_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

A ≤ ValuationSubring.ofPrime A P

source

theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] (x : { x // x ∈ A }) :

↑(ValuationSubring.valuation (ValuationSubring.ofPrime A P)) ↑x = 1 ↔ x ∈ Ideal.primeCompl P

source

@[simp]

theorem ValuationSubring.idealOfLE_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) [Ideal.IsPrime P] :

ValuationSubring.idealOfLE A (ValuationSubring.ofPrime A P) (_ : A ≤ ValuationSubring.ofPrime A P) = P

source

@[simp]

theorem ValuationSubring.ofPrime_idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) :

ValuationSubring.ofPrime R (ValuationSubring.idealOfLE R S h) = S

source

theorem ValuationSubring.ofPrime_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal { x // x ∈ A }) (Q : Ideal { x // x ∈ A }) [Ideal.IsPrime P] [Ideal.IsPrime Q] (h : P ≤ Q) :

ValuationSubring.ofPrime A Q ≤ ValuationSubring.ofPrime A P

source

theorem ValuationSubring.idealOfLE_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (R : ValuationSubring K) (S : ValuationSubring K) (hR : A ≤ R) (hS : A ≤ S) (h : R ≤ S) :

ValuationSubring.idealOfLE A S hS ≤ ValuationSubring.idealOfLE A R hR

source

@[simp]

theorem ValuationSubring.primeSpectrumEquiv_apply_coe {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum { x // x ∈ A }) :

↑(↑(ValuationSubring.primeSpectrumEquiv A) P) = ValuationSubring.ofPrime A P.asIdeal

source

@[simp]

theorem ValuationSubring.primeSpectrumEquiv_symm_apply_asIdeal {K : Type u} [Field K] (A : ValuationSubring K) (S : ↑{S | A ≤ S}) :

(↑(ValuationSubring.primeSpectrumEquiv A).symm S).asIdeal = ValuationSubring.idealOfLE A ↑S (_ : ↑S ∈ {S | A ≤ S})

source

def ValuationSubring.primeSpectrumEquiv {K : Type u} [Field K] (A : ValuationSubring K) :

PrimeSpectrum { x // x ∈ A } ≃ ↑{S | A ≤ S}

The equivalence between coarsenings of a valuation ring and its prime ideals.

Instances For

source

@[simp]

theorem ValuationSubring.primeSpectrumOrderEquiv_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) :

∀ (a : ↑{S | A ≤ S}), ↑(RelIso.symm (ValuationSubring.primeSpectrumOrderEquiv A)) a = Equiv.invFun (ValuationSubring.primeSpectrumEquiv A) a

source

@[simp]

theorem ValuationSubring.primeSpectrumOrderEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) :

∀ (a : PrimeSpectrum { x // x ∈ A }), ↑(ValuationSubring.primeSpectrumOrderEquiv A) a = Equiv.toFun (ValuationSubring.primeSpectrumEquiv A) a

source

def ValuationSubring.primeSpectrumOrderEquiv {K : Type u} [Field K] (A : ValuationSubring K) :

(PrimeSpectrum { x // x ∈ A })ᵒᵈ ≃o ↑{S | A ≤ S}

An ordered variant of primeSpectrumEquiv.

Instances For

source

instance ValuationSubring.linearOrderOverring {K : Type u} [Field K] (A : ValuationSubring K) :

LinearOrder ↑{S | A ≤ S}

source

def Valuation.valuationSubring {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) :

ValuationSubring K

The valuation subring associated to a valuation.

Instances For

source

@[simp]

theorem Valuation.mem_valuationSubring_iff {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : K) :

x ∈ Valuation.valuationSubring v ↔ ↑v x ≤ 1

source

theorem Valuation.isEquiv_iff_valuationSubring {K : Type u} [Field K] {Γ₁ : Type u_2} {Γ₂ : Type u_3} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] (v₁ : Valuation K Γ₁) (v₂ : Valuation K Γ₂) :

Valuation.IsEquiv v₁ v₂ ↔ Valuation.valuationSubring v₁ = Valuation.valuationSubring v₂

source

theorem Valuation.isEquiv_valuation_valuationSubring {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) :

Valuation.IsEquiv v (ValuationSubring.valuation (Valuation.valuationSubring v))

source

@[simp]

theorem ValuationSubring.valuationSubring_valuation {K : Type u} [Field K] (A : ValuationSubring K) :

Valuation.valuationSubring (ValuationSubring.valuation A) = A

source

def ValuationSubring.unitGroup {K : Type u} [Field K] (A : ValuationSubring K) :

Subgroup Kˣ

The unit group of a valuation subring, as a subgroup of Kˣ.

Instances For

source

@[simp]

theorem ValuationSubring.mem_unitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) :

x ∈ ValuationSubring.unitGroup A ↔ ↑(ValuationSubring.valuation A) ↑x = 1

source

def ValuationSubring.unitGroupMulEquiv {K : Type u} [Field K] (A : ValuationSubring K) :

{ x // x ∈ ValuationSubring.unitGroup A } ≃* { x // x ∈ A }ˣ

For a valuation subring A, A.unitGroup agrees with the units of A.

Instances For

source

@[simp]

theorem ValuationSubring.coe_unitGroupMulEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ ValuationSubring.unitGroup A }) :

↑↑(↑(ValuationSubring.unitGroupMulEquiv A) a) = ↑↑a

source

@[simp]

theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ A }ˣ) :

↑↑(↑(MulEquiv.symm (ValuationSubring.unitGroupMulEquiv A)) a) = ↑↑a

source

theorem ValuationSubring.unitGroup_le_unitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

ValuationSubring.unitGroup A ≤ ValuationSubring.unitGroup B ↔ A ≤ B

source

theorem ValuationSubring.unitGroup_injective {K : Type u} [Field K] :

Function.Injective ValuationSubring.unitGroup

source

theorem ValuationSubring.eq_iff_unitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

A = B ↔ ValuationSubring.unitGroup A = ValuationSubring.unitGroup B

source

def ValuationSubring.unitGroupOrderEmbedding {K : Type u} [Field K] :

ValuationSubring K ↪o Subgroup Kˣ

The map on valuation subrings to their unit groups is an order embedding.

Instances For

source

theorem ValuationSubring.unitGroup_strictMono {K : Type u} [Field K] :

StrictMono ValuationSubring.unitGroup

source

def ValuationSubring.nonunits {K : Type u} [Field K] (A : ValuationSubring K) :

Subsemigroup K

The nonunits of a valuation subring of K, as a subsemigroup of K

Instances For

source

theorem ValuationSubring.mem_nonunits_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : K} :

x ∈ ValuationSubring.nonunits A ↔ ↑(ValuationSubring.valuation A) x < 1

source

theorem ValuationSubring.nonunits_le_nonunits {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

ValuationSubring.nonunits B ≤ ValuationSubring.nonunits A ↔ A ≤ B

source

theorem ValuationSubring.nonunits_injective {K : Type u} [Field K] :

Function.Injective ValuationSubring.nonunits

source

theorem ValuationSubring.nonunits_inj {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

ValuationSubring.nonunits A = ValuationSubring.nonunits B ↔ A = B

source

def ValuationSubring.nonunitsOrderEmbedding {K : Type u} [Field K] :

ValuationSubring K ↪o (Subsemigroup K)ᵒᵈ

The map on valuation subrings to their nonunits is a dual order embedding.

Instances For

source

theorem ValuationSubring.coe_mem_nonunits_iff {K : Type u} [Field K] {A : ValuationSubring K} {a : { x // x ∈ A }} :

↑a ∈ ValuationSubring.nonunits A ↔ a ∈ LocalRing.maximalIdeal { x // x ∈ A }

The elements of A.nonunits are those of the maximal ideal of A after coercion to K.

See also mem_nonunits_iff_exists_mem_maximalIdeal, which gets rid of the coercion to K, at the expense of a more complicated right hand side.

source

theorem ValuationSubring.nonunits_le {K : Type u} [Field K] {A : ValuationSubring K} :

ValuationSubring.nonunits A ≤ A.toSubsemigroup

source

theorem ValuationSubring.nonunits_subset {K : Type u} [Field K] {A : ValuationSubring K} :

↑(ValuationSubring.nonunits A) ⊆ ↑A

source

theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} {a : K} :

a ∈ ValuationSubring.nonunits A ↔ ∃ ha, { val := a, property := ha } ∈ LocalRing.maximalIdeal { x // x ∈ A }

The elements of A.nonunits are those of the maximal ideal of A.

See also coe_mem_nonunits_iff, which has a simpler right hand side but requires the element to be in A already.

source

theorem ValuationSubring.image_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} :

Subtype.val '' ↑(LocalRing.maximalIdeal { x // x ∈ A }) = ↑(ValuationSubring.nonunits A)

A.nonunits agrees with the maximal ideal of A, after taking its image in K.

source

def ValuationSubring.principalUnitGroup {K : Type u} [Field K] (A : ValuationSubring K) :

Subgroup Kˣ

The principal unit group of a valuation subring, as a subgroup of Kˣ.

Instances For

source

theorem ValuationSubring.principal_units_le_units {K : Type u} [Field K] (A : ValuationSubring K) :

ValuationSubring.principalUnitGroup A ≤ ValuationSubring.unitGroup A

source

theorem ValuationSubring.mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) :

x ∈ ValuationSubring.principalUnitGroup A ↔ ↑(ValuationSubring.valuation A) (↑x - 1) < 1

source

theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

ValuationSubring.principalUnitGroup B ≤ ValuationSubring.principalUnitGroup A ↔ A ≤ B

source

theorem ValuationSubring.principalUnitGroup_injective {K : Type u} [Field K] :

Function.Injective ValuationSubring.principalUnitGroup

source

theorem ValuationSubring.eq_iff_principalUnitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :

A = B ↔ ValuationSubring.principalUnitGroup A = ValuationSubring.principalUnitGroup B

source

def ValuationSubring.principalUnitGroupOrderEmbedding {K : Type u} [Field K] :

ValuationSubring K ↪o (Subgroup Kˣ)ᵒᵈ

The map on valuation subrings to their principal unit groups is an order embedding.

Instances For

source

theorem ValuationSubring.coe_mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : { x // x ∈ ValuationSubring.unitGroup A }} :

↑x ∈ ValuationSubring.principalUnitGroup A ↔ ↑(ValuationSubring.unitGroupMulEquiv A) x ∈ MonoidHom.ker (Units.map ↑(LocalRing.residue { x // x ∈ A }))

source

def ValuationSubring.principalUnitGroupEquiv {K : Type u} [Field K] (A : ValuationSubring K) :

{ x // x ∈ ValuationSubring.principalUnitGroup A } ≃* { x // x ∈ MonoidHom.ker (Units.map ↑(LocalRing.residue { x // x ∈ A })) }

The principal unit group agrees with the kernel of the canonical map from the units of A to the units of the residue field of A.

Instances For

source

@[simp]

theorem ValuationSubring.principalUnitGroupEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ ValuationSubring.principalUnitGroup A }) :

↑↑↑(↑(ValuationSubring.principalUnitGroupEquiv A) a) = ↑↑a

source

@[simp]

theorem ValuationSubring.principalUnitGroup_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : { x // x ∈ MonoidHom.ker (Units.map ↑(LocalRing.residue { x // x ∈ A })) }) :

↑↑(↑(MulEquiv.symm (ValuationSubring.principalUnitGroupEquiv A)) a) = ↑↑↑a

source

def ValuationSubring.unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :

{ x // x ∈ ValuationSubring.unitGroup A } →* (LocalRing.ResidueField { x // x ∈ A })ˣ

The canonical map from the unit group of A to the units of the residue field of A.

Instances For

source

@[simp]

theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : { x // x ∈ ValuationSubring.unitGroup A }) :

↑(↑(ValuationSubring.unitGroupToResidueFieldUnits A) x) = ↑(Ideal.Quotient.mk (LocalRing.maximalIdeal { x // x ∈ A })) ↑(↑(ValuationSubring.unitGroupMulEquiv A) x)

source

theorem ValuationSubring.ker_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :

MonoidHom.ker (ValuationSubring.unitGroupToResidueFieldUnits A) = Subgroup.comap (Subgroup.subtype (ValuationSubring.unitGroup A)) (ValuationSubring.principalUnitGroup A)

source

theorem ValuationSubring.surjective_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :

Function.Surjective ↑(ValuationSubring.unitGroupToResidueFieldUnits A)

source

def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :

{ x // x ∈ ValuationSubring.unitGroup A } ⧸ Subgroup.comap (Subgroup.subtype (ValuationSubring.unitGroup A)) (ValuationSubring.principalUnitGroup A) ≃* (LocalRing.ResidueField { x // x ∈ A })ˣ

The quotient of the unit group of A by the principal unit group of A agrees with the units of the residue field of A.

Instances For

source

def ValuationSubring.instMulOneClassQuotientSubtypeUnitsToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldMemSubgroupInstGroupUnitsInstMembershipInstSetLikeSubgroupUnitGroupToGroupInstHasQuotientSubgroupComapSubtypePrincipalUnitGroup {K : Type u} [Field K] (A : ValuationSubring K) :

MulOneClass ({ x // x ∈ ValuationSubring.unitGroup A } ⧸ Subgroup.comap (Subgroup.subtype (ValuationSubring.unitGroup A)) (ValuationSubring.principalUnitGroup A))

Instances For

source

theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk {K : Type u} [Field K] (A : ValuationSubring K) :

MonoidHom.comp (MulEquiv.toMonoidHom (ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits A)) (QuotientGroup.mk' (Subgroup.comap (Subgroup.subtype (ValuationSubring.unitGroup A)) (ValuationSubring.principalUnitGroup A))) = ValuationSubring.unitGroupToResidueFieldUnits A

source

@[simp]

theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : { x // x ∈ ValuationSubring.unitGroup A }) :

↑(MulEquiv.toMonoidHom (ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits A)) ↑x = ↑(ValuationSubring.unitGroupToResidueFieldUnits A) x

Pointwise actions #

This transfers the action from Subring.pointwiseMulAction, noting that it only applies when the action is by a group. Notably this provides an instances when G is K ≃+* K.

These instances are in the Pointwise locale.

The lemmas in this section are copied from RingTheory/Subring/Pointwise.lean; try to keep these in sync.

source

def ValuationSubring.pointwiseHasSMul {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] :

SMul G (ValuationSubring K)

The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Instances For

source

@[simp]

theorem ValuationSubring.coe_pointwise_smul {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (S : ValuationSubring K) :

↑(g • S) = g • ↑S

source

@[simp]

theorem ValuationSubring.pointwise_smul_toSubring {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (S : ValuationSubring K) :

(g • S).toSubring = g • S.toSubring

source

def ValuationSubring.pointwiseMulAction {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] :

MulAction G (ValuationSubring K)

The action on a valuation subring corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

This is a stronger version of ValuationSubring.pointwiseSMul.

Instances For

source

theorem ValuationSubring.smul_mem_pointwise_smul {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (x : K) (S : ValuationSubring K) :

x ∈ S → g • x ∈ g • S

source

theorem ValuationSubring.mem_smul_pointwise_iff_exists {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (x : K) (S : ValuationSubring K) :

x ∈ g • S ↔ ∃ s, s ∈ S ∧ g • s = x

source

instance ValuationSubring.pointwise_central_scalar {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] [MulSemiringAction Gᵐᵒᵖ K] [IsCentralScalar G K] :

IsCentralScalar G (ValuationSubring K)

source

@[simp]

theorem ValuationSubring.smul_mem_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :

g • x ∈ g • S ↔ x ∈ S

source

theorem ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :

x ∈ g • S ↔ g⁻¹ • x ∈ S

source

theorem ValuationSubring.mem_inv_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :

x ∈ g⁻¹ • S ↔ g • x ∈ S

source

@[simp]

theorem ValuationSubring.pointwise_smul_le_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {T : ValuationSubring K} :

g • S ≤ g • T ↔ S ≤ T

source

theorem ValuationSubring.pointwise_smul_subset_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {T : ValuationSubring K} :

g • S ≤ T ↔ S ≤ g⁻¹ • T

source

theorem ValuationSubring.subset_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {T : ValuationSubring K} :

S ≤ g • T ↔ g⁻¹ • S ≤ T

source

def ValuationSubring.comap {K : Type u} [Field K] {L : Type u_1} [Field L] (A : ValuationSubring L) (f : K →+* L) :

ValuationSubring K

The pullback of a valuation subring A along a ring homomorphism K →+* L.

Instances For

source

@[simp]

theorem ValuationSubring.coe_comap {K : Type u} [Field K] {L : Type u_1} [Field L] (A : ValuationSubring L) (f : K →+* L) :

↑(ValuationSubring.comap A f) = ↑f ⁻¹' ↑A

source

@[simp]

theorem ValuationSubring.mem_comap {K : Type u} [Field K] {L : Type u_1} [Field L] {A : ValuationSubring L} {f : K →+* L} {x : K} :

x ∈ ValuationSubring.comap A f ↔ ↑f x ∈ A

source

theorem ValuationSubring.comap_comap {K : Type u} [Field K] {L : Type u_1} {J : Type u_2} [Field L] [Field J] (A : ValuationSubring J) (g : L →+* J) (f : K →+* L) :

ValuationSubring.comap (ValuationSubring.comap A g) f = ValuationSubring.comap A (RingHom.comp g f)

source

theorem Valuation.mem_unitGroup_iff (K : Type u) [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : Kˣ) :

x ∈ ValuationSubring.unitGroup (Valuation.valuationSubring v) ↔ ↑v ↑x = 1