WithAbs for fields

This extends the WithAbs mechanism to fields, providing a type synonym for a field which depends on an absolute value. This is useful when dealing with several absolute values on the same field.

In particular this allows us to define the completion of a field at a given absolute value.

@[instance_reducible]

instance WithAbs.instField {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) : Field (WithAbs v)

Equations

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

@[instance_reducible]

noncomputable instance WithAbs.normedField {R : Type u_1} [Field R] (v : AbsoluteValue R ℝ) : NormedField (WithAbs v)

Equations

• WithAbs.normedField v = { toNorm := (WithAbs.normedRing v).toNorm, toField := WithAbs.instField v, toMetricSpace := (WithAbs.normedRing v).toMetricSpace, dist_eq := ⋯, norm_mul := ⋯ }

instance WithAbs.instFiniteDimensional {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Module R T] [FiniteDimensional R T] : FiniteDimensional (WithAbs v) T

instance WithAbs.instFiniteDimensional_1 {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Module T R] [FiniteDimensional T R] : FiniteDimensional T (WithAbs v)

instance WithAbs.instIsSeparable {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Algebra R T] [Algebra.IsSeparable R T] : Algebra.IsSeparable (WithAbs v) T

instance WithAbs.instIsSeparable_1 {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] {T : Type u_3} [Field T] (v : AbsoluteValue R S) [Algebra T R] [Algebra.IsSeparable T R] : Algebra.IsSeparable T (WithAbs v)

@[simp]

theorem WithAbs.toAbs_div {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x y : R) : toAbs v (x / y) = toAbs v x / toAbs v y

@[simp]

theorem WithAbs.ofAbs_div {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x y : WithAbs v) : (x / y).ofAbs = x.ofAbs / y.ofAbs

@[simp]

theorem WithAbs.toAbs_inv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x : R) : toAbs v x⁻¹ = (toAbs v x)⁻¹

@[simp]

theorem WithAbs.ofAbs_inv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Field R] (v : AbsoluteValue R S) (x : WithAbs v) : x⁻¹.ofAbs = x.ofAbs⁻¹

theorem WithAbs.tendsto_one_div_one_add_pow_nhds_one {R : Type u_1} [Field R] {v : AbsoluteValue R ℝ} {a : R} (ha : v a < 1) : Filter.Tendsto (fun (n : ℕ) => (equiv v).symm (1 / (1 + a ^ n))) Filter.atTop (nhds 1)

instance WithAbs.instUniformContinuousConstSMulReal {R : Type u_1} [CommRing R] {T : Type u_3} [Field T] [Algebra R T] (w : AbsoluteValue T ℝ) : UniformContinuousConstSMul R (WithAbs w)

theorem WithAbs.isometry_map {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : Isometry ⇑(map v w (algebraMap K L))

The completion of a field at an absolute value.

@[reducible, inline]

abbrev AbsoluteValue.Completion {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : Type u_1

The completion of a field with respect to a real absolute value.

Equations

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

@[instance_reducible]

noncomputable instance AbsoluteValue.Completion.instCoe {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : Coe K v.Completion

Equations

• AbsoluteValue.Completion.instCoe v = { coe := fun (k : K) => ↑(WithAbs.toAbs v k) }

@[instance_reducible]

noncomputable def AbsoluteValue.Completion.algebraOfLiesOver {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] : Algebra v.Completion w.Completion

If w lies over v with completions K_v and L_w, then there is a unique K_v-algebra structure on L_w satisfying both IsScalarTower K K_v L_w and ContinuousSMul K_v L_w, see AbsoluteValue.Completion.algebraMap_eq and AbsoluteValue.Completion.algebra_eq.

Equations

• AbsoluteValue.Completion.algebraOfLiesOver v w = (UniformSpace.Completion.mapRingHom (WithAbs.map v w (algebraMap K L)) ⋯).toAlgebra

instance AbsoluteValue.Completion.instIsScalarTower {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] : IsScalarTower K v.Completion w.Completion

instance AbsoluteValue.Completion.instContinuousSMul {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] : ContinuousSMul v.Completion w.Completion

theorem AbsoluteValue.Completion.algebraMap_eq {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] : algebraMap v.Completion w.Completion = UniformSpace.Completion.mapRingHom (WithAbs.map v w (algebraMap K L)) ⋯

theorem AbsoluteValue.Completion.algebraMap_apply {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] (x : v.Completion) : (algebraMap v.Completion w.Completion) x = (UniformSpace.Completion.mapRingHom (WithAbs.map v w (algebraMap K L)) ⋯) x

theorem AbsoluteValue.Completion.algebra_eq {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] : inst✝ = algebraOfLiesOver v w

theorem AbsoluteValue.Completion.locallyCompactSpace {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L} [LocallyCompactSpace L] (h : Isometry ⇑f) : LocallyCompactSpace v.Completion

If the absolute value of a normed field factors through an embedding into another normed field that is locally compact, then the completion of the first normed field is also locally compact.