liftAlgebra — Mathlib

English

There is a natural scalar tower R -> FractionRing(R) -> K for suitable K.

Русский

Существует естественная пирамидальная структура скаляров: R → FractionRing(R) → K.

LaTeX

$$IsScalarTower R (FractionRing R) K$$

Lean4

/-- This is not an instance because it creates a diamond when `K = FractionRing R`.
Should usually be introduced locally along with `isScalarTower_liftAlgebra`
See note [reducible non-instances]. -/
noncomputable abbrev liftAlgebra : Algebra (FractionRing R) K :=
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  RingHom.toAlgebra (IsFractionRing.lift (FaithfulSMul.algebraMap_injective R K))

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