Subscheme structure on an irreducible component

We define the subscheme structure on an irreducible component of a Noetherian scheme. Typically, one takes the reduced induced subscheme structure, but this will throw away information if the irreducible component is not already reduced. Instead, we take the closed subscheme defined by the kernel of the restriction to the complement of the union of the other irreducible components. For example, if X is irreducible then this will give back the original scheme X.

Main definition

• AlgebraicGeometry.Scheme.irreducibleComponentIdeal: The ideal sheaf data associated to an irreducible component of a Noetherian scheme.
• AlgebraicGeometry.Scheme.irreducibleComponent: The subscheme structure on an irreducible component of a Noetherian scheme.

TODO

Prove that for affine schemes this subscheme structure is defined by the kernel of the localization away from the union of the other minimal prime ideals.

def AlgebraicGeometry.Scheme.irreducibleComponentOpen (X : Scheme) (Z : Set ↥X) [IsNoetherian X] : X.Opens

The complement of the irreducible components unequal to Z of a Noetherian scheme.

Equations

• X.irreducibleComponentOpen Z = { carrier := (⋃₀ (irreducibleComponents ↥X \ {Z}))ᶜ, is_open' := ⋯ }

def AlgebraicGeometry.Scheme.irreducibleComponentIdeal (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : X.IdealSheafData

The ideal sheaf data associated to an irreducible component of a Noetherian scheme.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.irreducibleComponentIdeal_def (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : X.irreducibleComponentIdeal Z hZ = Hom.ker (X.irreducibleComponentOpen Z).ι

noncomputable def AlgebraicGeometry.Scheme.irreducibleComponent (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : Scheme

The subscheme structure on an irreducible component of a Noetherian scheme.

Equations

• X.irreducibleComponent Z hZ = (X.irreducibleComponentIdeal Z hZ).subscheme

noncomputable def AlgebraicGeometry.Scheme.irreducibleComponentι (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : X.irreducibleComponent Z hZ ⟶ X

The inclusion from an irreducible component of a Noetherian scheme.

Equations

• X.irreducibleComponentι Z hZ = (X.irreducibleComponentIdeal Z hZ).subschemeι

theorem AlgebraicGeometry.Scheme.irreducibleComponentι_apply (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] (x : ↥(X.irreducibleComponent Z hZ)) : (X.irreducibleComponentι Z hZ) x = ↑x

instance AlgebraicGeometry.Scheme.instIsClosedImmersionIrreducibleComponentι (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : IsClosedImmersion (X.irreducibleComponentι Z hZ)

instance AlgebraicGeometry.Scheme.instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] : IrreducibleSpace ↥(X.irreducibleComponent Z hZ)

theorem AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] [IrreducibleSpace ↥X] : X.irreducibleComponentOpen Z = ⊤

instance AlgebraicGeometry.Scheme.instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat (X : Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) [IsNoetherian X] [IrreducibleSpace ↥X] : CategoryTheory.IsIso (X.irreducibleComponentι Z hZ)