Theorems · Theorem · commutative algebra

ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed

∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] {Γ' : Type u_4} [inst_4 : LinearOrderedCommGroupWithZero Γ']
  (w : Valuation R Γ') [inst_5 : w.Compatible] (x : ValuativeRel.ValueGroupWithZero R) (h : w.IsEquiv v),
  h.orderMonoidIso ((ValuativeRel.ValueGroupWithZero.embed w) x) = (ValuativeRel.ValueGroupWithZero.embed v) x

When we have h : w.IsEquiv v, the image group (with zero) of v is isomorphic to that of w via h.orderMonoidIso. Then the following diagram is commutative: `` ValueGroup₀ w ∧ | embed w / | / | ValueGroupWithZero R | h.orderMonoidIso \ | embed v \ | ∨ ∨ ValueGroup₀ v ``

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroValuation.CompatibleLinearOrderedCommGroupWithZeroValuation.Compatible