under — Mathlib

English

If B is an integral A-algebra and P is a maximal ideal of B, then the contraction of P to A is a maximal ideal of A.

Русский

Пусть B — интегральное A-алгебра, и P — максимальный идеал B. Тогда он стягивается в A в максимальный идеал A.

LaTeX

$$P.IsMaximal → (P.under A).IsMaximal$$

Lean4

/-- If `B` is an integral `A`-algebra, `P` is a maximal ideal of `B`, then the pull back of
  `P` is also a maximal ideal of `A`. -/
instance under [P.IsMaximal] : (P.under A).IsMaximal :=
  isMaximal_comap_of_isIntegral_of_isMaximal P

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