map_nonunit — Mathlib

English

If f is a local ring hom, the image of the maximal ideal of the source is contained in the maximal ideal of the target.

Русский

Образ максимального идеала источника содержится в максимальном идеале цели.

LaTeX

$$$\text{IsLocalHom}(f) \Rightarrow f[\mathfrak{m}_R] \subseteq \mathfrak{m}_S$$$

Lean4

/-- The image of the maximal ideal of the source is contained within the maximal ideal of the target.
-/
theorem map_nonunit (f : R →+* S) [IsLocalHom f] (a : R) (h : a ∈ maximalIdeal R) : f a ∈ maximalIdeal S := fun H =>
  h <| isUnit_of_map_unit f a H

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