English
Let f: X → Y and g: Y → Z be morphisms of schemes with g an open immersion and f ∘ g an open immersion. Then f is an open immersion.
Русский
Пусть f: X → Y и g: Y → Z — морфизмы схем. Если g является открытым вложением, а композиция f ∘ g — открытым вложением, то f является открытым вложением.
LaTeX
$$$\text{IsOpenImmersion}(g) \wedge \text{IsOpenImmersion}(f \circ g) \Rightarrow \text{IsOpenImmersion}(f)$$$
Lean4
theorem of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g] [IsOpenImmersion (f ≫ g)] :
IsOpenImmersion f :=
haveI (x : X) : IsIso (f.stalkMap x) :=
haveI : IsIso (g.stalkMap (f.base x) ≫ f.stalkMap x) :=
by
rw [← Scheme.stalkMap_comp]
infer_instance
IsIso.of_isIso_comp_left (f := g.stalkMap (f.base x)) _
IsOpenImmersion.of_stalk_iso _ <|
IsOpenEmbedding.of_comp _ (Scheme.Hom.isOpenEmbedding g) (Scheme.Hom.isOpenEmbedding (f ≫ g))
