Closed subschemes of a scheme over a base

If X is a scheme over S and I is an ideal sheaf on X, the closed subscheme V(I) is a scheme over S through its inclusion V(I) ⟶ X ⟶ S, and the inclusion is then an S-morphism.

Main definitions

• AlgebraicGeometry.Scheme.IdealSheafData.instOverSubscheme: the structure of scheme over S on V(I).

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.over_eq_subschemeι_comp: the structure morphism of V(I) is the inclusion followed by the structure morphism of X.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.IdealSheafData.instOverSubscheme {X S : Scheme} [X.Over S] (I : X.IdealSheafData) : I.subscheme.Over S

A closed subscheme of a scheme over S is a scheme over S through its inclusion.

theorem AlgebraicGeometry.Scheme.IdealSheafData.over_eq_subschemeι_comp {X S : Scheme} [X.Over S] (I : X.IdealSheafData) : I.subscheme ↘ S = CategoryTheory.CategoryStruct.comp I.subschemeι (X ↘ S)

The structure morphism of a closed subscheme over S is its inclusion followed by the structure morphism of the ambient scheme.

instance AlgebraicGeometry.Scheme.IdealSheafData.isOver_subschemeι {X S : Scheme} [X.Over S] (I : X.IdealSheafData) : Hom.IsOver I.subschemeι S

The inclusion of a closed subscheme is a morphism over S.