awayMap_fromZeroRingHom — Mathlib

English

Away map respects the zero-ring-hom embedding, i.e., it sends the zero element to zero under the canonical lift.

Русский

Away-map сохраняет вложение из нулевого кольца, т.е. нуль переходит в нуль под каноническим подниманием.

LaTeX

$$$$ awayMap 𝒜 hg hx (fromZeroRingHom 𝒜 _ a) = fromZeroRingHom 𝒜 _ a. $$$$

Lean4

theorem awayMap_fromZeroRingHom (a) : awayMap 𝒜 hg hx (fromZeroRingHom 𝒜 _ a) = fromZeroRingHom 𝒜 _ a :=
  by
  ext
  simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, val_awayMap, val_mk,
    SetLike.GradeZero.coe_one]
  convert IsLocalization.lift_eq _ _

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