map — Mathlib

English

The image of a finitely generated ideal under a ring homomorphism is finitely generated.

Русский

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

LaTeX

$$I.FG → (I.map f).FG$$

Lean4

/-- The image of a finitely generated ideal is finitely generated.

This is the `Ideal` version of `Submodule.FG.map`. -/
theorem map {R S : Type*} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) : (I.map f).FG := by
  classical
  obtain ⟨s, hs⟩ := h
  refine ⟨s.image f, ?_⟩
  rw [Finset.coe_image, ← Ideal.map_span, hs]

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