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

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

Equations

• ValuationSubring.instSetLikeValuationSubring = { 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.instSubringClassValuationSubringToRingToDivisionRingInstSetLikeValuationSubring {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.instCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubring {K : Type u} [Field K] (A : ValuationSubring K) : CommRing ↥A

Equations

• ValuationSubring.instCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubring A = let_fun this := inferInstance; this

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

Equations

• ⋯ = ⋯

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

Equations

• ValuationSubring.instTopValuationSubring = { 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.instOrderTopValuationSubringToLEToPreorderInstPartialOrderInstSetLikeValuationSubring {K : Type u} [Field K] : OrderTop (ValuationSubring K)

Equations

• ValuationSubring.instOrderTopValuationSubringToLEToPreorderInstPartialOrderInstSetLikeValuationSubring = OrderTop.mk ⋯

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

Equations

• ValuationSubring.instInhabitedValuationSubring = { default := ⊤ }

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

Equations

• ⋯ = ⋯

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

Equations

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

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.instIsFractionRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringInstCommRingSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToCommRingToEuclideanDomainInstAlgebraSubtypeMemValuationSubringInstMembershipInstSetLikeValuationSubringToCommSemiringToCommSemiringToSemifieldToSubsemiringToRingToDivisionRingToSubringToSemiringToDivisionSemiring {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

• ValuationSubring.ValueGroup A = ValuationRing.ValueGroup (↥A) K

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

Equations

• ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup A = id inferInstance

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.

Equations

• ValuationSubring.valuation A = ValuationRing.valuation (↥A) K

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

Equations

• ValuationSubring.inhabitedValueGroup A = { default := (ValuationSubring.valuation A) 0 }

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

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

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

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)ˣ), ↑↑a * y = x

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), ↑a * y = x

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

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

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

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

theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : ↥A) : a ∈ LocalRing.maximalIdeal ↥A ↔ (ValuationSubring.valuation A) ↑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

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

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

Equations

• ValuationSubring.instSemilatticeSupValuationSubring = let __src := inferInstance; 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

• ValuationSubring.inclusion R 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

• ValuationSubring.subtype R = Subring.subtype R.toSubring

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.

Equations

• ValuationSubring.mapOfLE R S h = { toZeroHom := { 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 ⇑(ValuationSubring.mapOfLE R S h)

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

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

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

• ValuationSubring.idealOfLE R S h = Ideal.comap (ValuationSubring.inclusion R S h) (LocalRing.maximalIdeal ↥S)

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)

Equations

• ⋯ = ⋯

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

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

Equations

• ValuationSubring.ofPrime A P = ValuationSubring.ofLE A (Subalgebra.toSubring (Localization.subalgebra.ofField K (Ideal.primeCompl P) ⋯)) ⋯

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

Equations

• ValuationSubring.ofPrimeAlgebra A P = Subalgebra.algebra (Localization.subalgebra.ofField K (Ideal.primeCompl P) ⋯)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) [Ideal.IsPrime P] (x : ↥A) : (ValuationSubring.valuation (ValuationSubring.ofPrime A P)) ↑x = 1 ↔ x ∈ Ideal.primeCompl P

@[simp]

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

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

theorem ValuationSubring.ofPrime_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal ↥A) (Q : Ideal ↥A) [Ideal.IsPrime P] [Ideal.IsPrime Q] (h : P ≤ Q) : ValuationSubring.ofPrime A Q ≤ ValuationSubring.ofPrime A 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) : ValuationSubring.idealOfLE A S hS ≤ ValuationSubring.idealOfLE A R hR

@[simp]

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

@[simp]

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

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.primeSpectrumOrderEquiv_symm_apply_asIdeal_carrier {K : Type u} [Field K] (A : ValuationSubring K) (S : { S : ValuationSubring K // A ≤ S }) : ↑((RelIso.symm (ValuationSubring.primeSpectrumOrderEquiv A)) S).asIdeal = ⇑(ValuationSubring.inclusion A ↑S ⋯) ⁻¹' ↑(LocalRing.maximalIdeal ↥↑S)

@[simp]

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

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

• ValuationSubring.primeSpectrumOrderEquiv A = let __src := ValuationSubring.primeSpectrumEquiv A; { toEquiv := __src, map_rel_iff' := ⋯ }

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

Equations

• ValuationSubring.linearOrderOverring A = let __src := inferInstance; 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

• Valuation.valuationSubring v = let __src := Valuation.integer v; { toSubring := __src, 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 ∈ Valuation.valuationSubring v ↔ 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 Γ₂) : Valuation.IsEquiv v₁ v₂ ↔ Valuation.valuationSubring v₁ = Valuation.valuationSubring v₂

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

@[simp]

theorem ValuationSubring.valuationSubring_valuation {K : Type u} [Field K] (A : ValuationSubring K) : Valuation.valuationSubring (ValuationSubring.valuation A) = 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

• ValuationSubring.unitGroup A = MonoidHom.ker (MonoidHom.comp (↑(ValuationSubring.valuation A).toMonoidWithZeroHom) (Units.coeHom K))

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

def ValuationSubring.unitGroupMulEquiv {K : Type u} [Field K] (A : ValuationSubring K) : ↥(ValuationSubring.unitGroup A) ≃* (↥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 : ↥(ValuationSubring.unitGroup A)) : ↑↑((ValuationSubring.unitGroupMulEquiv A) a) = ↑↑a

@[simp]

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

theorem ValuationSubring.unitGroup_le_unitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} : ValuationSubring.unitGroup A ≤ ValuationSubring.unitGroup B ↔ 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 ↔ ValuationSubring.unitGroup A = ValuationSubring.unitGroup B

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 = { toEmbedding := { toFun := fun (A : ValuationSubring K) => ValuationSubring.unitGroup A, 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

• ValuationSubring.nonunits A = { carrier := {x : K | (ValuationSubring.valuation A) x < 1}, mul_mem' := ⋯ }

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

theorem ValuationSubring.nonunits_le_nonunits {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} : ValuationSubring.nonunits B ≤ ValuationSubring.nonunits A ↔ 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} : ValuationSubring.nonunits A = ValuationSubring.nonunits B ↔ 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 = { toEmbedding := { toFun := fun (A : ValuationSubring K) => ValuationSubring.nonunits A, inj' := ⋯ }, map_rel_iff' := ⋯ }

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

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

theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} {a : K} : a ∈ ValuationSubring.nonunits A ↔ ∃ (ha : a ∈ A), { val := a, property := 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) = ↑(ValuationSubring.nonunits A)

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

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

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

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

theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} : ValuationSubring.principalUnitGroup B ≤ ValuationSubring.principalUnitGroup A ↔ 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 ↔ ValuationSubring.principalUnitGroup A = ValuationSubring.principalUnitGroup B

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 = { toEmbedding := { toFun := fun (A : ValuationSubring K) => ValuationSubring.principalUnitGroup A, inj' := ⋯ }, map_rel_iff' := ⋯ }

theorem ValuationSubring.coe_mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : ↥(ValuationSubring.unitGroup A)} : ↑x ∈ ValuationSubring.principalUnitGroup A ↔ (ValuationSubring.unitGroupMulEquiv A) x ∈ MonoidHom.ker (Units.map ↑(LocalRing.residue ↥A))

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

Equations

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

@[simp]

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

@[simp]

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

def ValuationSubring.unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) : ↥(ValuationSubring.unitGroup A) →* (LocalRing.ResidueField ↥A)ˣ

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

Equations

• ValuationSubring.unitGroupToResidueFieldUnits A = MonoidHom.comp (Units.map ↑(Ideal.Quotient.mk (LocalRing.maximalIdeal ↥A))) (MulEquiv.toMonoidHom (ValuationSubring.unitGroupMulEquiv A))

@[simp]

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

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)

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

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

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

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

Porting note: Lean needs to be reminded of this instance

Equations

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

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

@[simp]

theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply {K : Type u} [Field K] (A : ValuationSubring K) (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.

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

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

• ValuationSubring.comap A f = let __src := Subring.comap f A.toSubring; { toSubring := __src, 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) : ↑(ValuationSubring.comap A 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 ∈ ValuationSubring.comap A 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) : ValuationSubring.comap (ValuationSubring.comap A g) f = ValuationSubring.comap A (RingHom.comp g f)

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