Transporting the value group along an equivalence of valuations

Mathlib's Valuation.IsEquiv.orderMonoidIso is an isomorphism of the value monoids with zero, v.ValueGroup₀ ≃*o w.ValueGroup₀. Consumers that work with the value group — for instance any convex subgroup of it — need the corresponding isomorphism of groups, which this file supplies.

Since ValueGroup₀ f = WithZero ↥(valueGroup f), it is exactly the inverse of Mathlib's OrderMonoidIso.withZero, the equivalence between order isomorphisms of two groups and order isomorphisms of those groups with a zero adjoined.

Main definitions

• Valuation.IsEquiv.valueGroupOrderIso : The induced order isomorphism of value groups.

Main results

• Valuation.IsEquiv.valueGroupOrderIso_coe : it agrees with orderMonoidIso under the coercion into the value monoid with zero.
• Valuation.IsEquiv.valueGroupOrderIso_symm, Valuation.IsEquiv.valueGroupOrderIso_eq_refl and Valuation.IsEquiv.valueGroupOrderIso_trans : the transport is functorial, mirroring Mathlib's orderMonoidIso_symm, orderMonoidIso_eq_refl and orderMonoidIso_trans.

noncomputable def Valuation.IsEquiv.valueGroupOrderIso {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {Γ₀' : Type u_3} [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation A Γ₀} {w : Valuation A Γ₀'} (h : v.IsEquiv w) : ↥(↑v).valueGroup ≃*o ↥(↑w).valueGroup

The order isomorphism of value groups induced by an equivalence of valuations. Mathlib's IsEquiv.orderMonoidIso is an isomorphism of the value monoids with zero, and ValueGroup₀ f = WithZero ↥(valueGroup f), so this is exactly the inverse of Mathlib's OrderMonoidIso.withZero, which identifies order isomorphisms of two groups with those of the groups with zero adjoined.

Equations

• h.valueGroupOrderIso = OrderMonoidIso.withZero.symm h.orderMonoidIso

@[simp]

theorem Valuation.IsEquiv.valueGroupOrderIso_coe {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {Γ₀' : Type u_3} [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation A Γ₀} {w : Valuation A Γ₀'} (h : v.IsEquiv w) (γ : ↥(↑v).valueGroup) : ↑(h.valueGroupOrderIso γ) = h.orderMonoidIso ↑γ

The induced value-group isomorphism agrees with orderMonoidIso under the coercion.

theorem Valuation.IsEquiv.valueGroupOrderIso_symm {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {Γ₀' : Type u_3} [LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation A Γ₀} {w : Valuation A Γ₀'} (h : v.IsEquiv w) (h' : w.IsEquiv v) : h.valueGroupOrderIso.symm = h'.valueGroupOrderIso

Transport along the inverse equivalence is the inverse transport. Mirrors Mathlib's Valuation.IsEquiv.orderMonoidIso_symm.

@[simp]

theorem Valuation.IsEquiv.valueGroupOrderIso_eq_refl {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} (h : v.IsEquiv v) : h.valueGroupOrderIso = OrderMonoidIso.refl ↥(↑v).valueGroup

Transport along a valuation's equivalence with itself is the identity. Mirrors Mathlib's Valuation.IsEquiv.orderMonoidIso_eq_refl.

@[simp]

theorem Valuation.IsEquiv.valueGroupOrderIso_trans {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {Γ₀' : Type u_3} [LinearOrderedCommGroupWithZero Γ₀'] {Γ₀'' : Type u_4} [LinearOrderedCommGroupWithZero Γ₀''] {v : Valuation A Γ₀} {w : Valuation A Γ₀'} {u : Valuation A Γ₀''} (h : v.IsEquiv w) (h' : w.IsEquiv u) : h.valueGroupOrderIso.trans h'.valueGroupOrderIso = ⋯.valueGroupOrderIso

Transport along a composite equivalence is the composite transport. Mirrors Mathlib's Valuation.IsEquiv.orderMonoidIso_trans.