liftAlgHom_toRingHom — Mathlib

English

There is a map IsFractionRing.map that, given injective j : A →+* B with B a domain, yields a map K →+* L respecting localization data and sending z to g(j x) g(j y)^{-1} when z = f x f y^{-1}.

Русский

Существует отображение IsFractionRing.map, которое при инъективном j: A →+* B (B — область), задаёт отображение K →+* L, сохраняющее данные локализации и отправляющее z = f x / f y на g(j x) / g(j y).

LaTeX

$$$\text{IsFractionRing.map } L j : K \to+* L$$$

Lean4

theorem liftAlgHom_toRingHom : (liftAlgHom hg : K →ₐ[R] L).toRingHom = lift hg :=
  rfl

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