comap — Mathlib

English

Pullback preserves equivalence: if v1 IsEquiv v2, then v1.comap f IsEquiv v2.comap f for any ring hom f.

Русский

Вытяжка сохраняет эквивалентность: если v1 IsEquiv v2, то v1.comap f IsEquiv v2.comap f для любого кольцевого гомоморфизма f.

LaTeX

$$$$ \\mathrm{IsEquiv}(v_1 \\leftarrow_f) \\;\\Rightarrow\\; \\mathrm{IsEquiv}(v_1.comap f, v_2.comap f). $$$$

Lean4

/-- `comap` preserves equivalence. -/
theorem comap {S : Type*} [Ring S] (f : S →+* R) (h : v₁.IsEquiv v₂) : (v₁.comap f).IsEquiv (v₂.comap f) :=
  Valuation.IsEquiv.comap f h

Похожие утверждения