Valuative Relations as Valued #
In this temporary file, we provide a helper instance
for Valued R Γ derived from a ValuativeRel R,
so that downstream files can refer to ValuativeRel R,
to facilitate a refactor.
Alternate constructors #
theorem
IsValuativeTopology.of_zero
{R : Type u_1}
[CommRing R]
[ValuativeRel R]
[TopologicalSpace R]
[ContinuousConstVAdd R R]
(h₀ :
∀ (s : Set R),
s ∈ nhds 0 ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {z : R | (ValuativeRel.valuation R) z < ↑γ} ⊆ s)
:
Assuming ContinuousConstVAdd R R, we only need to check the neighbourhood of 0 in order to
prove IsValuativeTopology R.
@[implicit_reducible, instance 100]
instance
IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup
{R : Type u_2}
[CommRing R]
[ValuativeRel R]
[UniformSpace R]
[IsUniformAddGroup R]
[IsValuativeTopology R]
:
Helper Valued instance when ValuativeTopology R over a UniformSpace R,
for use in porting files from Valued to ValuativeRel.
Equations
- IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup = { toUniformSpace := inst✝², toIsUniformAddGroup := inst✝¹, v := ValuativeRel.valuation R, is_topological_valuation := ⋯ }
theorem
IsValuativeTopology.v_eq_valuation
{R : Type u_2}
[CommRing R]
[ValuativeRel R]
[UniformSpace R]
[IsUniformAddGroup R]
[IsValuativeTopology R]
:
theorem
IsValuativeTopology.continuous_valuation
{R : Type u_1}
[CommRing R]
[ValuativeRel R]
[TopologicalSpace R]
[IsValuativeTopology R]
:
The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ideal of elements that are not units.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residue field of a local ring is the quotient of the ring by its maximal ideal.
Equations
- One or more equations did not get rendered due to their size.