ringEquivOfRingEquiv_eq_map — Mathlib

English

The localization isomorphism constructed from a ring equivalence j equals the localization map induced by j on the nose, i.e., the maps agree as functions.

Русский

Изоморфизм локализации, построенный из кольцевого эквивалента j, совпадает с отображением локализации, индуцируемым самим j.

LaTeX

$$$$ (\\mathrm{ringEquivOfRingEquiv} \\ S Q j H) = \\mathrm{map}_Q(j)(M.le\\_comap\\_of\\_map\\_le(\\text{le_of_eq } H)) $$$$

Lean4

theorem ringEquivOfRingEquiv_eq_map {j : R ≃+* P} (H : M.map j.toMonoidHom = T) :
    (ringEquivOfRingEquiv S Q j H : S →+* Q) = map Q (j : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) :=
  rfl

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