# Valuation subrings of a field #

## Projects #

The order structure on `ValuationSubring K`.

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

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

This is equivalent to being maximal in the domination order of local subrings (the stacks project definition). See `LocalSubring.isMax_iff`.

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

Instances For

source
instance ValuationSubring.instSetLike {K : Type u} [Field K] :
SetLike (ValuationSubring K) K
Equations

- ValuationSubring.instSetLike = { coe := fun (A : ValuationSubring K) => ↑A.toSubring, coe_injective' := ⋯ }

source
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 B : ValuationSubring K) (h : ∀ (x : K), x ∈ A ↔ x ∈ B) :
A = B
source
theorem ValuationSubring.ext_iff {K : Type u} [Field K] {A B : ValuationSubring K} :
A = B ↔ ∀ (x : K), x ∈ A ↔ x ∈ 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 y : K) :
x ∈ A → y ∈ A → x + y ∈ A
source
theorem ValuationSubring.mul_mem {K : Type u} [Field K] (A : ValuationSubring K) (x 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.instSubringClass {K : Type u} [Field K] :
SubringClass (ValuationSubring K) K
source
theorem ValuationSubring.toSubring_injective {K : Type u} [Field K] :
Function.Injective toSubring
source
instance ValuationSubring.instCommRingSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) :
CommRing ↥A
Equations

- A.instCommRingSubtypeMem = inferInstanceAs (CommRing ↥A.toSubring)

source
instance ValuationSubring.instIsDomainSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) :
IsDomain ↥A
source
instance ValuationSubring.instTop {K : Type u} [Field K] :
Top (ValuationSubring K)
Equations

- ValuationSubring.instTop = { top := let __src := ⊤; { toSubring := __src, mem_or_inv_mem' := ⋯ } }

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.instOrderTop {K : Type u} [Field K] :
OrderTop (ValuationSubring K)
Equations

- ValuationSubring.instOrderTop = { toTop := ValuationSubring.instTop, le_top := ⋯ }

source
instance ValuationSubring.instInhabited {K : Type u} [Field K] :
Inhabited (ValuationSubring K)
Equations

- ValuationSubring.instInhabited = { default := ⊤ }

source
instance ValuationSubring.instValuationRingSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) :
ValuationRing ↥A
source
instance ValuationSubring.instAlgebraSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) :
Algebra (↥A) K
Equations

- A.instAlgebraSubtypeMem = inferInstanceAs (Algebra (↥A.toSubring) K)

source
instance ValuationSubring.isLocalRing {K : Type u} [Field K] (A : ValuationSubring K) :
IsLocalRing ↥A
source
@[simp]
theorem ValuationSubring.algebraMap_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) :
(algebraMap (↥A) K) a = ↑a
source
instance ValuationSubring.instIsFractionRingSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) :
IsFractionRing (↥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.

Equations

- A.ValueGroup = ValuationRing.ValueGroup (↥A) K

Instances For

source
instance ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup {K : Type u_1} [Field K] (A : ValuationSubring K) :
LinearOrderedCommGroupWithZero A.ValueGroup
Equations

- A.instLinearOrderedCommGroupWithZeroValueGroup = ValuationRing.linearOrderedCommGroupWithZero (↥A) K

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

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

Equations

- A.valuation = ValuationRing.valuation (↥A) K

Instances For

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

- A.inhabitedValueGroup = { default := A.valuation 0 }

source
theorem ValuationSubring.valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) :
A.valuation ↑a ≤ 1
source
theorem ValuationSubring.mem_of_valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (h : A.valuation x ≤ 1) :
x ∈ A
source
theorem ValuationSubring.valuation_le_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
A.valuation x ≤ 1 ↔ x ∈ A
source
theorem ValuationSubring.valuation_eq_iff {K : Type u} [Field K] (A : ValuationSubring K) (x y : K) :
A.valuation x = A.valuation y ↔ ∃ (a : (↥A)ˣ), ↑↑a * y = x
source
theorem ValuationSubring.valuation_le_iff {K : Type u} [Field K] (A : ValuationSubring K) (x y : K) :
A.valuation x ≤ A.valuation y ↔ ∃ (a : ↥A), ↑a * y = x
source
theorem ValuationSubring.valuation_surjective {K : Type u} [Field K] (A : ValuationSubring K) :
Function.Surjective ⇑A.valuation
source
theorem ValuationSubring.valuation_unit {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) :
A.valuation ↑↑a = 1
source
theorem ValuationSubring.valuation_eq_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) :
IsUnit a ↔ A.valuation ↑a = 1
source
theorem ValuationSubring.valuation_lt_one_or_eq_one {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) :
A.valuation ↑a < 1 ∨ A.valuation ↑a = 1
source
theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) :
a ∈ IsLocalRing.maximalIdeal ↥A ↔ A.valuation ↑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`.

Equations

- ValuationSubring.ofSubring R hR = { toSubring := R, mem_or_inv_mem' := hR }

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 ∈ 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.

Equations

- R.ofLE S h = { toSubring := S, mem_or_inv_mem' := ⋯ }

Instances For

source
instance ValuationSubring.instSemilatticeSup {K : Type u} [Field K] :
SemilatticeSup (ValuationSubring K)
Equations

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

source
def ValuationSubring.inclusion {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
↥R →+* ↥S

The ring homomorphism induced by the partial order.

Equations

- R.inclusion S h = Subring.inclusion h

Instances For

source
def ValuationSubring.subtype {K : Type u} [Field K] (R : ValuationSubring K) :
↥R →+* K

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

Equations

- R.subtype = R.subtype

Instances For

source
@[simp]
theorem ValuationSubring.subtype_apply {K : Type u} [Field K] {R : ValuationSubring K} (x : ↥R) :
R.subtype x = ↑x
source
theorem ValuationSubring.subtype_injective {K : Type u} [Field K] (R : ValuationSubring K) :
Function.Injective ⇑R.subtype
source
@[simp]
theorem ValuationSubring.coe_subtype {K : Type u} [Field K] (R : ValuationSubring K) :
⇑R.subtype = Subtype.val
source
def ValuationSubring.mapOfLE {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
R.ValueGroup →*₀ S.ValueGroup

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

Equations

- R.mapOfLE S h = { toFun := Quotient.map' id ⋯, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
theorem ValuationSubring.monotone_mapOfLE {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
Monotone ⇑(R.mapOfLE S h)
source
@[simp]
theorem ValuationSubring.mapOfLE_comp_valuation {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation
source
@[simp]
theorem ValuationSubring.mapOfLE_valuation_apply {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) (x : K) :
(R.mapOfLE S h) (R.valuation x) = S.valuation x
source
def ValuationSubring.idealOfLE {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
Ideal ↥R

The ideal corresponding to a coarsening of a valuation ring.

Equations

- R.idealOfLE S h = Ideal.comap (R.inclusion S h) (IsLocalRing.maximalIdeal ↥S)

Instances For

source
instance ValuationSubring.prime_idealOfLE {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
(R.idealOfLE S h).IsPrime
source
def ValuationSubring.ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
ValuationSubring K

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

Equations

- A.ofPrime P = A.ofLE (Localization.subalgebra.ofField K P.primeCompl ⋯).toSubring ⋯

Instances For

source
instance ValuationSubring.ofPrimeAlgebra {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
Algebra ↥A ↥(A.ofPrime P)
Equations

- A.ofPrimeAlgebra P = (Localization.subalgebra.ofField K P.primeCompl ⋯).algebra

source
instance ValuationSubring.ofPrime_scalar_tower {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
IsScalarTower (↥A) (↥(A.ofPrime P)) K
source
instance ValuationSubring.ofPrime_localization {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
IsLocalization.AtPrime (↥(A.ofPrime P)) P
source
theorem ValuationSubring.le_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
A ≤ A.ofPrime P
source
theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] (x : ↥A) :
(A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl
source
@[simp]
theorem ValuationSubring.idealOfLE_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] :
A.idealOfLE (A.ofPrime P) ⋯ = P
source
@[simp]
theorem ValuationSubring.ofPrime_idealOfLE {K : Type u} [Field K] (R S : ValuationSubring K) (h : R ≤ S) :
R.ofPrime (R.idealOfLE S h) = S
source
theorem ValuationSubring.ofPrime_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (P Q : Ideal ↥A) [P.IsPrime] [Q.IsPrime] (h : P ≤ Q) :
A.ofPrime Q ≤ A.ofPrime P
source
theorem ValuationSubring.idealOfLE_le_of_le {K : Type u} [Field K] (A R S : ValuationSubring K) (hR : A ≤ R) (hS : A ≤ S) (h : R ≤ S) :
A.idealOfLE S hS ≤ A.idealOfLE R hR
source
def ValuationSubring.primeSpectrumEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
PrimeSpectrum ↥A ≃ { S : ValuationSubring K // A ≤ S }

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

Equations

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

Instances For

source
@[simp]
theorem ValuationSubring.primeSpectrumEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum ↥A) :
A.primeSpectrumEquiv P = ⟨A.ofPrime P.asIdeal, ⋯⟩
source
def ValuationSubring.primeSpectrumOrderEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
(PrimeSpectrum ↥A)ᵒᵈ ≃o { S : ValuationSubring K // A ≤ S }

An ordered variant of `primeSpectrumEquiv`.

Equations

- A.primeSpectrumOrderEquiv = { toEquiv := OrderDual.ofDual.trans A.primeSpectrumEquiv, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal {K : Type u} [Field K] (A : ValuationSubring K) (a✝ : { S : ValuationSubring K // A ≤ S }) :
↑((RelIso.symm A.primeSpectrumOrderEquiv) a✝).asIdeal = ⇑(A.inclusion ↑a✝ ⋯) ⁻¹' ↑(IsLocalRing.maximalIdeal ↥↑a✝)
source
@[simp]
theorem ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier {K : Type u} [Field K] (A : ValuationSubring K) (a✝ : (PrimeSpectrum ↥A)ᵒᵈ) :
↑↑(A.primeSpectrumOrderEquiv a✝) = {x : K | ∃ a ∈ A, ∃ (a_1 : K), (∃ (x : a_1 ∈ A), ⟨a_1, ⋯⟩ ∉ (OrderDual.ofDual a✝).asIdeal) ∧ x = a * a_1⁻¹}
source
instance ValuationSubring.le_total_ideal {K : Type u} [Field K] (A : ValuationSubring K) :
IsTotal { S : ValuationSubring K // A ≤ S } LE.le
source
instance ValuationSubring.linearOrderOverring {K : Type u} [Field K] (A : ValuationSubring K) :
LinearOrder { S : ValuationSubring K // A ≤ S }
Equations

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

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.

Equations

- v.valuationSubring = { toSubring := v.integer, mem_or_inv_mem' := ⋯ }

Instances For

source
@[simp]
theorem Valuation.mem_valuationSubring_iff {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : K) :
x ∈ v.valuationSubring ↔ 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 Γ₂) :
v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring
source
theorem Valuation.isEquiv_valuation_valuationSubring {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) :
v.IsEquiv v.valuationSubring.valuation
source
theorem Valuation.valuationSubring.integers {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) :
v.Integers ↥v.valuationSubring
source
@[simp]
theorem ValuationSubring.valuationSubring_valuation {K : Type u} [Field K] (A : ValuationSubring K) :
A.valuation.valuationSubring = 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ˣ`.

Equations

- A.unitGroup = ((↑A.valuation.toMonoidWithZeroHom).comp (Units.coeHom K)).ker

Instances For

source
@[simp]
theorem ValuationSubring.mem_unitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K ˣ) :
x ∈ A.unitGroup ↔ A.valuation ↑x = 1
source
def ValuationSubring.unitGroupMulEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
↥A.unitGroup ≃* (↥A)ˣ

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

Equations

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

Instances For

source
@[simp]
theorem ValuationSubring.coe_unitGroupMulEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A.unitGroup) :
↑↑(A.unitGroupMulEquiv a) = ↑↑a
source
@[simp]
theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) :
↑↑(A.unitGroupMulEquiv.symm a) = ↑↑a
source
theorem ValuationSubring.unitGroup_le_unitGroup {K : Type u} [Field K] {A B : ValuationSubring K} :
A.unitGroup ≤ B.unitGroup ↔ A ≤ B
source
theorem ValuationSubring.unitGroup_injective {K : Type u} [Field K] :
Function.Injective unitGroup
source
theorem ValuationSubring.eq_iff_unitGroup {K : Type u} [Field K] {A B : ValuationSubring K} :
A = B ↔ A.unitGroup = B.unitGroup
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.

Equations

- ValuationSubring.unitGroupOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.unitGroup, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source
theorem ValuationSubring.unitGroup_strictMono {K : Type u} [Field K] :
StrictMono 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`

Equations

- A.nonunits = { carrier := {x : K | A.valuation x < 1}, mul_mem' := ⋯ }

Instances For

source
theorem ValuationSubring.mem_nonunits_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : K} :
x ∈ A.nonunits ↔ A.valuation x < 1
source
theorem ValuationSubring.nonunits_le_nonunits {K : Type u} [Field K] {A B : ValuationSubring K} :
B.nonunits ≤ A.nonunits ↔ A ≤ B
source
theorem ValuationSubring.nonunits_injective {K : Type u} [Field K] :
Function.Injective nonunits
source
theorem ValuationSubring.nonunits_inj {K : Type u} [Field K] {A B : ValuationSubring K} :
A.nonunits = B.nonunits ↔ 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.

Equations

- ValuationSubring.nonunitsOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.nonunits, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source
theorem ValuationSubring.coe_mem_nonunits_iff {K : Type u} [Field K] {A : ValuationSubring K} {a : ↥A} :
↑a ∈ A.nonunits ↔ a ∈ IsLocalRing.maximalIdeal ↥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} :
A.nonunits ≤ A.toSubsemigroup
source
theorem ValuationSubring.nonunits_subset {K : Type u} [Field K] {A : ValuationSubring K} :
↑A.nonunits ⊆ ↑A
source
theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} {a : K} :
a ∈ A.nonunits ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥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 '' ↑(IsLocalRing.maximalIdeal ↥A) = ↑A.nonunits

`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ˣ`.

Equations

- A.principalUnitGroup = { carrier := {x : K ˣ | A.valuation (↑x - 1) < 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source
theorem ValuationSubring.principal_units_le_units {K : Type u} [Field K] (A : ValuationSubring K) :
A.principalUnitGroup ≤ A.unitGroup
source
theorem ValuationSubring.mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K ˣ) :
x ∈ A.principalUnitGroup ↔ A.valuation (↑x - 1) < 1
source
theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup {K : Type u} [Field K] {A B : ValuationSubring K} :
B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B
source
theorem ValuationSubring.principalUnitGroup_injective {K : Type u} [Field K] :
Function.Injective principalUnitGroup
source
theorem ValuationSubring.eq_iff_principalUnitGroup {K : Type u} [Field K] {A B : ValuationSubring K} :
A = B ↔ A.principalUnitGroup = B.principalUnitGroup
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.

Equations

- ValuationSubring.principalUnitGroupOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.principalUnitGroup, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source
theorem ValuationSubring.coe_mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : ↥A.unitGroup} :
↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker
source
def ValuationSubring.principalUnitGroupEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
↥A.principalUnitGroup ≃* ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker

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`.

Equations

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

Instances For

source
theorem ValuationSubring.principalUnitGroupEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A.principalUnitGroup) :
↑↑↑(A.principalUnitGroupEquiv a) = ↑↑a
source
theorem ValuationSubring.principalUnitGroup_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker) :
↑↑(A.principalUnitGroupEquiv.symm a) = ↑↑↑a
source
def ValuationSubring.unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
↥A.unitGroup →* (IsLocalRing.ResidueField ↥A)ˣ

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

Equations

- A.unitGroupToResidueFieldUnits = (Units.map ↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom

Instances For

source
@[simp]
theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : ↥A.unitGroup) :
↑(A.unitGroupToResidueFieldUnits x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) ↑(A.unitGroupMulEquiv x)
source
theorem ValuationSubring.ker_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
source
theorem ValuationSubring.surjective_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
Function.Surjective ⇑A.unitGroupToResidueFieldUnits
source
def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃* (IsLocalRing.ResidueField ↥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`.

Equations

- A.unitsModPrincipalUnitsEquivResidueFieldUnits = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective A.unitGroupToResidueFieldUnits ⋯)

Instances For

source
theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk {K : Type u} [Field K] (A : ValuationSubring K) :
(↑A.unitsModPrincipalUnitsEquivResidueFieldUnits).comp (QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) = A.unitGroupToResidueFieldUnits
source
theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : ↥A.unitGroup) :
A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom ↑x = A.unitGroupToResidueFieldUnits 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 the file `Mathlib/Algebra/Ring/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.

Equations

- ValuationSubring.pointwiseHasSMul = { smul := fun (g : G) (S : ValuationSubring K) => let __src := g • S.toSubring; { toSubring := __src, mem_or_inv_mem' := ⋯ } }

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`.

Equations

- ValuationSubring.pointwiseMulAction = Function.Injective.mulAction ValuationSubring.toSubring ⋯ ⋯

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
instance ValuationSubring.instCovariantClassHSMulLe {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] :
CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le
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, 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 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 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 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`.

Equations

- A.comap f = { toSubring := Subring.comap f A.toSubring, mem_or_inv_mem' := ⋯ }

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) :
↑(A.comap 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 ∈ A.comap 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) :
(A.comap g).comap f = A.comap (g.comp f)
source
theorem Valuation.mem_unitGroup_iff (K : Type u) [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : K ˣ) :
x ∈ v.valuationSubring.unitGroup ↔ v ↑x = 1
source
theorem Valuation.mem_maximalIdeal_iff (K : Type u) [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) {a : ↥v.valuationSubring} :
a ∈ IsLocalRing.maximalIdeal ↥v.valuationSubring ↔ v ↑a < 1