specComap_injective_of_surjective

English

If a ring hom f: R → S is surjective on rings, then the induced map f.specComap on prime spectra is injective.

Русский

Если кольцевой гомоморфизм f: R → S сюръективен, то индуцированное отображение f.specComap на спектры простых инъективно.

LaTeX

$$$\\text{If } f: R \\to S \\text{ is surjective, then } f.{\\rm specComap} \\text{ is injective}$$$

Lean4

theorem specComap_injective_of_surjective (f : R →+* S) (hf : Function.Surjective f) : Function.Injective f.specComap :=
  fun x y h =>
  PrimeSpectrum.ext
    (Ideal.comap_injective_of_surjective f hf
      (congr_arg PrimeSpectrum.asIdeal h : (f.specComap x).asIdeal = (f.specComap y).asIdeal))

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