instIsScalarTowerResidueField — Mathlib

English

There is a natural IsScalarTower relation among R, p.ResidueField, and q.ResidueField when p ⊂ A, q ⊂ B with q lying over p.

Русский

Существует естественное отношение IsScalarTower между R, p.ResidueField и q.ResidueField при p ⊂ A, q ⊂ B и q лежит над p.

LaTeX

$$$IsScalarTower\ R\ p.\mathrm{ResidueField}\ q.\mathrmResidueField$$$

Lean4

instance (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    IsScalarTower R p.ResidueField q.ResidueField :=
  .of_algebraMap_eq' ((Ideal.ResidueField.mapₐ p q Ideal.LiesOver.over).restrictScalars R).comp_algebraMap.symm

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