map_ringHom — Mathlib

English

If f is a ring homomorphism and I is principal, then the image map f I is principal with generator f(generator I).

Русский

Если f — гомоморфизм колец и I является главным, то образ f(I) также главный, порожденный f(generator I).

LaTeX

$$$IsPrincipal(I) \\Rightarrow IsPrincipal(\\\\mathrm{map}(f,I))$$$

Lean4

theorem map_ringHom (f : F) {I : Ideal R} (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I) :=
  ⟨⟨f (IsPrincipal.generator I), by
      rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span, Ideal.span_singleton_generator]⟩⟩

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