Theorems · Definition · commutative algebra

ValuativeRel.ValueGroupWithZero.embed

{R : Type u_2} →
  {Γ : Type u_3} →
    [inst : Ring R] →
      [inst_1 : ValuativeRel R] →
        [inst_2 : LinearOrderedCommGroupWithZero Γ] →
          (v : Valuation R Γ) →
            [v.Compatible] → ValuativeRel.ValueGroupWithZero R →*₀ (MonoidWithZeroHom.ofClass v).ValueGroup₀

The ValueGroupWithZero R is the "minimal" value group (with zero) among all value groups of valuations that are compatible with the valuative relation, in the sense that it is canonically isomorphic to the subgroup (with zero) generated by v '' R for any compatible v. ValueGroupWithZero.embed v is exactly this isomorphism map; it will later be upgraded to ValueGroupWithZero.orderMonoidIso v.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroValuation.Compatible