A valuation subring of a field K
is a subring A
such that for every x : K
,
either x ∈ A
or x⁻¹ ∈ A
.
Instances For
The value group of the valuation associated to A
. Note: it is actually a group with zero.
Instances For
Any valuation subring of K
induces a natural valuation on K
.
Instances For
An overring of a valuation ring is a valuation ring.
Instances For
The ring homomorphism induced by the partial order.
Instances For
The canonical ring homomorphism from a valuation ring to its field of fractions.
Instances For
The canonical map on value groups induced by a coarsening of valuation rings.
Instances For
The ideal corresponding to a coarsening of a valuation ring.
Instances For
The coarsening of a valuation ring associated to a prime ideal.
Instances For
The equivalence between coarsenings of a valuation ring and its prime ideals.
Instances For
An ordered variant of primeSpectrumEquiv
.
Instances For
The valuation subring associated to a valuation.
Instances For
The unit group of a valuation subring, as a subgroup of Kˣ
.
Instances For
For a valuation subring A
, A.unitGroup
agrees with the units of A
.
Instances For
The map on valuation subrings to their unit groups is an order embedding.
Instances For
The nonunits of a valuation subring of K
, as a subsemigroup of K
Instances For
The map on valuation subrings to their nonunits is a dual order embedding.
Instances For
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.
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.
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 Kˣ
.
Instances For
The map on valuation subrings to their principal unit groups is an order embedding.
Instances For
The principal unit group agrees with the kernel of the canonical map from
the units of A
to the units of the residue field of A
.
Instances For
The canonical map from the unit group of A
to the units of the residue field of A
.
Instances For
The quotient of the unit group of A
by the principal unit group of A
agrees with
the units of the residue field of A
.
Instances For
Instances For
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.
The action on a valuation subring corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
Instances For
The action on a valuation subring corresponding to applying the action to every element.
This is available as an instance in the pointwise
locale.
This is a stronger version of ValuationSubring.pointwiseSMul
.
Instances For
The pullback of a valuation subring A
along a ring homomorphism K →+* L
.