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
@[implicit_reducible, 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.

source
theorem IsValuativeTopology.v_eq_valuation {R : Type u_2} [CommRing R] [ValuativeRel R] [UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] :
Valued.v = ValuativeRel.valuation R
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.

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

    The ideal of elements that are not units.

    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.

      Instances For