Sections cut out by ideal sheaves

Let f : X ⟶ S be a morphism of schemes. A section s of f which is a closed immersion, for instance any section of a separated morphism, is determined by its ideal sheaf s.ker: a second section t of f with s.ker ≤ t.ker is equal to s. Conversely, an ideal sheaf I on X is the ideal sheaf of a section of a separated morphism f exactly when its closed subscheme V(I) maps isomorphically to S, and the section is then the inverse of V(I) ⟶ S followed by the inclusion V(I) ⟶ X.

On a relative curve, this is how a relative effective Cartier divisor of degree one is the divisor of a unique section.

Main declarations

• AlgebraicGeometry.Scheme.Hom.isClosedImmersion_of_comp_eq_id: a section of a separated morphism is a closed immersion;
• AlgebraicGeometry.Scheme.Hom.ker_le_ker_iff_of_comp_eq_id: a section of f which is a closed immersion is determined by its ideal sheaf;
• AlgebraicGeometry.Scheme.Hom.ker_eq_ker_iff_of_comp_eq_id: two sections of a separated morphism are equal exactly when their ideal sheaves are;
• AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso: the section cut out by an ideal sheaf whose closed subscheme maps isomorphically to S, characterised by AlgebraicGeometry.Scheme.IdealSheafData.eq_sectionOfIsIso_iff;
• AlgebraicGeometry.Scheme.IdealSheafData.isIso_subschemeι_comp_iff: an ideal sheaf is the ideal sheaf of a section of a separated morphism f exactly when its closed subscheme maps isomorphically to the base.

theorem AlgebraicGeometry.Scheme.Hom.isClosedImmersion_of_comp_eq_id {X S : Scheme} (s : S ⟶ X) {f : X ⟶ S} [IsSeparated f] (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) : IsClosedImmersion s

A section of a separated morphism is a closed immersion.

theorem AlgebraicGeometry.Scheme.Hom.ker_le_ker_iff_of_comp_eq_id {X S : Scheme} (s t : S ⟶ X) {f : X ⟶ S} [IsClosedImmersion s] (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (ht : CategoryTheory.CategoryStruct.comp t f = CategoryTheory.CategoryStruct.id S) : ker s ≤ ker t ↔ s = t

A closed-immersion section is determined by its ideal sheaf. If s and t are sections of f : X ⟶ S and s is a closed immersion, then the ideal sheaf of s is contained in that of t exactly when s = t.

theorem AlgebraicGeometry.Scheme.Hom.ker_eq_ker_iff_of_comp_eq_id {X S : Scheme} (s t : S ⟶ X) {f : X ⟶ S} [IsSeparated f] (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (ht : CategoryTheory.CategoryStruct.comp t f = CategoryTheory.CategoryStruct.id S) : ker s = ker t ↔ s = t

Two sections of a separated morphism are equal exactly when their ideal sheaves are.

theorem AlgebraicGeometry.Scheme.Hom.isIso_ker_subschemeι_comp {X S : Scheme} (s : S ⟶ X) {f : X ⟶ S} [IsClosedImmersion s] (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (ker s).subschemeι f)

The closed subscheme cut out by a closed-immersion section s of f : X ⟶ S maps isomorphically to S.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : S ⟶ X

The section cut out by an ideal sheaf I on X whose closed subscheme V(I) maps isomorphically to S under f : X ⟶ S: the inverse of V(I) ⟶ S followed by the inclusion V(I) ⟶ X. It is the unique section of f with ideal sheaf I (eq_sectionOfIsIso_iff).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso_comp {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : CategoryTheory.CategoryStruct.comp (sectionOfIsIso f I) f = CategoryTheory.CategoryStruct.id S

The section cut out by I is a section of f.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionOfIsIso_comp_assoc {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (sectionOfIsIso f I) (CategoryTheory.CategoryStruct.comp f h) = h

The section cut out by I is a section of f.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_comp_comp_sectionOfIsIso {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : CategoryTheory.CategoryStruct.comp I.subschemeι (CategoryTheory.CategoryStruct.comp f (sectionOfIsIso f I)) = I.subschemeι

The section cut out by I factors through the inclusion V(I) ⟶ X: precomposing it with V(I) ⟶ S gives back that inclusion.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_comp_comp_sectionOfIsIso_assoc {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp I.subschemeι (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (sectionOfIsIso f I) h)) = CategoryTheory.CategoryStruct.comp I.subschemeι h

The section cut out by I factors through the inclusion V(I) ⟶ X: precomposing it with V(I) ⟶ S gives back that inclusion.

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsClosedImmersionSectionOfIsIso {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : IsClosedImmersion (sectionOfIsIso f I)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_sectionOfIsIso {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : Hom.ker (sectionOfIsIso f I) = I

The ideal sheaf of the section cut out by I is I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_sectionOfIsIso_iff {X S : Scheme} (f : X ⟶ S) (I : X.IdealSheafData) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f)] {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) : s = sectionOfIsIso f I ↔ Hom.ker s = I

The section cut out by I is the unique section with ideal sheaf I. A section s of f is the section cut out by I exactly when its ideal sheaf is I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isIso_subschemeι_comp_iff {X S : Scheme} {f : X ⟶ S} [IsSeparated f] (I : X.IdealSheafData) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp I.subschemeι f) ↔ ∃ (s : S ⟶ X), CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S ∧ Hom.ker s = I

Ideal sheaves of sections. An ideal sheaf I on X is the ideal sheaf of a section of a separated morphism f : X ⟶ S exactly when its closed subscheme maps isomorphically to S.