Documentation

Mathlib.Topology.Algebra.Valued.ValuativeRel

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 #

source
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) :
IsValuativeTopology R

Assuming ContinuousConstVAdd R R, we only need to check the neighbourhood of 0 in order to prove IsValuativeTopology R.

source
theorem IsValuativeTopology.mem_nhds_iff' {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {s : Set R} {x : R} :
s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {z : R | (ValuativeRel.valuation R) (z - x) < ↑γ} ⊆ s

A version mentioning subtraction.

source
@[deprecated IsValuativeTopology.mem_nhds_iff' (since := "2025-08-01")]
theorem ValuativeTopology.mem_nhds {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {s : Set R} {x : R} :
s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {z : R | (ValuativeRel.valuation R) (z - x) < ↑γ} ⊆ s

Alias of IsValuativeTopology.mem_nhds_iff'.

A version mentioning subtraction.

source
theorem IsValuativeTopology.mem_nhds_zero_iff {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (s : Set R) :
s ∈ nhds 0 ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {x : R | (ValuativeRel.valuation R) x < ↑γ} ⊆ s
source
@[deprecated IsValuativeTopology.mem_nhds_zero_iff (since := "2025-08-04")]
theorem ValuativeTopology.mem_nhds_iff {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (s : Set R) :
s ∈ nhds 0 ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {x : R | (ValuativeRel.valuation R) x < ↑γ} ⊆ s

Alias of IsValuativeTopology.mem_nhds_zero_iff.

source
@[instance 100]
instance IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup {R : Type u_2} [CommRing R] [ValuativeRel R] [UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology 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
    source
    theorem IsValuativeTopology.hasBasis_nhds {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (x : R) :
    (nhds x).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {z : R | (ValuativeRel.valuation R) (z - x) < ↑γ}
    source
    theorem IsValuativeTopology.hasBasis_nhds_zero (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] :
    (nhds 0).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {x : R | (ValuativeRel.valuation R) x < ↑γ}
    source
    @[deprecated IsValuativeTopology.hasBasis_nhds_zero (since := "2025-08-01")]
    theorem ValuativeTopology.hasBasis_nhds_zero (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] :
    (nhds 0).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {x : R | (ValuativeRel.valuation R) x < ↑γ}

    Alias of IsValuativeTopology.hasBasis_nhds_zero.

    source
    @[instance 100]
    instance IsValuativeTopology.isTopologicalAddGroup (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] :
    IsTopologicalAddGroup R
    source
    @[instance 100]
    instance IsValuativeTopology.instIsTopologicalRing {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] :
    IsTopologicalRing R
    source
    theorem IsValuativeTopology.isOpen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsOpen {x : R | (ValuativeRel.valuation R) x < r}
    source
    @[deprecated IsValuativeTopology.isOpen_ball (since := "2025-08-01")]
    theorem ValuativeTopology.isOpen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsOpen {x : R | (ValuativeRel.valuation R) x < r}

    Alias of IsValuativeTopology.isOpen_ball.

    source
    theorem IsValuativeTopology.isClosed_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClosed {x : R | (ValuativeRel.valuation R) x < r}
    source
    @[deprecated IsValuativeTopology.isClosed_ball (since := "2025-08-01")]
    theorem ValuativeTopology.isClosed_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClosed {x : R | (ValuativeRel.valuation R) x < r}

    Alias of IsValuativeTopology.isClosed_ball.

    source
    theorem IsValuativeTopology.isClopen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClopen {x : R | (ValuativeRel.valuation R) x < r}
    source
    @[deprecated IsValuativeTopology.isClopen_ball (since := "2025-08-01")]
    theorem ValuativeTopology.isClopen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClopen {x : R | (ValuativeRel.valuation R) x < r}

    Alias of IsValuativeTopology.isClopen_ball.

    source
    theorem IsValuativeTopology.isOpen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsOpen {x : R | (ValuativeRel.valuation R) x ≤ r}
    source
    @[deprecated IsValuativeTopology.isOpen_closedBall (since := "2025-08-01")]
    theorem ValuativeTopology.isOpen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsOpen {x : R | (ValuativeRel.valuation R) x ≤ r}

    Alias of IsValuativeTopology.isOpen_closedBall.

    source
    theorem IsValuativeTopology.isClosed_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClosed {x : R | (ValuativeRel.valuation R) x ≤ r}
    source
    @[deprecated IsValuativeTopology.isClosed_closedBall (since := "2025-08-01")]
    theorem ValuativeTopology.isClosed_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (r : ValuativeRel.ValueGroupWithZero R) :
    IsClosed {x : R | (ValuativeRel.valuation R) x ≤ r}

    Alias of IsValuativeTopology.isClosed_closedBall.

    source
    theorem IsValuativeTopology.isClopen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsClopen {x : R | (ValuativeRel.valuation R) x ≤ r}
    source
    @[deprecated IsValuativeTopology.isClopen_closedBall (since := "2025-08-01")]
    theorem ValuativeTopology.isClopen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsClopen {x : R | (ValuativeRel.valuation R) x ≤ r}

    Alias of IsValuativeTopology.isClopen_closedBall.

    source
    theorem IsValuativeTopology.isClopen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsClopen {x : R | (ValuativeRel.valuation R) x = r}
    source
    @[deprecated IsValuativeTopology.isClopen_sphere (since := "2025-08-01")]
    theorem ValuativeTopology.isClopen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsClopen {x : R | (ValuativeRel.valuation R) x = r}

    Alias of IsValuativeTopology.isClopen_sphere.

    source
    theorem IsValuativeTopology.isOpen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsOpen {x : R | (ValuativeRel.valuation R) x = r}
    source
    @[deprecated IsValuativeTopology.isOpen_sphere (since := "2025-08-01")]
    theorem ValuativeTopology.isOpen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {r : ValuativeRel.ValueGroupWithZero R} (hr : r ≠ 0) :
    IsOpen {x : R | (ValuativeRel.valuation R) x = r}

    Alias of IsValuativeTopology.isOpen_sphere.

    source
    theorem IsValuativeTopology.continuous_valuation {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] :
    Continuous ⇑(ValuativeRel.valuation R)
    source
    def ValuativeRel.«term𝒪[_]» :
    Lean.ParserDescr

    The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.

    Equations
      Instances For
        source
        def ValuativeRel.«term𝓂[_]» :
        Lean.ParserDescr

        The ideal of elements that are not units.

        Equations
          Instances For
            source
            def ValuativeRel.«term𝓀[_]» :
            Lean.ParserDescr

            The residue field of a local ring is the quotient of the ring by its maximal ideal.

            Equations
              Instances For