comap_injective_of_surjective — Mathlib

English

If f is a surjective ring homomorphism, then the induced comap on prime spectra is injective.

Русский

Если гомоморфизм f сюрьективен, тогда отображение comap на спектры простых идеалов инъективно.

LaTeX

$$The map (algebraMap R S).specComap is injective.$$

Lean4

theorem comap_injective_of_surjective (f : R →+* S) (hf : Function.Surjective f) : Function.Injective (comap f) :=
  fun _ _ h => specComap_injective_of_surjective _ hf h

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