comap_C_surjective — Mathlib

English

The map comap along the constant polynomial map C: R → R[X] is surjective: every prime of R arises as comap of a prime of R[X].

Русский

Карта comap по константному вложению C: R → R[X] сюръективна: каждый прим в R получается как comap прима в R[X].

LaTeX

$$$\\text{comap}_{C}: \\mathrm{PrimeSpectrum}(R[X]) \\to \\mathrm{PrimeSpectrum}(R) \\text{ is surjective}$$$

Lean4

theorem comap_C_surjective : Function.Surjective (comap (R := R) C) :=
  by
  intro x
  refine ⟨comap (evalRingHom 0) x, ?_⟩
  rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp), comap_id, ContinuousMap.id_apply]

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