Absolute values are equivalent iff...

Stream: mathlib4

[Michael Stoll]

I have completed a proof of the statement that two (real-valued) absolute values on a field F are equivalent iff they induce the same topology on F:

lemma equiv_iff_isHomeomorph (v₁ v₂ : AbsoluteValue F ℝ) :
    v₁ ≈ v₂ ↔ IsHomeomorph ((WithAbs.equiv v₂).symm ∘ WithAbs.equiv v₁)

(as a first step to proving results about extending absolute values to finite field extensions). See Equivalence.lean in the Heights repository. [EDIT: update the link to the file]

I'm planning to set up a short sequence of PRs to get this into Mathlib. Comments are welcome!

[Michael Stoll]

#20588 is a first small step in this direction. It introduces the predicate AbsoluteValue.IsNontrivial, which simplifies handling the distinction between trivial and nontrivial absolute values (without the need for a decidability instance).

[Michael Stoll]

#20608 adds a few API lemmas for powers with real exponents.

[Michael Stoll]

#20612 adds two lemmas on the existence of a (natural or integral) power of some element 0 < c < 1 between to other elements.

[Michael Stoll]

#20642 extends the API for docs#WithAbs and docs#WithAbs.equiv .

[Michael Stoll]

#20685 adds docs#Real.rpow versions of four lemmas that exist for docs#NNReal.rpow and docs#ENNReal.rpow .

[Michael Stoll]

Michael Stoll said:

#20642 extends the API for docs#WithAbs and docs#WithAbs.equiv .

It occurred to me that most of the API lemmas for docs#WithAbs.equiv can be gotten rid of by replacing docs#WithAbs.equiv with docs#WithAbs.ringEquiv (i.e., use the ring isomorphism instead of just a bijection). I do that in #20713; there was only one place downstream where docs#WithAbs.ringEquiv was used (which the PR deprecates in favor of docs#WithAbs.equiv with the now same definition); the API lemmas are so far used nowhere in Mathlib.