toRingHom_toRatAlgHom — Mathlib

English

If f is a ℚ-algebra homomorphism, then the underlying ring homomorphism (viewed as a RatAlgHom) is exactly f; i.e., forgetting the ℚ-algebra structure yields the same map.

Русский

Если f — гомоморфизм ℚ-алгебр, то его основанный на кольце гомоморфизм (рассматриваемый как RatAlgHom) равен f; забывание ℚ-алгебраической структуры не изменяет отображение.

LaTeX

$$$(f : R \\to\\+* S).toRatAlgHom = f$$$

Lean4

@[simp]
theorem toRingHom_toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →ₐ[ℚ] S) :
    (f : R →+* S).toRatAlgHom = f :=
  AlgHom.ext fun _x => rfl

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