comp_iff — Mathlib

English

For a ring hom f, Spec.map f is Preimmersion iff its underlying map is an embedding and f.hom is surjective on stalks.

Русский

Для гомоморфизма f, Spec.map f есть Preimmersion тогда и только тогда, когда базовая карта — вложение и f.hom сюръективен на stalk.

LaTeX

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

Lean4

theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] :
    IsPreimmersion (f ≫ g) ↔ IsPreimmersion f :=
  ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩

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