Reduced induced closed subschemes

5 fully proved

Ideal Sheaf Data

TheoremThe subscheme cut out by a vanishing ideal is reduced#✓fully proved

The subscheme cut out by a vanishing ideal is reduced.

theorem isReduced_subscheme_vanishingIdeal {X : Scheme.{u}} (Z : Closeds X) :
    IsReduced (vanishingIdeal Z).subscheme

Used by 1

Used byReducedness and kernel bound for the vanishing-ideal subscheme

TheoremVanishing ideal lies in the kernel of maps from reduced schemes#✓fully proved

The vanishing ideal of a closed subset is contained in the kernel of any map from a reduced scheme landing in the subset.

theorem vanishingIdeal_le_ker {X : Scheme.{u}} {T : Scheme.{u}} [IsReduced T] (Z : Closeds X)
    (f : T ⟶ X) (hf : Set.range f ⊆ Z) : vanishingIdeal Z ≤ f.ker

Used by 2

Used byUniversal property of the reduced subscheme on a closed subset · Reducedness and kernel bound for the vanishing-ideal subscheme

TheoremUniversal property of the reduced subscheme on a closed subset#✓fully proved

A map from a reduced scheme landing in a closed subset lifts uniquely to the subscheme cut out by the vanishing ideal.

theorem exists_lift_subschemeι_vanishingIdeal {X : Scheme.{u}} {T : Scheme.{u}} [IsReduced T]
    (Z : Closeds X) (f : T ⟶ X) (hf : Set.range f ⊆ Z) :
    ∃! g : T ⟶ (vanishingIdeal Z).subscheme, g ≫ (vanishingIdeal Z).subschemeι = f

Uses 1

Proof usesVanishing ideal lies in the kernel of maps from reduced schemes

TheoremReducedness and kernel bound for the vanishing-ideal subscheme#✓fully proved

The subscheme cut out by a vanishing ideal is reduced, and its ideal sheaf is contained in the kernel of any map from a reduced scheme landing in the subset.

theorem isReduced_subscheme_vanishingIdeal_and_le_ker {X : Scheme.{u}} (Z : Closeds X) :
    IsReduced (vanishingIdeal Z).subscheme ∧
      ∀ {T : Scheme.{u}} [IsReduced T] (f : T ⟶ X), Set.range f ⊆ Z →
        vanishingIdeal Z ≤ f.ker

Uses 2 · Used by 1

Proof usesThe subscheme cut out by a vanishing ideal is reduced · Vanishing ideal lies in the kernel of maps from reduced schemes

Used byUnique lifting of maps from reduced schemes through closed immersions

Algebraic Geometry

TheoremUnique lifting of maps from reduced schemes through closed immersions#✓fully proved

A map from a reduced scheme into a closed immersion whose range contains the image lifts uniquely.

theorem IsClosedImmersion.existsUnique_comp_eq_of_range_subset_of_isReduced
    {X Y T : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i] (f : T ⟶ X) [IsReduced T]
    (H : Set.range f.base ⊆ Set.range i.base) :
    ∃! g : T ⟶ Y, g ≫ i = f

Uses 1

Proof usesReducedness and kernel bound for the vanishing-ideal subscheme

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.