instNontrivialSubtypeUnitsMemSubmonoidValueMonoid

English

If a valuation v on a ring A takes values in a linearly ordered commutative group with zero Γ and has rank-one discreteness, then the associated value monoid is nontrivial (i.e., it contains an element not equal to the identity).

Русский

Пусть v — оценка на кольце A, значения которой лежат в линейно упорядоченной симметричной группе с единицей Γ и градуированность равна 1; тогда соответствующий моноид значений не тривиален, то есть содержит элемент не равный единице.

LaTeX

$$$\operatorname{Nontrivial}(\mathrm{valueMonoid}(v))$$$

Lean4

instance [IsRankOneDiscrete v] : Nontrivial (valueMonoid v) :=
  by
  by_contra! H
  apply ((valueGroup v).nontrivial_iff_ne_bot).mp (by infer_instance)
  apply closure_eq_bot_iff.mpr
  rw [subsingleton_iff] at H
  intro x hx
  specialize H ⟨x, hx⟩ ⟨1, one_mem_valueMonoid v⟩
  simpa using H

Похожие утверждения