isScalarTower_liftAlgebra — Mathlib

English

The canonical algebra map from FractionRing R to K equals the lift of the faithful algebra map when appropriate.

Русский

Каноническое отображение алгебра из FractionRing R в K равно подъему доверенного отображения.

LaTeX

$$algebraMap (FractionRing R) K = IsFractionRing.lift (FaithfulSMul.algebraMap_injective R K)$$

Lean4

instance isScalarTower_liftAlgebra : IsScalarTower R (FractionRing R) K :=
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  .of_algebraMap_eq fun x ↦ (IsFractionRing.lift_algebraMap (FaithfulSMul.algebraMap_injective R K) x).symm

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