Comap for valuative relations

We define the pullback (comap) of a ValuativeRel along a ring homomorphism.

Main definitions

• ValuativeRel.comap φ v : Given φ : A →+* B and a valuative relation v on B, the induced ValuativeRel A defined by a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂).

References

Ported from the open Mathlib pull request leanprover-community/mathlib4#38009; this copy is deleted in favour of the Mathlib declarations once that pull request reaches the pinned Mathlib.

@[instance_reducible]

def ValuativeRel.comap {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] (φ : A →+* B) (v : ValuativeRel B) : ValuativeRel A

The pullback of a ValuativeRel along φ : A →+* B: a₁ ≤ᵥ a₂ ↔ φ(a₁) ≤ᵥ φ(a₂). Use comap_vle and comap_vlt to compute with it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.comap_vle {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) : a₁ ≤ᵥ a₂ ↔ φ a₁ ≤ᵥ φ a₂

The relation pulled back along φ compares images under φ.

@[simp]

theorem ValuativeRel.comap_vlt {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] (φ : A →+* B) (v : ValuativeRel B) (a₁ a₂ : A) : a₁ <ᵥ a₂ ↔ φ a₁ <ᵥ φ a₂

The strict relation pulled back along φ compares images under φ.

@[simp]

theorem ValuativeRel.comap_id {A : Type u_1} [Semiring A] (v : ValuativeRel A) : comap (RingHom.id A) v = v

Pulling back along the identity homomorphism is the identity.

@[simp]

theorem ValuativeRel.comap_comp {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] {C : Type u_3} [Semiring C] (φ : A →+* B) (ψ : B →+* C) (v : ValuativeRel C) : comap (ψ.comp φ) v = comap φ (comap ψ v)

Pulling back along a composite is the composite of the pullbacks.