map_surjective — Mathlib

English

For every morphism f: Spec S → Spec R, there exists a ring hom φ: R → S with f = Spec.map φ. In other words, Spec.map is surjective on morphisms.

Русский

Для каждого морфизма f: Spec S → Spec R существует кольцевой гомоморфизм φ: R → S такой, что f = Spec.map φ. Иными словами, отображение Spec.map сюръективно на морфизма.

LaTeX

$$$\forall f:\mathrm{Spec}S \to \mathrm{Spec}R,\; \exists \varphi:\, R \to S \;\text{ s.t. }\; \mathrm{Spec.map}(\varphi) = f.$$$

Lean4

/-- Useful for replacing `f` by `Spec.map φ` everywhere in proofs. -/
theorem map_surjective {R S : CommRingCat} : Function.Surjective (Spec.map : (R ⟶ S) → _) :=
  by
  intro f
  use Spec.preimage f
  simp

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