Reduced equidimensional schemes

The API of AlgebraicGeometry.Scheme.IsReducedEquidimensional k X (Hironaka.Scheme.Resolution.Defs): X is reduced and its smooth locus over k is smooth of one relative dimension. Its members are the objects of AlgebraicGeometry.ReducedEquidimensionalScheme, the inputs of Kollár's Theorem 36, and the resolution functor of the library (Hironaka.Resolution.BRFunctor) is constructed and proved on them.

The predicate is the equidimensionality of [Kol07, Notation 64 (1)] ("X is a smooth, equidimensional (possibly reducible) scheme of finite type over a field of characteristic zero", in force for the chapter that proves Theorem 36), transported to reduced, possibly singular schemes through Mathlib's Scheme.Hom.smoothLocus. The irreducible components of a member may meet. The class is stable under open subschemes and under finite disjoint unions of open subschemes of one member (Hironaka.Resolution.Algebraic.Kol07.Thm36.ClassClosure); it is not stable under arbitrary finite disjoint unions (a point and a line are not equidimensional). The empty scheme is a member (its smooth locus is smooth of every relative dimension). Why the equidimensionality is needed, and the stability of the class under change of fields and étale morphisms, are recorded in the docstring of AlgebraicGeometry.exists_functorial_resolution.

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.isReduced {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] (h : IsReducedEquidimensional k X) : IsReduced X

A member is reduced.

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.exists_smoothOfRelativeDimension {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] (h : IsReducedEquidimensional k X) : ∃ (d : ℕ), SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (Hom.smoothLocus (X ↘ Spec ↧k)).ι (X ↘ Spec ↧k))

The smooth locus of a member is smooth of one relative dimension.