English
If f: X → Y and g: Y → Z are morphisms with g a closed immersion and f ≫ g a closed immersion, then f is a closed immersion.
Русский
Если морфизмы f: X → Y и g: Y → Z таковы, что g — замкнутое вложение и (f ≫ g) — замкнутое вложение, тогда f — замкнутое вложение.
LaTeX
$$$$IsClosedImmersion(g) \\,\\land\\, IsClosedImmersion(f\\circ g) \\Rightarrow IsClosedImmersion(f).$$$$
Lean4
/-- If `f ≫ g` and `g` are closed immersions, then `f` is a closed immersion.
Also see `IsClosedImmersion.of_comp` for the general version
where `g` is only required to be separated.
-/
theorem of_comp_isClosedImmersion {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion g]
[IsClosedImmersion (f ≫ g)] : IsClosedImmersion f
where
base_closed := by
have h := (f ≫ g).isClosedEmbedding
simp only [Scheme.comp_coeBase, TopCat.coe_comp] at h
refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_
intro Z hZ
rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding, ← Set.image_comp]
exact h.isClosedMap _ hZ
surj_on_stalks
x := by
have h := (f ≫ g).stalkMap_surjective x
simp_rw [Scheme.stalkMap_comp] at h
exact Function.Surjective.of_comp h
