Fields complete w.r.t. an absolute value

Stream: mathlib4

[Michael Stoll]

What is the idiomatic way to say that a Field F is complete with respect to a given v : AbsoluteValue F ℝ?

[Andrew Yang]

Maybe CompleteSpace (WithAbs v)?

[Matt Diamond]

I can't say if it's idiomatic, but building upon what Andrew said, docs#AbsoluteValue.Completion looks promising

[Matt Diamond]

Oh wait, never mind, you're talking about a field that's already complete.

[Michael Stoll]

Andrew Yang said:

Maybe CompleteSpace (WithAbs v)?

docs#WithAbs gives me the following poroblem:

import Mathlib.Analysis.Normed.Ring.WithAbs

variable {F : Type*} [Field F] (v w : AbsoluteValue F ℝ)

/- fun x => x : WithAbs v → WithAbs v -/
#check (fun x ↦ (x : WithAbs w) : WithAbs v → WithAbs w)

example : WithAbs v = WithAbs w := rfl

I.e., the implementation of docs#WithAbs as a type synonym seems to make it impossible to meaningfully talk about the normed field structures induced by two different absolute values on the same field. E.g., I would like to say that two absolute values induce the same topology; my attempt was IsHomeomorph (fun x ↦ x : WithAbs v → WithAbs w), but this runs into the problem above.

Should docs#WithAbs be refactored to bundle the absolute value instead? Or what would be the "correct" way of solving the problem within the existing framework?

[Yaël Dillies]

That's because you didn't use docs#WithAbs.equiv

[Michael Stoll]

Where should I use docs#WithAbs.equiv in the above?

[Yaël Dillies]

import Mathlib.Analysis.Normed.Ring.WithAbs

variable {F : Type*} [Field F] (v w : AbsoluteValue F ℝ)

#check ((WithAbs.equiv w).symm ∘ WithAbs.equiv v : WithAbs v → WithAbs w)

[Michael Stoll]

While we are at it: Is there a simple way to get DiscreteTopology Y from DiscreteTopology X and a homeomorphism X \to Y?

[Michael Stoll]

@loogle DiscreteTopology, Homeomorph

[loogle]

:shrug: nothing found

[Michael Stoll]

@loogle DiscreteTopology, IsHomeomorph

[loogle]

:shrug: nothing found

[Riccardo Brasca]

We have DiscreteTopology.of_continuous_injective

[Kevin Buzzard]

Yes, this is the canonical trick: if you want to push something along a bijection, ask first whether it pushes along an injection or surjection.