Basic facts about valuative relations

General lemmas about ValuativeRel that Mathlib does not yet provide.

Main results

• TauCeti.ValuativeRel.not_vle_zero_of_isUnit : If f is a unit, then ¬ f ≤ᵥ 0.
• TauCeti.ValuativeRel.vle_of_vle_inv_mul and TauCeti.ValuativeRel.vle_of_inv_mul_vle : cancel a unit in valuation comparisons.
• TauCeti.valuativeExtension_self: every valuative commutative semiring is a valuative extension of itself.
• TauCeti.valuation_le_one_of_sub_sq_le_one: if an integral element differs from a square by an integral element, then the square root is integral.
• TauCeti.one_add_pow_ne_zero_of_valuation_lt_one: a positive power of an element of valuation less than one cannot equal -1.

References

TauCeti.ValuativeRel.not_vle_zero_of_isUnit is ported from the open Mathlib pull request leanprover-community/mathlib4#38009; this copy is deleted in favour of the Mathlib declaration once that pull request reaches the pinned Mathlib.

theorem TauCeti.ValuativeRel.not_vle_zero_of_isUnit {A : Type u_1} [Semiring A] [ValuativeRel A] {f : A} (hf : IsUnit f) : ¬f ≤ᵥ 0

If f is a unit, then ¬ f ≤ᵥ 0.

theorem TauCeti.ValuativeRel.vle_of_vle_inv_mul {A : Type u_1} [Semiring A] [ValuativeRel A] (ϖ : Aˣ) {t : A} (h : 1 ≤ᵥ ↑ϖ⁻¹ * t) : ↑ϖ ≤ᵥ t

If 1 ≤ᵥ ϖ⁻¹ * t for a unit ϖ, then ϖ ≤ᵥ t.

theorem TauCeti.ValuativeRel.vle_of_inv_mul_vle {A : Type u_1} [Semiring A] [ValuativeRel A] (ϖ : Aˣ) {t : A} (h : ↑ϖ⁻¹ * t ≤ᵥ 1) : t ≤ᵥ ↑ϖ

If ϖ⁻¹ * t ≤ᵥ 1 for a unit ϖ, then t ≤ᵥ ϖ.

instance TauCeti.valuativeExtension_self (K : Type u_1) [CommSemiring K] [ValuativeRel K] : ValuativeExtension K K

A commutative semiring equipped with a valuative relation is a valuative extension of itself.

theorem TauCeti.valuation_le_one_of_sub_sq_le_one {K : Type u_1} [Ring K] [ValuativeRel K] {u ξ : K} (hu : (ValuativeRel.valuation K) u ≤ 1) (hξ : (ValuativeRel.valuation K) (u - ξ ^ 2) ≤ 1) : (ValuativeRel.valuation K) ξ ≤ 1

If an element of valuation at most one differs from a square by an element of valuation at most one, then the square root also has valuation at most one.

theorem TauCeti.one_add_pow_ne_zero_of_valuation_lt_one {K : Type u_1} [Ring K] [ValuativeRel K] {x : K} (hx : (ValuativeRel.valuation K) x < 1) {n : ℕ} (hn : n ≠ 0) : 1 + x ^ n ≠ 0

A positive power of an element of valuation less than one cannot equal -1.