of_surjective — Mathlib

English

If a surjective map f yields a principal comap of an ideal I, then I is principal.

Русский

Если отображение f сюръективно и образ I по обратному отображению является главным, то сам I главный.

LaTeX

$$$IsPrincipal(I) \\Rightarrow IsPrincipal(I\\\\mathrm{comap}(f))$$$

Lean4

/-- The surjective image of a principal ideal ring is again a principal ideal ring. -/
theorem of_surjective [IsPrincipalIdealRing R] (f : F) (hf : Function.Surjective f) : IsPrincipalIdealRing S :=
  ⟨fun I => Ideal.IsPrincipal.of_comap f hf I⟩

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