Rational realizations of ℤᵐ⁰

This file constructs the monoid-with-zero homomorphism from ℤᵐ⁰ to the nonnegative rationals that sends an integer exponent n to e ^ n. It is the rational-valued counterpart of Mathlib's WithZeroMulInt.toNNReal and is useful when a discretely valued field has an integer-valued normalization whose associated absolute value is rational.

Main definitions

• WithZeroMulInt.toNNRat: sends 0 to 0 and a nonzero exponent n to e ^ n.

Main results

• WithZeroMulInt.toNNRat_strictMono: the map is strictly increasing when 1 < e.

The construction and proofs follow Mathlib's WithZeroMulInt.toNNReal, with codomain ℚ≥0 instead of ℝ≥0.

def WithZeroMulInt.toNNRat {e : ℚ≥0} (he : e ≠ 0) : WithZero (Multiplicative ℤ) →*₀ ℚ≥0

The monoid-with-zero homomorphism ℤᵐ⁰ → ℚ≥0 sending a nonzero exponent n to e ^ n.

This is the nonnegative-rational counterpart of Mathlib's WithZeroMulInt.toNNReal.

Equations

• WithZeroMulInt.toNNRat he = WithZero.lift' ((Units.coeHom ℚ≥0).comp ((zpowersHom ℚ≥0ˣ) (Units.mk0 e he)))

@[simp]

theorem WithZeroMulInt.toNNRat_coe {e : ℚ≥0} (he : e ≠ 0) (n : Multiplicative ℤ) : (toNNRat he) ↑n = e ^ Multiplicative.toAdd n

On a finite exponent, toNNRat is the corresponding integer power of its base.

theorem WithZeroMulInt.toNNRat_apply_of_ne_zero {e : ℚ≥0} (he : e ≠ 0) {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) : (toNNRat he) x = e ^ Multiplicative.toAdd (WithZero.unzero hx)

The value of toNNRat at a nonzero exponent is the corresponding integer power.

theorem WithZeroMulInt.toNNRat_ne_zero {e : ℚ≥0} {x : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hx : x ≠ 0) : (toNNRat he) x ≠ 0

toNNRat sends nonzero exponents to nonzero values.

theorem WithZeroMulInt.toNNRat_pos {e : ℚ≥0} {x : WithZero (Multiplicative ℤ)} (he : e ≠ 0) (hx : x ≠ 0) : 0 < (toNNRat he) x

toNNRat sends nonzero exponents to positive values.

theorem WithZeroMulInt.toNNRat_strictMono {e : ℚ≥0} (he : 1 < e) : StrictMono ⇑(toNNRat ⋯)

The map toNNRat is strictly increasing when its base is greater than one.

theorem WithZeroMulInt.toNNRat_eq_one_iff {e : ℚ≥0} (x : WithZero (Multiplicative ℤ)) (he0 : e ≠ 0) (he1 : e ≠ 1) : (toNNRat he0) x = 1 ↔ x = 1

For a base different from zero and one, toNNRat takes the value one only at exponent one, which represents the integer exponent zero in ℤᵐ⁰.

theorem WithZeroMulInt.toNNRat_lt_one_iff {e : ℚ≥0} {x : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNRat ⋯) x < 1 ↔ x < 1

For a base greater than one, strict comparison with one in ℚ≥0 is strict comparison with one in ℤᵐ⁰.

theorem WithZeroMulInt.toNNRat_le_one_iff {e : ℚ≥0} {x : WithZero (Multiplicative ℤ)} (he : 1 < e) : (toNNRat ⋯) x ≤ 1 ↔ x ≤ 1

For a base greater than one, comparison with one in ℚ≥0 is comparison with one in ℤᵐ⁰.