instIsScalarTower — Mathlib

English

The composition of mapPiEvalRingHom with algebraMap equals the corresponding algebraMap composed with Pi.evalRingHom.

Русский

Состав mapPiEvalRingHom с algebraMap равен algebraMap с Pi.evalRingHom.

LaTeX

$$$(mapPiEvalRingHom I).\mathrm{comp} (algebraMap _ _) = (algebraMap _ _).\mathrm{comp} (Pi.evalRingHom R i).$$$

Lean4

instance (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
    IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P) :=
  .of_algebraMap_eq <| by
    simp [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply R A (Localization.AtPrime p),
      Localization.localRingHom_to_map, IsScalarTower.algebraMap_apply R B (Localization.AtPrime P),
      IsScalarTower.algebraMap_apply R A B]

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