Theorems · Theorem · commutative algebra

ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq

∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] (γ : ValuativeRel.ValueGroupWithZero R),
  MonoidWithZeroHom.ValueGroup₀.embedding ((ValuativeRel.ValueGroupWithZero.embed (ValuativeRel.valuation R)) γ) = γ

When v is valuation R, in the following commutative diagram where the first row is the map v factored through its image group (with zero), `` embedding R –––––––––––> ValueGroup₀ v –––––-–––> ValueGroupWithZero R │ ∧ │ / │ / embed v ∨ / ValueGroupWithZero R ` the map from ValueGroupWithZero R` to itself is identity.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingValuativeRel