Spec_map_iff — Mathlib

English

Same criterion as above but explicitly stated for ring-level morphisms.

Русский

Та же запись критерия для морфизмов на уровне колец.

LaTeX

$$$ IsPreimmersion (Spec.map f) \iff IsEmbedding (PrimeSpectrum.comap f.hom) \land f.hom.SurjectiveOnStalks $$$

Lean4

theorem Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
    IsPreimmersion (Spec.map f) ↔ IsEmbedding (PrimeSpectrum.comap f.hom) ∧ f.hom.SurjectiveOnStalks :=
  by
  haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso :=
    by
    rw [← RingHom.toMorphismProperty_respectsIso_iff]
    exact RingHom.surjective_respectsIso
  rw [← HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks), isPreimmersion_iff, and_comm]
  rfl

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