Trivial Valuative Relations

Trivial valuative relations relate all non-zero elements to each other. Equivalently, all elements are related to 1: the relation is equal to the relation induced by the trivial valuation which sends all non-zero elements to 1.

TODO

A trivial valuative relation is equivalent to the value group being isomorphic to WithZero Unit.

def ValuativeRel.trivialRel {R : Type} [CommRing R] [DecidableEq R] [IsDomain R] : ValuativeRel R

The trivial valuative relation on a domain R, such that all non-zero elements are related. The domain condition is necessary so that the relation is closed when multiplying.

Equations

• ValuativeRel.trivialRel = { rel := fun (x y : R) => if y = 0 then x = 0 else True, rel_total := ⋯, rel_trans := ⋯, rel_add := ⋯, rel_mul_right := ⋯, rel_mul_cancel := ⋯, not_rel_one_zero := ⋯ }

theorem ValuativeRel.eq_trivialRel_of_compatible_one {R Γ : Type} [CommRing R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [h : ValuativeRel R] [hv : Valuation.Compatible 1] : h = trivialRel

theorem ValuativeRel.trivialRel_eq_ofValuation_one {R Γ : Type} [CommRing R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] : trivialRel = ofValuation 1

theorem ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel (R Γ : Type) [CommRing R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] : Subsingleton (ValueGroupWithZero R)ˣ

theorem ValuativeRel.not_isNontrivial_of_trivialRel {R Γ : Type} [CommRing R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] : ¬IsNontrivial R

theorem ValuativeRel.isDiscrete_trivialRel {R Γ : Type} [CommRing R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] : IsDiscrete R