English
There is a canonical IsScalarTower relation for R, p.ResidueField, q.ResidueField, and Q.ResidueField when p ⊂ A, q ⊂ B, and Q lies over p.
Русский
Существует каноническое отношение IsScalarTower между R, p.ResidueField, q.ResidueField и Q.ResidueField при p ⊂ A, q ⊂ B и Q лежит над p.
LaTeX
$$$IsScalarTower\ R\ p.\mathrm{ResidueField}\ q.\mathrmResidueField\ Q.\mathrmResidueField$$$
Lean4
instance (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] (Q : Ideal B) [Q.IsPrime] [Q.LiesOver q]
[Q.LiesOver p] : IsScalarTower p.ResidueField q.ResidueField Q.ResidueField :=
by
refine .of_algebraMap_eq fun x ↦ ?_
simp only [RingHom.algebraMap_toAlgebra, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Ideal.ResidueField.mapₐ_apply,
Ideal.ResidueField.map, IsLocalRing.ResidueField.map_map, IsScalarTower.algebraMap_eq R A B,
← Localization.localRingHom_comp]
