instAlgebraResidueFieldOfLiesOver

English

There is a natural algebra structure on p.ResidueField over q.ResidueField when p ⊂ A, q ⊂ B are prime ideals with q lying over p.

Русский

Существует естественная структура алгебры над q.ResidueField на p.ResidueField, если p ⊂ A, q ⊂ B — простые идеалы и q лежит над p.

LaTeX

$$$\text{Given } p \subset A, q \subset B \text{ with } p, q \text{ prime and } q\text{ lies over } p,\; \text{there is an } Algebra\; p.\mathrm{ResidueField}\; q.\mathrmResidueField$$$

Lean4

noncomputable instance (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    Algebra p.ResidueField q.ResidueField :=
  (Ideal.ResidueField.mapₐ p q Ideal.LiesOver.over).toAlgebra

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