The finite affine cover of a scheme as one smooth surjection

Kollár's Proposition 37 [Kol07, Proposition 37] extends a blow-up sequence functor from affine schemes to all schemes of finite type over k by descent along the smooth surjection g : X' = ∐ᵢ Uᵢ → X from the disjoint union of a finite affine open cover, using the two projections τ₁, τ₂ : X'' → X' of the kernel pair X'' = X' ×_X X'. Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean has this setting on a Triple (a smooth X); the gluing of the resolution functor of [Kol07, Theorem 36] needs it for an arbitrary scheme X of finite type over k, since the input of the resolution functor is not smooth. This module provides the scheme-level part. The cover and its morphisms depend on X alone ([CompactSpace X], which a quasi-compact X → Spec k provides); the field enters only the structure morphisms and the finite-type, separated and affine statements:

• finiteAffineCover X, Mathlib's affine cover refined to a finite subcover; affineCoverScheme X (X'), affineCoverDesc X (g), affineCoverPair X (X''), affineCoverFst X, affineCoverSnd X (τ₁, τ₂);
• X' is affine (isAffine_affineCoverScheme), g is a smooth surjection (smooth_affineCoverDesc, surjective_affineCoverDesc; locality on the source, the pieces being open immersions) and a coproduct of open immersions (openImmersionCoprods_affineCoverDesc, the hypothesis of the descent exists_pullback_eq_of_kernelPair of Hironaka/Resolution/Algebraic/Kol07/GlobalizeDescent.lean); X' is of finite type, quasi-compact and separated over Spec k when X is of finite type;
• X'' is affine (isAffine_affineCoverPair; g is an affine morphism because X → Spec k is separated), τ₁, τ₂ are smooth surjections (base change of g), τ₁ ≫ g = τ₂ ≫ g, and the kernel pair is a pullback square (isPullback_affineCoverFst_affineCoverSnd).

The affineCover… names keep the base names distinct from Triple.cover… of Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean, whose statements are the instances of these at T.X.left.

The finite affine cover and its disjoint union

noncomputable def AlgebraicGeometry.finiteAffineCover (X : Scheme) [CompactSpace ↥X] : X.OpenCover

A finite affine open cover of the quasi-compact scheme X ("choose an open affine cover X = ∪ Uᵢ", the proof of [Kol07, Proposition 37]): Mathlib's affine cover, refined to a finite subcover.

Equations

• AlgebraicGeometry.finiteAffineCover X = X.affineCover.finiteSubcover

instance AlgebraicGeometry.finite_finiteAffineCover_I₀ (X : Scheme) [CompactSpace ↥X] : Finite (finiteAffineCover X).I₀

The finite subcover has a finite index type.

instance AlgebraicGeometry.isAffine_finiteAffineCover_X (X : Scheme) [CompactSpace ↥X] (i : (finiteAffineCover X).I₀) : IsAffine ((finiteAffineCover X).X i)

The members of the finite affine cover are affine.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineCoverScheme (X : Scheme) [CompactSpace ↥X] : Scheme

X' := ∐ᵢ Uᵢ, the disjoint union of the members of the finite affine cover (the proof of [Kol07, Proposition 37]).

Equations

• AlgebraicGeometry.affineCoverScheme X = ∐ fun (i : (AlgebraicGeometry.finiteAffineCover X).I₀) => (AlgebraicGeometry.finiteAffineCover X).X i

noncomputable def AlgebraicGeometry.affineCoverDesc (X : Scheme) [CompactSpace ↥X] : affineCoverScheme X ⟶ X

The morphism g : X' → X induced by the inclusions of the members of the cover, "a smooth surjection" in the proof of [Kol07, Proposition 37].

Equations

• AlgebraicGeometry.affineCoverDesc X = CategoryTheory.Limits.Sigma.desc (AlgebraicGeometry.finiteAffineCover X).f

theorem AlgebraicGeometry.isAffine_affineCoverScheme (X : Scheme) [CompactSpace ↥X] : IsAffine (affineCoverScheme X)

X' is affine.

instance AlgebraicGeometry.instIsAffineAffineCoverScheme (X : Scheme) [CompactSpace ↥X] : IsAffine (affineCoverScheme X)

theorem AlgebraicGeometry.ι_comp_affineCoverDesc (X : Scheme) [CompactSpace ↥X] (i : (finiteAffineCover X).I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : (finiteAffineCover X).I₀) => (finiteAffineCover X).X i) i) (affineCoverDesc X) = (finiteAffineCover X).f i

The piece inclusions.

theorem AlgebraicGeometry.ι_comp_affineCoverDesc_assoc (X : Scheme) [CompactSpace ↥X] (i : (finiteAffineCover X).I₀) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : (finiteAffineCover X).I₀) => (finiteAffineCover X).X i) i) (CategoryTheory.CategoryStruct.comp (affineCoverDesc X) h) = CategoryTheory.CategoryStruct.comp ((finiteAffineCover X).f i) h

The piece inclusions.

theorem AlgebraicGeometry.smooth_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverDesc X)

g is smooth: locality on the source, each piece being an open immersion.

instance AlgebraicGeometry.instSmoothAffineCoverDesc (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverDesc X)

theorem AlgebraicGeometry.smoothOfRelativeDimension_zero_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : SmoothOfRelativeDimension 0 (affineCoverDesc X)

g is smooth of relative dimension 0 (a coproduct of open immersions).

theorem AlgebraicGeometry.locallyOfFiniteType_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : LocallyOfFiniteType (affineCoverDesc X)

g is locally of finite type (a coproduct of open immersions).

theorem AlgebraicGeometry.surjective_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : Function.Surjective ⇑(affineCoverDesc X)

g is surjective (the pieces cover X).

theorem AlgebraicGeometry.openImmersionCoprods_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : openImmersionCoprods (affineCoverDesc X)

g is a coproduct of open immersions: X' is the coproduct of the members and each Sigma.ι i ≫ g = Uᵢ → X is an open immersion; the hypothesis of the kernel-pair descent exists_pullback_eq_of_kernelPair.

The kernel pair

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.affineCoverPair (X : Scheme) [CompactSpace ↥X] : Scheme

The kernel pair X'' = X' ×_X X' (Kollár's X'' := ∐_{i ≤ j} Uᵢ ∩ Uⱼ, of which "we can also think … as the fiber product X' ×_X X'", the proof of [Kol07, Proposition 37]).

Equations

• AlgebraicGeometry.affineCoverPair X = CategoryTheory.Limits.pullback (AlgebraicGeometry.affineCoverDesc X) (AlgebraicGeometry.affineCoverDesc X)

noncomputable def AlgebraicGeometry.affineCoverFst (X : Scheme) [CompactSpace ↥X] : affineCoverPair X ⟶ affineCoverScheme X

The first projection τ₁ : X'' → X' of the kernel pair.

Equations

• AlgebraicGeometry.affineCoverFst X = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.affineCoverDesc X) (AlgebraicGeometry.affineCoverDesc X)

noncomputable def AlgebraicGeometry.affineCoverSnd (X : Scheme) [CompactSpace ↥X] : affineCoverPair X ⟶ affineCoverScheme X

The second projection τ₂ : X'' → X' of the kernel pair.

Equations

• AlgebraicGeometry.affineCoverSnd X = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.affineCoverDesc X) (AlgebraicGeometry.affineCoverDesc X)

theorem AlgebraicGeometry.isPullback_affineCoverFst_affineCoverSnd (X : Scheme) [CompactSpace ↥X] : CategoryTheory.IsPullback (affineCoverFst X) (affineCoverSnd X) (affineCoverDesc X) (affineCoverDesc X)

The kernel pair of g is a pullback square.

theorem AlgebraicGeometry.affineCoverFst_comp_affineCoverDesc (X : Scheme) [CompactSpace ↥X] : CategoryTheory.CategoryStruct.comp (affineCoverFst X) (affineCoverDesc X) = CategoryTheory.CategoryStruct.comp (affineCoverSnd X) (affineCoverDesc X)

τ₁ ≫ g = τ₂ ≫ g.

theorem AlgebraicGeometry.smooth_affineCoverFst (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverFst X)

τ₁ is smooth (base change of g).

theorem AlgebraicGeometry.smooth_affineCoverSnd (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverSnd X)

τ₂ is smooth (base change of g).

instance AlgebraicGeometry.instSmoothAffineCoverFst (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverFst X)

instance AlgebraicGeometry.instSmoothAffineCoverSnd (X : Scheme) [CompactSpace ↥X] : Smooth (affineCoverSnd X)

theorem AlgebraicGeometry.smoothOfRelativeDimension_zero_affineCoverFst (X : Scheme) [CompactSpace ↥X] : SmoothOfRelativeDimension 0 (affineCoverFst X)

τ₁ is smooth of relative dimension 0 (base change of g).

theorem AlgebraicGeometry.surjective_affineCoverFst (X : Scheme) [CompactSpace ↥X] : Function.Surjective ⇑(affineCoverFst X)

τ₁ is surjective.

theorem AlgebraicGeometry.surjective_affineCoverSnd (X : Scheme) [CompactSpace ↥X] : Function.Surjective ⇑(affineCoverSnd X)

τ₂ is surjective.

Over the base field

theorem AlgebraicGeometry.compactSpace_of_quasiCompact_over (k : Type u) [Field k] (Y : Scheme) [Y.Over (Spec ↧k)] [QuasiCompact (Y ↘ Spec ↧k)] : CompactSpace ↥Y

A scheme quasi-compact over Spec k is a compact space (the hypothesis of the cover).

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instOverAffineCoverScheme (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : (affineCoverScheme X).Over (Spec ↧k)

X' is a scheme over Spec k through g.

Equations

• AlgebraicGeometry.instOverAffineCoverScheme X = { hom := CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.affineCoverDesc X) (X ↘ AlgebraicGeometry.Spec ↧k) }

instance AlgebraicGeometry.instIsOverAffineCoverDesc (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : Scheme.Hom.IsOver (affineCoverDesc X) (Spec ↧k)

g is a morphism over Spec k.

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

X' is locally of finite type over Spec k when X is.

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

theorem AlgebraicGeometry.quasiCompact_affineCoverScheme (X : Scheme) [CompactSpace ↥X] (k : Type u) [Field k] [X.Over (Spec ↧k)] : QuasiCompact (affineCoverScheme X ↘ Spec ↧k)

X' is quasi-compact over Spec k (affine over an affine base).

theorem AlgebraicGeometry.isSeparated_affineCoverScheme (X : Scheme) [CompactSpace ↥X] (k : Type u) [Field k] [X.Over (Spec ↧k)] : IsSeparated (affineCoverScheme X ↘ Spec ↧k)

X' is separated over Spec k (affine over an affine base).

instance AlgebraicGeometry.instIsSeparatedAffineCoverScheme (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : IsSeparated (affineCoverScheme X ↘ Spec ↧k)

theorem AlgebraicGeometry.isAffine_affineCoverPair (X : Scheme) [CompactSpace ↥X] (k : Type u) [Field k] [X.Over (Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] : IsAffine (affineCoverPair X)

X'' is affine: g is an affine morphism because X' → X → Spec k is affine and X → Spec k is separated, and the fibre product of g with itself is affine. Kollár's X'' is a disjoint union of the Uᵢ ∩ Uⱼ; that these are affine uses the separatedness of X, a point left implicit in his text.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instOverAffineCoverPair (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : (affineCoverPair X).Over (Spec ↧k)

X'' is a scheme over Spec k through τ₁.

Equations

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

instance AlgebraicGeometry.instIsOverAffineCoverFst (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : Scheme.Hom.IsOver (affineCoverFst X) (Spec ↧k)

τ₁ is a morphism over Spec k.

theorem AlgebraicGeometry.affineCoverSnd_comp_over (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : CategoryTheory.CategoryStruct.comp (affineCoverSnd X) (affineCoverScheme X ↘ Spec ↧k) = affineCoverPair X ↘ Spec ↧k

τ₂ is a morphism over Spec k (τ₁ ≫ g = τ₂ ≫ g).

instance AlgebraicGeometry.instIsOverAffineCoverSnd (X : Scheme) [CompactSpace ↥X] {k : Type u} [Field k] [X.Over (Spec ↧k)] : Scheme.Hom.IsOver (affineCoverSnd X) (Spec ↧k)

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

X'' is locally of finite type over Spec k when X is.

theorem AlgebraicGeometry.isSeparated_affineCoverPair (X : Scheme) [CompactSpace ↥X] (k : Type u) [Field k] [X.Over (Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] : IsSeparated (affineCoverPair X ↘ Spec ↧k)

X'' is separated over Spec k when X is (X'' is then affine over an affine base).