Documentation

Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

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.

source
@[instance_reducible]
def ValuativeRel.trivialRel {R : Type u_3} [Semiring 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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ValuativeRel.eq_trivialRel_of_compatible_one {R : Type u_1} {Γ : Type u_2} [Ring R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [h : ValuativeRel R] [hv : Valuation.Compatible 1] :
    h = trivialRel
    source
    theorem ValuativeRel.trivialRel_eq_ofValuation_one {R : Type u_1} {Γ : Type u_2} [Ring R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] :
    trivialRel = ofValuation 1
    source
    theorem ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel (R : Type u_1) (Γ : Type u_2) [Ring R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] :
    Subsingleton (ValueGroupWithZero R)ˣ
    source
    theorem ValuativeRel.not_isNontrivial_of_trivialRel {R : Type u_1} {Γ : Type u_2} [Ring R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] :
    ¬IsNontrivial R
    source
    theorem ValuativeRel.isDiscrete_trivialRel {R : Type u_1} {Γ : Type u_2} [Ring R] [DecidableEq R] [IsDomain R] [LinearOrderedCommGroupWithZero Γ] [ValuativeRel R] [Valuation.Compatible 1] :
    IsDiscrete R