18.6. Subschemes
Mathlib does not have a definition of subschemes, we simply use morphisms Z ⟶ X
with the relevant properties. We give two prominent examples of such properties
and how to construct them.
18.6.1. Open subschemes
Given an open subset of X, we can naturally regard it as a scheme.
example (U : X.Opens) : Scheme := U
example (U : X.Opens) : (U : Scheme) ⟶ X := U.ι
Instead of working with U : X.Opens, it is often convenient to allow arbitrary
open immersions instead.
example (f : U ⟶ X) [IsOpenImmersion f] : X.Opens :=
f.opensRange
We rely on typeclass inference to automatically fill proofs using stability properties.
example (f : U ⟶ V) (g : V ⟶ X)
[IsOpenImmersion f] [IsOpenImmersion g] :
IsOpenImmersion (f ≫ g) :=
inferInstance
18.6.2. Closed subschemes
A closed subscheme is a morphism satisfying IsClosedImmersion. For example,
this proves that the range of a closed immersion is closed:
example (f : Y ⟶ X) [IsClosedImmersion f] :
IsClosed (Set.range f) :=
f.isClosedEmbedding.isClosed_range
A closed immersion determines an ideal sheaf.
example (f : Y ⟶ X) [IsClosedImmersion f] :
X.IdealSheafData :=
f.ker
And conversely, every ideal sheaf determines a closed immersion.
example :
(MorphismProperty.Over @IsClosedImmersion ⊤ X)ᵒᵖ ≌
X.IdealSheafData :=
IsClosedImmersion.overEquivIdealSheafData X