Valuation subrings of a field

Projects

The order structure on ValuationSubring K.

structure ValuationSubring (K : Type u) [Field K] extends Subring : 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.

• 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

theorem ValuationSubring.mem_or_inv_mem' {K : Type u} [Field K] (self : ValuationSubring K) (x : K) : x ∈ self.carrier ∨ x⁻¹ ∈ self.carrier

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

instance ValuationSubring.instSubringClass {K : Type u} [Field K] : SubringClass (ValuationSubring K) K

Equations

• ⋯ = ⋯

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

instance ValuationSubring.instCommRingSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) : CommRing ↥A

Equations

• A.instCommRingSubtypeMem = inferInstance

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

Equations

• ⋯ = ⋯

instance ValuationSubring.instTop {K : Type u} [Field K] : Top (ValuationSubring K)

Equations

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

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

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

instance ValuationSubring.instOrderTop {K : Type u} [Field K] : OrderTop (ValuationSubring K)

Equations

• ValuationSubring.instOrderTop = OrderTop.mk ⋯

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

Equations

• ValuationSubring.instInhabited = { default := ⊤ }

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

Equations

• ⋯ = ⋯

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

Equations

• A.instAlgebraSubtypeMem = inferInstance

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

Equations

• ⋯ = ⋯

@[simp]

theorem ValuationSubring.algebraMap_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) : (algebraMap (↥A) K) a = ↑a

instance ValuationSubring.instIsFractionRingSubtypeMem {K : Type u} [Field K] (A : ValuationSubring K) : IsFractionRing (↥A) K

Equations

• ⋯ = ⋯

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

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

Equations

• A.instLinearOrderedCommGroupWithZeroValueGroup = id inferInstance

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

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

Equations

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

theorem ValuationSubring.valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) : A.valuation ↑a ≤ 1

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

theorem ValuationSubring.valuation_le_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) : A.valuation x ≤ 1 ↔ x ∈ A

theorem ValuationSubring.valuation_eq_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) : A.valuation x = A.valuation y ↔ ∃ (a : (↥A)ˣ), ↑↑a * y = x

theorem ValuationSubring.valuation_le_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) : A.valuation x ≤ A.valuation y ↔ ∃ (a : ↥A), ↑a * y = x

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

theorem ValuationSubring.valuation_unit {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) : A.valuation ↑↑a = 1

theorem ValuationSubring.valuation_eq_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) : IsUnit a ↔ A.valuation ↑a = 1

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

theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) : a ∈ LocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1

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 }

@[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

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' := ⋯ }

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

Equations

• ValuationSubring.instSemilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

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

The ring homomorphism induced by the partial order.

Equations

• R.inclusion S h = Subring.inclusion h

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

def ValuationSubring.mapOfLE {K : Type u} [Field K] (R : ValuationSubring K) (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' := ⋯ }

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

@[simp]

theorem ValuationSubring.mapOfLE_comp_valuation {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R ≤ S) : ⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation

@[simp]

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

def ValuationSubring.idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (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) (LocalRing.maximalIdeal ↥S)

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

Equations

• ⋯ = ⋯

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 ⋯

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

instance ValuationSubring.ofPrime_scalar_tower {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] : IsScalarTower (↥A) (↥(A.ofPrime P)) K

Equations

• ⋯ = ⋯

instance ValuationSubring.ofPrime_localization {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] : IsLocalization.AtPrime (↥(A.ofPrime P)) P

Equations

• ⋯ = ⋯

theorem ValuationSubring.le_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] : A ≤ A.ofPrime P

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

@[simp]

theorem ValuationSubring.idealOfLE_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [P.IsPrime] : A.idealOfLE (A.ofPrime P) ⋯ = P

@[simp]

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

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

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) : A.idealOfLE S hS ≤ A.idealOfLE R hR

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.

@[simp]

theorem ValuationSubring.primeSpectrumEquiv_apply_coe {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum ↥A) : ↑(A.primeSpectrumEquiv P) = A.ofPrime P.asIdeal

@[simp]

theorem ValuationSubring.primeSpectrumEquiv_symm_apply_asIdeal {K : Type u} [Field K] (A : ValuationSubring K) (S : { S : ValuationSubring K // A ≤ S }) : (A.primeSpectrumEquiv.symm S).asIdeal = A.idealOfLE ↑S ⋯

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 := A.primeSpectrumEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem ValuationSubring.primeSpectrumOrderEquiv_symm_apply_asIdeal_carrier {K : Type u} [Field K] (A : ValuationSubring K) (S : { S : ValuationSubring K // A ≤ S }) : ↑((RelIso.symm A.primeSpectrumOrderEquiv) S).asIdeal = ⇑(A.inclusion ↑S ⋯) ⁻¹' ↑(LocalRing.maximalIdeal ↥↑S)

@[simp]

theorem ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum ↥A) : ↑↑(A.primeSpectrumOrderEquiv P) = {x : K | ∃ a ∈ A, ∃ (a_1 : K), (∃ (x : a_1 ∈ A), ⟨a_1, ⋯⟩ ∈ P.asIdeal.primeCompl) ∧ x = a * a_1⁻¹}

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

Equations

• A.linearOrderOverring = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

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' := ⋯ }

@[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

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

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

@[simp]

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

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

@[simp]

theorem ValuationSubring.mem_unitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) : x ∈ A.unitGroup ↔ A.valuation ↑x = 1

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.

@[simp]

theorem ValuationSubring.coe_unitGroupMulEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A.unitGroup) : ↑↑(A.unitGroupMulEquiv a) = ↑↑a

@[simp]

theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) : ↑↑(A.unitGroupMulEquiv.symm a) = ↑↑a

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

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

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

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' := ⋯ }

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

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' := ⋯ }

theorem ValuationSubring.mem_nonunits_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : K} : x ∈ A.nonunits ↔ A.valuation x < 1

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

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

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

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' := ⋯ }

theorem ValuationSubring.coe_mem_nonunits_iff {K : Type u} [Field K] {A : ValuationSubring K} {a : ↥A} : ↑a ∈ A.nonunits ↔ a ∈ LocalRing.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.

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

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

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

theorem ValuationSubring.image_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} : Subtype.val '' ↑(LocalRing.maximalIdeal ↥A) = ↑A.nonunits

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

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' := ⋯ }

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

theorem ValuationSubring.mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) : x ∈ A.principalUnitGroup ↔ A.valuation (↑x - 1) < 1

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

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

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

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' := ⋯ }

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 ↑(LocalRing.residue ↥A)).ker

def ValuationSubring.principalUnitGroupEquiv {K : Type u} [Field K] (A : ValuationSubring K) : ↥A.principalUnitGroup ≃* ↥(Units.map ↑(LocalRing.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.

theorem ValuationSubring.principalUnitGroupEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A.principalUnitGroup) : ↑↑↑(A.principalUnitGroupEquiv a) = ↑↑a

theorem ValuationSubring.principalUnitGroup_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥(Units.map ↑(LocalRing.residue ↥A)).ker) : ↑↑(A.principalUnitGroupEquiv.symm a) = ↑↑↑a

def ValuationSubring.unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) : ↥A.unitGroup →* (LocalRing.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 (LocalRing.maximalIdeal ↥A))).comp A.unitGroupMulEquiv.toMonoidHom

@[simp]

theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : ↥A.unitGroup) : ↑(A.unitGroupToResidueFieldUnits x) = (Ideal.Quotient.mk (LocalRing.maximalIdeal ↥A)) ↑(A.unitGroupMulEquiv x)

theorem ValuationSubring.ker_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) : A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup

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

def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) : ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃* (LocalRing.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 ⋯)

def ValuationSubring.instMulOneClassQuotientSubtypeUnitsMemSubgroupUnitGroupComapSubtypePrincipalUnitGroup {K : Type u} [Field K] (A : ValuationSubring K) : MulOneClass (↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup)

Porting note: Lean needs to be reminded of this instance

Equations

• A.instMulOneClassQuotientSubtypeUnitsMemSubgroupUnitGroupComapSubtypePrincipalUnitGroup = inferInstance

theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk {K : Type u} [Field K] (A : ValuationSubring K) : A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom.comp (QuotientGroup.mk' (Subgroup.comap A.unitGroup.subtype A.principalUnitGroup)) = A.unitGroupToResidueFieldUnits

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; try to keep these in sync.

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' := ⋯ } }

@[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

@[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

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 ⋯ ⋯

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

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

Equations

• ⋯ = ⋯

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

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)

Equations

• ⋯ = ⋯

@[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

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

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

@[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

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

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

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' := ⋯ }

@[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

@[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

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)

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