Ring topologised by a valuation

For a given valuation v : Valuation R Γ₀ on a ring R taking values in Γ₀, this file defines the type synonym WithVal v of R. By assigning a Valued (WithVal v) Γ₀ instance, WithVal v represents the ring R equipped with the topology coming from v. The type synonym WithVal v is in isomorphism to R as rings via WithVal.equiv v. This isomorphism should be used to explicitly map terms of WithVal v to terms of R.

The WithVal type synonym is used to define the completion of R with respect to v in Valuation.Completion. An example application of this is IsDedekindDomain.HeightOneSpectrum.adicCompletion, which is the completion of the field of fractions of a Dedekind domain with respect to a height-one prime ideal of the domain.

Main definitions

• WithVal : type synonym for a ring equipped with the topology coming from a valuation.
• WithVal.equiv : the canonical ring equivalence between WithValuation v and R.
• Valuation.Completion : the uniform space completion of a field K according to the uniform structure defined by the specified valuation.

def WithVal {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] : Valuation R Γ₀ → Type u_1

Type synonym for a ring equipped with the topology coming from a valuation.

Equations

• WithVal x✝ = R

instance WithVal.instRing {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Ring (WithVal v)

Equations

• WithVal.instRing v = inst✝¹

instance WithVal.instCommRing {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [CommRing R] : CommRing (WithVal v)

Equations

• WithVal.instCommRing v = inst✝

instance WithVal.instField {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [Field R] : Field (WithVal v)

Equations

• WithVal.instField v = inst✝

instance WithVal.instInhabited {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Inhabited (WithVal v)

Equations

• WithVal.instInhabited v = { default := 0 }

instance WithVal.instAlgebra {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {S : Type u_3} [CommSemiring S] [CommRing R] [Algebra S R] : Algebra S (WithVal v)

Equations

• WithVal.instAlgebra v = inst✝

instance WithVal.instIsFractionRing {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {S : Type u_3} [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] : IsFractionRing S (WithVal v)

instance WithVal.instSMul {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {S : Type u_3} [SMul S R] : SMul S (WithVal v)

Equations

• WithVal.instSMul v = inst✝

instance WithVal.instIsScalarTower {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) {P : Type u_3} {S : Type u_4} [SMul P S] [SMul S R] [SMul P R] [IsScalarTower P S R] : IsScalarTower P S (WithVal v)

instance WithVal.instValued {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : Valued (WithVal v) Γ₀

Equations

• WithVal.instValued v = Valued.mk' v

def WithVal.equiv {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) : WithVal v ≃+* R

Canonical ring equivalence between WithValuation v and R.

Equations

• WithVal.equiv v = RingEquiv.refl (WithVal v)

theorem WithVal.apply_equiv {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (r : WithVal v) : v ((equiv v) r) = v r

The completion of a field with respect to a valuation.

@[reducible, inline]

abbrev Valuation.Completion {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) : Type u_3

The completion of a field with respect to a valuation.

Equations

• v.Completion = UniformSpace.Completion (WithVal v)

instance Valuation.instCoeCompletion {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [Ring R] (v : Valuation R Γ₀) : Coe R v.Completion

Equations

• v.instCoeCompletion = inferInstanceAs (Coe (WithVal v) (UniformSpace.Completion (WithVal v)))

instance NumberField.RingOfIntegers.instCoeHeadWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] (v : Valuation K Γ₀) : CoeHead (RingOfIntegers (WithVal v)) (WithVal v)

Equations

• NumberField.RingOfIntegers.instCoeHeadWithVal v = inferInstanceAs (CoeHead (NumberField.RingOfIntegers K) K)

instance NumberField.RingOfIntegers.instIsDedekindDomainWithVal {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [Field K] [NumberField K] (v : Valuation K Γ₀) : IsDedekindDomain (RingOfIntegers (WithVal v))