of_comp — Mathlib

English

Spec.map f is Preimmersion iff the induced prime-spectrum map is an embedding and f.hom is surjective on stalks.

Русский

Spec.map f является Preimmersion тогда и только тогда, когда соответствующая карта PrimeSpectrum является вложением, а f.hom сюръективен на stalk.

LaTeX

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

Lean4

theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] [IsPreimmersion (f ≫ g)] : IsPreimmersion f
    where
  base_embedding := by
    have h := (f ≫ g).isEmbedding
    rwa [← g.isEmbedding.of_comp_iff]
  surj_on_stalks
    x := by
    have h := (f ≫ g).stalkMap_surjective x
    rw [Scheme.stalkMap_comp] at h
    exact Function.Surjective.of_comp h

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