Closure properties of the classes of inputs

The functorial resolution theorem AlgebraicGeometry.exists_functorial_resolution is stated on the class IsReducedEquidimensional k X of reduced schemes whose smooth locus over k is smooth of one relative dimension (Hironaka.Scheme.Resolution.Defs). The descent of [Kol07, Proposition 37] constructs the resolution functor from the affine cover X' = ∐ Uᵢ → X through the kernel pair X'' = X' ×_X X', so Hironaka.Resolution.Algebraic.Kol07.Thm36.BR needs X' and X'' in the class whenever X is, and the affine functoriality (Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineFunctoriality) needs the coproducts of its charts in the class. The second part of this file proves these closure properties:

• IsReducedEquidimensional.of_isOpenImmersion: open subschemes over k (smoothOfRelativeDimension_of_isOpenImmersion: the smooth locus of an open subscheme is the preimage of the smooth locus, preimage_smoothLocus_eq, and the restricted open immersion is étale);
• IsReducedEquidimensional.of_openCover: a scheme covered by reduced opens whose smooth loci have ONE common relative dimension d (SmoothOfRelativeDimension d is Zariski-local at the source);
• IsReducedEquidimensional.of_openCover_of_isOpenImmersion, .sigma: a scheme covered by open subschemes of ONE member, over k, and in particular a disjoint union ∐ Wᵢ of open subschemes of one member — the class is NOT closed under arbitrary disjoint unions (a point and a line);
• IsReducedEquidimensional.affineCoverScheme, .affineCoverPair: Kollár's X' and X'';
• isReducedEquidimensional_of_isIntegral: an integral algebraic k-scheme is a member.

The first part of the file is the corresponding closure theory of the class HasDisjointIntegralComponents X of reduced schemes with pairwise disjoint irreducible components, finite disjoint unions of integral schemes, used by Hironaka's Main Theorems on regular schemes (Hironaka.Resolution.Algebraic.Hir64). The same descent needs X' and X'' in the class whenever X is, and the components' open neighbourhoods irreducibleComponentOpen in the class too. This file proves the closure properties:

• HasDisjointIntegralComponents.of_isOpenImmersion: open subschemes (the components of an open subspace are the traces of the components meeting it, exists_eq_preimage_of_mem_irreducibleComponents);
• HasDisjointIntegralComponents.of_openCover_of_pairwise_disjoint: a scheme covered by pairwise disjoint open subschemes in the class (an irreducible set inside such a cover lies in one member, subset_of_isPreirreducible_of_pairwise_disjoint);
• HasDisjointIntegralComponents.sigma: disjoint unions ∐ Z (Mathlib's sigmaOpenCover, disjoint_opensRange_sigmaι);
• HasDisjointIntegralComponents.affineCoverScheme, .affineCoverPair: Kollár's X' and X'' (the affine opens, respectively their pairwise fibre products, are open subschemes of X);
• the component lemmas: irreducibleComponentOpen_eq, on the class Mathlib's open neighbourhood of a component IS the component; support_irreducibleComponentIdeal.

Irreducible components under open embeddings and disjoint covers (topology)

theorem Hironaka.Resolution.exists_eq_preimage_of_mem_irreducibleComponents {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsOpenEmbedding f) {D : Set Y} (hD : D ∈ irreducibleComponents Y) : ∃ C ∈ irreducibleComponents X, D = f ⁻¹' C

Every irreducible component of the source of an open embedding is the preimage of an irreducible component of the target.

theorem Hironaka.Resolution.subset_of_isPreirreducible_of_pairwise_disjoint {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {U : ι → Set X} (hU : ∀ (i : ι), IsOpen (U i)) (hd : Pairwise fun (i j : ι) => Disjoint (U i) (U j)) (hcov : ∀ (x : X), ∃ (i : ι), x ∈ U i) {S : Set X} (hS : IsPreirreducible S) {i : ι} (hi : (S ∩ U i).Nonempty) : S ⊆ U i

A preirreducible set inside a union of pairwise disjoint open sets that meets one of them lies in it.

The class is closed under open subschemes, disjoint covers and disjoint unions

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.of_isOpenImmersion {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] (hX : X.HasDisjointIntegralComponents) : Y.HasDisjointIntegralComponents

An open subscheme of a member of the class is in the class: reducedness is local, and two components of Y meeting are the traces of two components of X meeting.

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.of_openCover_of_pairwise_disjoint {X : Scheme} (𝒰 : X.OpenCover) (hd : Pairwise fun (i j : 𝒰.I₀) => Disjoint (Set.range ⇑(𝒰.f i)) (Set.range ⇑(𝒰.f j))) (h : ∀ (i : 𝒰.I₀), (𝒰.X i).HasDisjointIntegralComponents) : X.HasDisjointIntegralComponents

A scheme covered by pairwise disjoint open subschemes in the class is in the class: an irreducible component lies in one member of the cover, and two components meeting lie in the same member, where they are the images of two meeting components.

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.sigma {ι : Type u} (Z : ι → Scheme) (h : ∀ (i : ι), (Z i).HasDisjointIntegralComponents) : (∐ Z).HasDisjointIntegralComponents

A disjoint union of members of the class is in the class ("X' := ∐ Uᵢ", Kol07, Proposition 37, proof).

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.affineCoverScheme {X : Scheme} [CompactSpace ↥X] (hX : X.HasDisjointIntegralComponents) : (AlgebraicGeometry.affineCoverScheme X).HasDisjointIntegralComponents

The finite affine cover X' = ∐ Uᵢ of a member of the class is in the class Kol07, Proposition 37, proof.

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.affineCoverPair {X : Scheme} [CompactSpace ↥X] (hX : X.HasDisjointIntegralComponents) : (AlgebraicGeometry.affineCoverPair X).HasDisjointIntegralComponents

The kernel pair X'' = X' ×_X X' of the affine cover of a member of the class is in the class ("the disjoint union of the Uᵢ ∩ Uⱼ", [Kol07, Proposition 37, proof]): it is covered by the pairwise disjoint open subschemes Uᵢ ×_X X' (the base changes of the pieces Uᵢ → X), each an open subscheme of X'.

The components on the class

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.irreducibleComponentOpen_eq {X : Scheme} [IsNoetherian X] (hX : X.HasDisjointIntegralComponents) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) : ↑(X.irreducibleComponentOpen Z) = Z

On the class, Mathlib's open neighbourhood of a component, the complement of the other components, is the component itself.

theorem AlgebraicGeometry.Scheme.HasDisjointIntegralComponents.of_isIntegral (X : Scheme) [IsIntegral X] : X.HasDisjointIntegralComponents

An integral scheme is in the class: reduced, with a single irreducible component (irreducibleComponents_eq_singleton).

theorem Hironaka.Resolution.support_irreducibleComponentIdeal {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X) : ↑(X.irreducibleComponentIdeal Z hZ).support = Z

The support of the reduced ideal of an irreducible component is the component.

instance Hironaka.Resolution.instLocallyOfFiniteTypeAffineCoverPair (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : AlgebraicGeometry.LocallyOfFiniteType (AlgebraicGeometry.affineCoverPair X ↘ AlgebraicGeometry.Spec ↧k)

The kernel pair X'' = X' ×_X X' of the finite affine cover is locally of finite type over k (locallyOfFiniteType_affineCoverPair), the instance needed to evaluate the affine construction on it (the condition (37.1) of [Kol07, Proposition 37]).

instance Hironaka.Resolution.instQuasiCompactAffineCoverPair (k : Type u) [Field k] (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsSeparated (X ↘ AlgebraicGeometry.Spec ↧k)] : AlgebraicGeometry.QuasiCompact (AlgebraicGeometry.affineCoverPair X ↘ AlgebraicGeometry.Spec ↧k)

The kernel pair of the finite affine cover of a separated X is affine (isAffine_affineCoverPair), hence quasi-compact over k: the instance needed to evaluate the affine construction on it.

The class of reduced equidimensional schemes

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.smoothOfRelativeDimension_of_isOpenImmersion {k : Type u} [Field k] {X Y : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] (f : Y ⟶ X) [IsOpenImmersion f] (φ : Y ⟶ Spec ↧k) [LocallyOfFinitePresentation φ] (hφ : CategoryTheory.CategoryStruct.comp f (X ↘ Spec ↧k) = φ) {d : ℕ} [SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (Hom.smoothLocus (X ↘ Spec ↧k)).ι (X ↘ Spec ↧k))] : SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (Hom.smoothLocus φ).ι φ)

The smooth locus over k of an open subscheme f : Y ⟶ X, with Y over k through φ = f ≫ (X ↘ Spec k), is smooth of the relative dimension of the smooth locus of X: it is the preimage of the smooth locus of X (preimage_smoothLocus_eq), and the restriction of f to the smooth loci is an open immersion, étale.

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.of_isOpenImmersion {k : Type u} [Field k] {X Y : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] [Y.Over (Spec ↧k)] [LocallyOfFiniteType (Y ↘ Spec ↧k)] (f : Y ⟶ X) [IsOpenImmersion f] [Hom.IsOver f (Spec ↧k)] (hX : IsReducedEquidimensional k X) : IsReducedEquidimensional k Y

An open subscheme over k of a member of the class is in the class: reducedness is local, and the smooth locus is the preimage of the smooth locus (smoothOfRelativeDimension_of_isOpenImmersion).

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.of_openCover {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] (𝒰 : X.OpenCover) (d : ℕ) (hred : ∀ (i : 𝒰.I₀), IsReduced (𝒰.X i)) (hd : ∀ (i : 𝒰.I₀), SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (Hom.smoothLocus (CategoryTheory.CategoryStruct.comp (𝒰.f i) (X ↘ Spec ↧k))).ι (CategoryTheory.CategoryStruct.comp (𝒰.f i) (X ↘ Spec ↧k)))) : IsReducedEquidimensional k X

A scheme covered by reduced open subschemes whose smooth loci over k all have the relative dimension d is in the class: SmoothOfRelativeDimension d is Zariski-local at the source, and the smooth locus of X is covered by its traces on the pieces, each an open subscheme of the smooth locus of the piece.

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.of_openCover_of_isOpenImmersion {k : Type u} [Field k] {X Y : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] [Y.Over (Spec ↧k)] [LocallyOfFiniteType (Y ↘ Spec ↧k)] (hY : IsReducedEquidimensional k Y) (𝒰 : X.OpenCover) (e : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (hoi : ∀ (i : 𝒰.I₀), IsOpenImmersion (e i)) (he : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) (X ↘ Spec ↧k) = CategoryTheory.CategoryStruct.comp (e i) (Y ↘ Spec ↧k)) : IsReducedEquidimensional k X

A scheme covered by open subschemes of ONE member Y, compatibly over k, is in the class: the pieces are reduced and their smooth loci have the relative dimension of that of Y (smoothOfRelativeDimension_of_isOpenImmersion).

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.sigma {k : Type u} [Field k] {ι : Type u} {Y : Scheme} [Y.Over (Spec ↧k)] [LocallyOfFiniteType (Y ↘ Spec ↧k)] (W : ι → Scheme) (e : (i : ι) → W i ⟶ Y) [∀ (i : ι), IsOpenImmersion (e i)] [(∐ W).Over (Spec ↧k)] [LocallyOfFiniteType ((∐ W) ↘ Spec ↧k)] (hover : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι W i) ((∐ W) ↘ Spec ↧k) = CategoryTheory.CategoryStruct.comp (e i) (Y ↘ Spec ↧k)) (hY : IsReducedEquidimensional k Y) : IsReducedEquidimensional k (∐ W)

A disjoint union ∐ Wᵢ of open subschemes e i : Wᵢ ⟶ Y of one member Y, over k compatibly with the e i, is in the class ("X' := ∐ Uᵢ", [Kol07, Proposition 37, proof]).

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.affineCoverScheme {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] [CompactSpace ↥X] (hX : IsReducedEquidimensional k X) : IsReducedEquidimensional k (AlgebraicGeometry.affineCoverScheme X)

The finite affine cover X' = ∐ Uᵢ of a member of the class is in the class Kol07, Proposition 37, proof.

theorem AlgebraicGeometry.Scheme.IsReducedEquidimensional.affineCoverPair {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] [CompactSpace ↥X] (hX : IsReducedEquidimensional k X) : IsReducedEquidimensional k (AlgebraicGeometry.affineCoverPair X)

The kernel pair X'' = X' ×_X X' of the affine cover of a member of the class is in the class ("the disjoint union of the Uᵢ ∩ Uⱼ", [Kol07, Proposition 37, proof]): it is covered by the open subschemes Uᵢ ×_X X' of X' (the base changes of the pieces Uᵢ → X).

theorem Hironaka.Resolution.isReducedEquidimensional_of_isIntegral {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] : AlgebraicGeometry.Scheme.IsReducedEquidimensional k X

An integral scheme locally of finite type over a field k of characteristic zero is a member of the class IsReducedEquidimensional k X of the functorial resolution theorem (Kollár's equidimensional schemes, [Kol07, Notation 64]). It is reduced; the smooth locus of X over k contains the generic point (genericPoint_mem_smoothLocus_of_perfectField), so it is a nonempty open subscheme of the integral X, itself integral hence preconnected, smooth over k (preimage_smoothLocus_eq with smoothLocus_eq_top_iff), and of one relative dimension by exists_smoothOfRelativeDimension_of_preconnectedSpace.