# Valuation subrings of a field #

## Projects #

The order structure on ValuationSubring K.

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

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.carrierb self.carriera * b self.carrier
• one_mem' : 1 self.carrier
• add_mem' : ∀ {a b : K}, a self.carrierb self.carriera + 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
theorem ValuationSubring.mem_or_inv_mem' {K : Type u} [] (self : ) (x : K) :
x self.carrier x⁻¹ self.carrier
instance ValuationSubring.instSetLike {K : Type u} [] :
Equations
• ValuationSubring.instSetLike = { coe := fun (A : ) => A.toSubring, coe_injective' := }
@[simp]
theorem ValuationSubring.mem_carrier {K : Type u} [] (A : ) (x : K) :
x A.carrier x A
@[simp]
theorem ValuationSubring.mem_toSubring {K : Type u} [] (A : ) (x : K) :
x A.toSubring x A
theorem ValuationSubring.ext {K : Type u} [] (A : ) (B : ) (h : ∀ (x : K), x A x B) :
A = B
theorem ValuationSubring.zero_mem {K : Type u} [] (A : ) :
0 A
theorem ValuationSubring.one_mem {K : Type u} [] (A : ) :
1 A
theorem ValuationSubring.add_mem {K : Type u} [] (A : ) (x : K) (y : K) :
x Ay Ax + y A
theorem ValuationSubring.mul_mem {K : Type u} [] (A : ) (x : K) (y : K) :
x Ay Ax * y A
theorem ValuationSubring.neg_mem {K : Type u} [] (A : ) (x : K) :
x A-x A
theorem ValuationSubring.mem_or_inv_mem {K : Type u} [] (A : ) (x : K) :
x A x⁻¹ A
Equations
• =
theorem ValuationSubring.toSubring_injective {K : Type u} [] :
Function.Injective ValuationSubring.toSubring
instance ValuationSubring.instCommRingSubtypeMem {K : Type u} [] (A : ) :
Equations
• A.instCommRingSubtypeMem = let_fun this := inferInstance; this
instance ValuationSubring.instIsDomainSubtypeMem {K : Type u} [] (A : ) :
Equations
• =
instance ValuationSubring.instTop {K : Type u} [] :
Equations
• ValuationSubring.instTop = { top := let __src := ; { toSubring := __src, mem_or_inv_mem' := } }
theorem ValuationSubring.mem_top {K : Type u} [] (x : K) :
theorem ValuationSubring.le_top {K : Type u} [] (A : ) :
instance ValuationSubring.instOrderTop {K : Type u} [] :
Equations
• ValuationSubring.instOrderTop =
instance ValuationSubring.instInhabited {K : Type u} [] :
Equations
• ValuationSubring.instInhabited = { default := }
Equations
• =
instance ValuationSubring.instAlgebraSubtypeMem {K : Type u} [] (A : ) :
Algebra (A) K
Equations
• A.instAlgebraSubtypeMem = let_fun this := inferInstance; this
instance ValuationSubring.localRing {K : Type u} [] (A : ) :
Equations
• =
@[simp]
theorem ValuationSubring.algebraMap_apply {K : Type u} [] (A : ) (a : A) :
(algebraMap (A) K) a = a
Equations
• =
def ValuationSubring.ValueGroup {K : Type u} [] (A : ) :

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

Equations
• A.ValueGroup =
Instances For
Equations
• A.instLinearOrderedCommGroupWithZeroValueGroup = id inferInstance
def ValuationSubring.valuation {K : Type u} [] (A : ) :
Valuation K A.ValueGroup

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

Equations
• A.valuation =
Instances For
instance ValuationSubring.inhabitedValueGroup {K : Type u} [] (A : ) :
Inhabited A.ValueGroup
Equations
• A.inhabitedValueGroup = { default := A.valuation 0 }
theorem ValuationSubring.valuation_le_one {K : Type u} [] (A : ) (a : A) :
A.valuation a 1
theorem ValuationSubring.mem_of_valuation_le_one {K : Type u} [] (A : ) (x : K) (h : A.valuation x 1) :
x A
theorem ValuationSubring.valuation_le_one_iff {K : Type u} [] (A : ) (x : K) :
A.valuation x 1 x A
theorem ValuationSubring.valuation_eq_iff {K : Type u} [] (A : ) (x : K) (y : K) :
A.valuation x = A.valuation y ∃ (a : (A)ˣ), a * y = x
theorem ValuationSubring.valuation_le_iff {K : Type u} [] (A : ) (x : K) (y : K) :
A.valuation x A.valuation y ∃ (a : A), a * y = x
theorem ValuationSubring.valuation_surjective {K : Type u} [] (A : ) :
Function.Surjective A.valuation
theorem ValuationSubring.valuation_unit {K : Type u} [] (A : ) (a : (A)ˣ) :
A.valuation a = 1
theorem ValuationSubring.valuation_eq_one_iff {K : Type u} [] (A : ) (a : A) :
A.valuation a = 1
theorem ValuationSubring.valuation_lt_one_or_eq_one {K : Type u} [] (A : ) (a : A) :
A.valuation a < 1 A.valuation a = 1
theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [] (A : ) (a : A) :
A.valuation a < 1
def ValuationSubring.ofSubring {K : Type u} [] (R : ) (hR : ∀ (x : K), x R x⁻¹ R) :

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

Equations
• = { toSubring := R, mem_or_inv_mem' := hR }
Instances For
@[simp]
theorem ValuationSubring.mem_ofSubring {K : Type u} [] (R : ) (hR : ∀ (x : K), x R x⁻¹ R) (x : K) :
x R
def ValuationSubring.ofLE {K : Type u} [] (R : ) (S : ) (h : R.toSubring S) :

An overring of a valuation ring is a valuation ring.

Equations
• R.ofLE S h = { toSubring := S, mem_or_inv_mem' := }
Instances For
Equations
• ValuationSubring.instSemilatticeSup = let __src := inferInstance;
def ValuationSubring.inclusion {K : Type u} [] (R : ) (S : ) (h : R S) :
R →+* S

The ring homomorphism induced by the partial order.

Equations
• R.inclusion S h =
Instances For
def ValuationSubring.subtype {K : Type u} [] (R : ) :
R →+* K

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

Equations
• R.subtype = R.subtype
Instances For
def ValuationSubring.mapOfLE {K : Type u} [] (R : ) (S : ) (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 := , map_zero' := , map_one' := , map_mul' := }
Instances For
theorem ValuationSubring.monotone_mapOfLE {K : Type u} [] (R : ) (S : ) (h : R S) :
Monotone (R.mapOfLE S h)
@[simp]
theorem ValuationSubring.mapOfLE_comp_valuation {K : Type u} [] (R : ) (S : ) (h : R S) :
(R.mapOfLE S h) R.valuation = S.valuation
@[simp]
theorem ValuationSubring.mapOfLE_valuation_apply {K : Type u} [] (R : ) (S : ) (h : R S) (x : K) :
(R.mapOfLE S h) (R.valuation x) = S.valuation x
def ValuationSubring.idealOfLE {K : Type u} [] (R : ) (S : ) (h : R S) :
Ideal R

The ideal corresponding to a coarsening of a valuation ring.

Equations
Instances For
instance ValuationSubring.prime_idealOfLE {K : Type u} [] (R : ) (S : ) (h : R S) :
(R.idealOfLE S h).IsPrime
Equations
• =
def ValuationSubring.ofPrime {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :

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

Equations
Instances For
instance ValuationSubring.ofPrimeAlgebra {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :
Algebra A (A.ofPrime P)
Equations
instance ValuationSubring.ofPrime_scalar_tower {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :
IsScalarTower (A) ((A.ofPrime P)) K
Equations
• =
instance ValuationSubring.ofPrime_localization {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :
IsLocalization.AtPrime ((A.ofPrime P)) P
Equations
• =
theorem ValuationSubring.le_ofPrime {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :
A A.ofPrime P
theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] (x : A) :
(A.ofPrime P).valuation x = 1 x P.primeCompl
@[simp]
theorem ValuationSubring.idealOfLE_ofPrime {K : Type u} [] (A : ) (P : Ideal A) [P.IsPrime] :
A.idealOfLE (A.ofPrime P) = P
@[simp]
theorem ValuationSubring.ofPrime_idealOfLE {K : Type u} [] (R : ) (S : ) (h : R S) :
R.ofPrime (R.idealOfLE S h) = S
theorem ValuationSubring.ofPrime_le_of_le {K : Type u} [] (A : ) (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} [] (A : ) (R : ) (S : ) (hR : A R) (hS : A S) (h : R S) :
A.idealOfLE S hS A.idealOfLE R hR
@[simp]
theorem ValuationSubring.primeSpectrumEquiv_apply_coe {K : Type u} [] (A : ) (P : ) :
(A.primeSpectrumEquiv P) = A.ofPrime P.asIdeal
@[simp]
theorem ValuationSubring.primeSpectrumEquiv_symm_apply_asIdeal {K : Type u} [] (A : ) (S : { S : // A S }) :
(A.primeSpectrumEquiv.symm S).asIdeal = A.idealOfLE S
def ValuationSubring.primeSpectrumEquiv {K : Type u} [] (A : ) :
{ S : // 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
@[simp]
theorem ValuationSubring.primeSpectrumOrderEquiv_symm_apply_asIdeal_carrier {K : Type u} [] (A : ) (S : { S : // A S }) :
((RelIso.symm A.primeSpectrumOrderEquiv) S).asIdeal = (A.inclusion S ) ⁻¹' ()
@[simp]
theorem ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier {K : Type u} [] (A : ) (P : ) :
(A.primeSpectrumOrderEquiv P) = {x : K | aA, ∃ (a_1 : K), (∃ (x : a_1 A), a_1, P.asIdeal.primeCompl) x = a * a_1⁻¹}
def ValuationSubring.primeSpectrumOrderEquiv {K : Type u} [] (A : ) :
()ᵒᵈ ≃o { S : // A S }

An ordered variant of primeSpectrumEquiv.

Equations
• A.primeSpectrumOrderEquiv = let __src := A.primeSpectrumEquiv; { toEquiv := __src, map_rel_iff' := }
Instances For
instance ValuationSubring.linearOrderOverring {K : Type u} [] (A : ) :
LinearOrder { S : // A S }
Equations
• A.linearOrderOverring = let __src := inferInstance; LinearOrder.mk inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE
def Valuation.valuationSubring {K : Type u} [] {Γ : Type u_1} (v : ) :

The valuation subring associated to a valuation.

Equations
• v.valuationSubring = let __src := v.integer; { toSubring := __src, mem_or_inv_mem' := }
Instances For
@[simp]
theorem Valuation.mem_valuationSubring_iff {K : Type u} [] {Γ : Type u_1} (v : ) (x : K) :
x v.valuationSubring v x 1
theorem Valuation.isEquiv_iff_valuationSubring {K : Type u} [] {Γ₁ : Type u_2} {Γ₂ : Type u_3} (v₁ : Valuation K Γ₁) (v₂ : Valuation K Γ₂) :
v₁.IsEquiv v₂ v₁.valuationSubring = v₂.valuationSubring
theorem Valuation.isEquiv_valuation_valuationSubring {K : Type u} [] {Γ : Type u_1} (v : ) :
v.IsEquiv v.valuationSubring.valuation
@[simp]
theorem ValuationSubring.valuationSubring_valuation {K : Type u} [] (A : ) :
A.valuation.valuationSubring = A
def ValuationSubring.unitGroup {K : Type u} [] (A : ) :

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

Equations
• A.unitGroup = ((A.valuation.toMonoidWithZeroHom).comp ()).ker
Instances For
@[simp]
theorem ValuationSubring.mem_unitGroup_iff {K : Type u} [] (A : ) (x : Kˣ) :
x A.unitGroup A.valuation x = 1
def ValuationSubring.unitGroupMulEquiv {K : Type u} [] (A : ) :
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
@[simp]
theorem ValuationSubring.coe_unitGroupMulEquiv_apply {K : Type u} [] (A : ) (a : A.unitGroup) :
(A.unitGroupMulEquiv a) = a
@[simp]
theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply {K : Type u} [] (A : ) (a : (A)ˣ) :
(A.unitGroupMulEquiv.symm a) = a
theorem ValuationSubring.unitGroup_le_unitGroup {K : Type u} [] {A : } {B : } :
A.unitGroup B.unitGroup A B
theorem ValuationSubring.unitGroup_injective {K : Type u} [] :
Function.Injective ValuationSubring.unitGroup
theorem ValuationSubring.eq_iff_unitGroup {K : Type u} [] {A : } {B : } :
A = B A.unitGroup = B.unitGroup

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

Equations
• ValuationSubring.unitGroupOrderEmbedding = { toFun := fun (A : ) => A.unitGroup, inj' := , map_rel_iff' := }
Instances For
theorem ValuationSubring.unitGroup_strictMono {K : Type u} [] :
StrictMono ValuationSubring.unitGroup
def ValuationSubring.nonunits {K : Type u} [] (A : ) :

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

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

Equations
• ValuationSubring.nonunitsOrderEmbedding = { toFun := fun (A : ) => A.nonunits, inj' := , map_rel_iff' := }
Instances For
theorem ValuationSubring.coe_mem_nonunits_iff {K : Type u} [] {A : } {a : A} :
a A.nonunits

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} [] {A : } :
A.nonunits A.toSubsemigroup
theorem ValuationSubring.nonunits_subset {K : Type u} [] {A : } :
A.nonunits A
theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal {K : Type u} [] {A : } {a : K} :
a A.nonunits ∃ (ha : a A), a, ha

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} [] {A : } :
Subtype.val '' = A.nonunits

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

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

Equations
• A.principalUnitGroup = { carrier := {x : Kˣ | A.valuation (x - 1) < 1}, mul_mem' := , one_mem' := , inv_mem' := }
Instances For
theorem ValuationSubring.principal_units_le_units {K : Type u} [] (A : ) :
A.principalUnitGroup A.unitGroup
theorem ValuationSubring.mem_principalUnitGroup_iff {K : Type u} [] (A : ) (x : Kˣ) :
x A.principalUnitGroup A.valuation (x - 1) < 1
theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup {K : Type u} [] {A : } {B : } :
B.principalUnitGroup A.principalUnitGroup A B
theorem ValuationSubring.principalUnitGroup_injective {K : Type u} [] :
Function.Injective ValuationSubring.principalUnitGroup
theorem ValuationSubring.eq_iff_principalUnitGroup {K : Type u} [] {A : } {B : } :
A = B A.principalUnitGroup = B.principalUnitGroup

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

Equations
• ValuationSubring.principalUnitGroupOrderEmbedding = { toFun := fun (A : ) => A.principalUnitGroup, inj' := , map_rel_iff' := }
Instances For
theorem ValuationSubring.coe_mem_principalUnitGroup_iff {K : Type u} [] (A : ) {x : A.unitGroup} :
x A.principalUnitGroup A.unitGroupMulEquiv x ().ker
def ValuationSubring.principalUnitGroupEquiv {K : Type u} [] (A : ) :
A.principalUnitGroup ≃* ().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
theorem ValuationSubring.principalUnitGroupEquiv_apply {K : Type u} [] (A : ) (a : A.principalUnitGroup) :
(A.principalUnitGroupEquiv a) = a
theorem ValuationSubring.principalUnitGroup_symm_apply {K : Type u} [] (A : ) (a : ().ker) :
(A.principalUnitGroupEquiv.symm a) = a
def ValuationSubring.unitGroupToResidueFieldUnits {K : Type u} [] (A : ) :
A.unitGroup →*

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

Equations
• A.unitGroupToResidueFieldUnits = ().comp A.unitGroupMulEquiv.toMonoidHom
Instances For
@[simp]
theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply {K : Type u} [] (A : ) (x : A.unitGroup) :
(A.unitGroupToResidueFieldUnits x) = (A.unitGroupMulEquiv x)
theorem ValuationSubring.ker_unitGroupToResidueFieldUnits {K : Type u} [] (A : ) :
A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
theorem ValuationSubring.surjective_unitGroupToResidueFieldUnits {K : Type u} [] (A : ) :
Function.Surjective A.unitGroupToResidueFieldUnits
def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits {K : Type u} [] (A : ) :
A.unitGroup Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃*

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

Porting note: Lean needs to be reminded of this instance

Equations
• A.instMulOneClassQuotientSubtypeUnitsMemSubgroupUnitGroupComapSubtypePrincipalUnitGroup = inferInstance
Instances For
theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk {K : Type u} [] (A : ) :
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} [] (A : ) (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 RingTheory/Subring/Pointwise.lean; try to keep these in sync.

def ValuationSubring.pointwiseHasSMul {K : Type u} [] {G : Type u_1} [] [] :
SMul G ()

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 : ) => let __src := g S.toSubring; { toSubring := __src, mem_or_inv_mem' := } }
Instances For
@[simp]
theorem ValuationSubring.coe_pointwise_smul {K : Type u} [] {G : Type u_1} [] [] (g : G) (S : ) :
(g S) = g S
@[simp]
theorem ValuationSubring.pointwise_smul_toSubring {K : Type u} [] {G : Type u_1} [] [] (g : G) (S : ) :
(g S).toSubring = g S.toSubring
def ValuationSubring.pointwiseMulAction {K : Type u} [] {G : Type u_1} [] [] :

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
Instances For
theorem ValuationSubring.smul_mem_pointwise_smul {K : Type u} [] {G : Type u_1} [] [] (g : G) (x : K) (S : ) :
x Sg x g S
instance ValuationSubring.instCovariantClassHSMulLe {K : Type u} [] {G : Type u_1} [] [] :
CovariantClass G () HSMul.hSMul LE.le
Equations
• =
theorem ValuationSubring.mem_smul_pointwise_iff_exists {K : Type u} [] {G : Type u_1} [] [] (g : G) (x : K) (S : ) :
x g S sS, g s = x
instance ValuationSubring.pointwise_central_scalar {K : Type u} [] {G : Type u_1} [] [] [] [] :
Equations
• =
@[simp]
theorem ValuationSubring.smul_mem_pointwise_smul_iff {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {x : K} :
g x g S x S
theorem ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {x : K} :
x g S g⁻¹ x S
theorem ValuationSubring.mem_inv_pointwise_smul_iff {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {x : K} :
x g⁻¹ S g x S
@[simp]
theorem ValuationSubring.pointwise_smul_le_pointwise_smul_iff {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {T : } :
g S g T S T
theorem ValuationSubring.pointwise_smul_subset_iff {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {T : } :
g S T S g⁻¹ T
theorem ValuationSubring.subset_pointwise_smul_iff {K : Type u} [] {G : Type u_1} [] [] {g : G} {S : } {T : } :
S g T g⁻¹ S T
def ValuationSubring.comap {K : Type u} [] {L : Type u_1} [] (A : ) (f : K →+* L) :

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

Equations
• A.comap f = let __src := Subring.comap f A.toSubring; { toSubring := __src, mem_or_inv_mem' := }
Instances For
@[simp]
theorem ValuationSubring.coe_comap {K : Type u} [] {L : Type u_1} [] (A : ) (f : K →+* L) :
(A.comap f) = f ⁻¹' A
@[simp]
theorem ValuationSubring.mem_comap {K : Type u} [] {L : Type u_1} [] {A : } {f : K →+* L} {x : K} :
x A.comap f f x A
theorem ValuationSubring.comap_comap {K : Type u} [] {L : Type u_1} {J : Type u_2} [] [] (A : ) (g : L →+* J) (f : K →+* L) :
(A.comap g).comap f = A.comap (g.comp f)
theorem Valuation.mem_unitGroup_iff (K : Type u) [] {Γ : Type u_1} (v : ) (x : Kˣ) :
x v.valuationSubring.unitGroup v x = 1