The irreducible components of a reduced Noetherian scheme #
Facts about an irreducible component C of a reduced Noetherian scheme X, used by the resolution
functor of [Kol07, Theorem 36] on reduced equidimensional schemes, where the components may meet.
Mathlib's open neighbourhood X.irreducibleComponentOpen C, the complement of the other
components, is a nonempty open subscheme contained in C with closure C, hence integral
(isIntegral_irreducibleComponentOpen_of_isReduced); its generic point is a generic point of C
and lies in the smooth locus of X over a perfect field (exists_isGenericPoint_mem_smoothLocus);
the reduced closed subscheme X.irreducibleComponentIdeal C of C is integral
(isIntegral_irreducibleComponent_of_isReduced), and so is its push-forward along a closed
immersion (isIntegral_subscheme_map_irreducibleComponentIdeal_of_isReduced); the
generic point of C pushed along a closed immersion is a generic point of the pushed subscheme
(isGenericPoint_map_irreducibleComponentIdeal); and a flat morphism sends the generic point of a
component to the generic point of the component containing its image (map_genericPoint_eq_of_flat,
comap_irreducibleComponentIdeal_le). No disjointness of the components is assumed.
Mathlib's irreducibleComponentIdeal C is the kernel of the inclusion of the open neighbourhood,
so its reducedness is that of a scheme-theoretic image: the kernel of a morphism from a reduced
scheme is radical (radical_ker_eq_self), so the image is reduced (isReduced_image).
The scheme-theoretic image of a reduced scheme is reduced #
The kernel of a morphism from a reduced scheme is radical: its radical has, on every affine
open U, an ideal contained in the radical of ker (f.app U), which is ker (f.app U) itself
since the sections of the reduced source form a reduced ring, and the kernel is the largest ideal
sheaf below these kernels (Scheme.IdealSheafData.le_ofIdeals_iff).
The scheme-theoretic image of a morphism from a reduced scheme is reduced
(radical_ker_eq_self, isReduced_subscheme_of_radical_eq_self).
The open neighbourhood of a component #
The open neighbourhood of a component is contained in the component: a point outside the other
components lies on its own component, which is C.
The closure of the open neighbourhood of a component is the component (Mathlib's
closure_sUnion_irreducibleComponents_sdiff_singleton).
On a reduced Noetherian scheme the open neighbourhood of a component is an integral scheme:
reduced as an open of X, irreducible since its closure is the irreducible C.
Every component of a reduced scheme of finite type over a perfect field has a generic point in
the smooth locus: the generic point of the integral open neighbourhood of the component is a generic
point of the component (its closure is the component) and a smooth point
(Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField).
The reduced closed subscheme of a component #
On a reduced Noetherian scheme the reduced closed subscheme of a component is integral:
irreducible, its support being the irreducible C, and reduced as the scheme-theoretic image of
the open neighbourhood of the component (isReduced_image).
The reduced ideal of a component of a reduced Noetherian scheme pushed along a closed immersion
emb has an integral subscheme: V(I_C) → X → A is a closed immersion from an integral scheme with
kernel I_C.map emb.
The support of the reduced ideal of a component is the component.
The generic point of a component C of X, pushed along a closed immersion emb, is the
generic point of the support of the reduced ideal of C pushed to the ambient.
Components along a flat morphism #
A flat map sends the generic point of a component D of Z to the generic point of the
component C ⊇ f(D) of X: generalisations lift along flat maps, and the generic point of a
component has no proper generalisation.
If the component D of the reduced Noetherian Z maps into the component C of X under
f, the pullback of the reduced ideal of C lies in that of D (the Galois connection
le_support_iff_le_vanishingIdeal; the reduced ideal of D is radical).