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.

instance ValuativeRel.instValuedValueGroupWithZeroOfIsUniformAddGroupOfValuativeTopology {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [ValuativeRel R] [ValuativeTopology R] : Valued R (ValueGroupWithZero R)

Equations

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

theorem ValuativeTopology.hasBasis_nhds_zero (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] : (nhds 0).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {x : R | (ValuativeRel.valuation R) x < ↑γ}

theorem ValuativeTopology.mem_nhds {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] {s : Set R} {x : R} : s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {y : R | (ValuativeRel.valuation R) (y - x) < ↑γ} ⊆ s

theorem ValuativeTopology.isOpen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] (r : ValuativeRel.ValueGroupWithZero R) : IsOpen {x : R | (ValuativeRel.valuation R) x < r}

theorem ValuativeTopology.isClosed_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] (r : ValuativeRel.ValueGroupWithZero R) : IsClosed {x : R | (ValuativeRel.valuation R) x < r}

theorem ValuativeTopology.isClopen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] (r : ValuativeRel.ValueGroupWithZero R) : IsClopen {x : R | (ValuativeRel.valuation R) x < r}

theorem ValuativeTopology.isOpen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) : IsOpen {x : R | (ValuativeRel.valuation R) x ≤ r}

theorem ValuativeTopology.isClosed_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] (r : ValuativeRel.ValueGroupWithZero R) : IsClosed {x : R | (ValuativeRel.valuation R) x ≤ r}

theorem ValuativeTopology.isClopen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) : IsClopen {x : R | (ValuativeRel.valuation R) x ≤ r}

theorem ValuativeTopology.isClopen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) : IsClopen {x : R | (ValuativeRel.valuation R) x = r}

theorem ValuativeTopology.isOpen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [ValuativeTopology R] [IsTopologicalAddGroup R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) : IsOpen {x : R | (ValuativeRel.valuation R) x = r}

def Valued.instValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] [UniformSpace R] [IsUniformAddGroup R] [ValuativeTopology R] : Valued R (ValuativeRel.ValueGroupWithZero R)

Helper Valued instance when ValuativeTopology R over a UniformSpace R, for use in porting files from Valued to ValuativeRel.

Equations

• Valued.instValueGroupWithZero = { toUniformSpace := inst✝², toIsUniformAddGroup := inst✝¹, v := ValuativeRel.valuation R, is_topological_valuation := ⋯ }

def ValuativeRel.«term𝒪[_]» : Lean.ParserDescr

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.

def ValuativeRel.«term𝓂[_]» : Lean.ParserDescr

The ideal of elements that are not units.

Equations

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

def ValuativeRel.«term𝓀[_]» : Lean.ParserDescr

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.