The trivial valuation attached to a prime ideal #
The trivial valuation of a prime ideal 𝔭 of a commutative ring: it is 0 on 𝔭 and 1
off it. It is the pullback of Mathlib's trivial valuation 1 on the quotient domain A ⧸ 𝔭
along the quotient map. This is the construction behind the trivial-valuation section of
the support map of the valuation spectrum.
Main definitions #
Valuation.trivialValuation 𝔭: The trivial valuation attached to a prime ideal𝔭, with values in any linearly ordered commutative monoid with zeroΓ₀(the valuation-spectrum section specializes it toWithZero (Multiplicative ℤ)).
Main results #
Valuation.trivialValuation_eq_zero_iff: The trivial valuation vanishes exactly on𝔭.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Remark 4.6.
noncomputable def
Valuation.trivialValuation
{A : Type u_1}
[CommRing A]
{Γ₀ : Type u_2}
[LinearOrderedCommMonoidWithZero Γ₀]
(𝔭 : Ideal A)
[𝔭.IsPrime]
:
Valuation A Γ₀
The trivial valuation attached to a prime ideal 𝔭 (Wedhorn, Remark 4.6): it is 0 on
𝔭 and 1 off it, as the pullback of the trivial valuation on the quotient domain A ⧸ 𝔭
along the quotient map.
Equations
Instances For
theorem
Valuation.trivialValuation_apply
{A : Type u_1}
[CommRing A]
{Γ₀ : Type u_2}
[LinearOrderedCommMonoidWithZero Γ₀]
{𝔭 : Ideal A}
[𝔭.IsPrime]
(a : A)
:
The value of the trivial valuation, as an if.
@[simp]
theorem
Valuation.trivialValuation_eq_zero_iff
{A : Type u_1}
[CommRing A]
{Γ₀ : Type u_2}
[LinearOrderedCommMonoidWithZero Γ₀]
[Nontrivial Γ₀]
{𝔭 : Ideal A}
[𝔭.IsPrime]
{a : A}
:
The trivial valuation vanishes exactly on the prime ideal.
@[simp]
theorem
Valuation.trivialValuation_eq_one_iff
{A : Type u_1}
[CommRing A]
{Γ₀ : Type u_2}
[LinearOrderedCommMonoidWithZero Γ₀]
[Nontrivial Γ₀]
{𝔭 : Ideal A}
[𝔭.IsPrime]
{a : A}
:
The trivial valuation takes the value 1 exactly off the prime ideal.