The proof of Theorem 105: the local cover, the kernel pair, uniqueness of the extension

Kollár's proof of the globalization theorem [Kol07, Theorem 105] for M = {open immersions}, in this library the class openImmersionCoprods of coproducts of open immersions, has four moves: (a) a global triple (X, I, E) is covered by finitely many local M-covers gₓᵢ : Uₓᵢ → X (clause (i) of the data at every point, quasi-compactness of X), and X' := ∐ᵢ Uₓᵢ with g : X' → X is a local triple by clause (ii); (b) X'' := X' ×_X X' with its projections τ₁, τ₂ is a local triple (the hypothesis LocalCoversFibreClosed) and the τᵢ are surjective members of M; (c) B commutes with the τᵢ, so τ₁^* B(X') = B(X'') = τ₂^* B(X'); (d) the sequence B(X') descends to X along g (the gluing of Proposition 37, Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Descent.lean), and the extension is B̄(X) := that descent. This module proves (a), (b) and (c), the uniqueness of the extension, the instance of the hypotheses for the classes of Proposition 37 (all triples, affine triples), and two lemmas on the class; the descent (d) and the construction of B̄ are in Hironaka/Resolution/Algebraic/Kol07/GlobalizeDescent.lean.

The class lemmas

Composition (openImmersionCoprods_comp): if Y = ∐ᵢ Uᵢ maps to Z = ∐ⱼ Vⱼ by open immersions on the summands and Z maps to W likewise, then Y is the coproduct of the Uᵢ ×_Z Vⱼ (open subschemes of the Uᵢ, disjoint, covering) and each maps to W by an open immersion. Used for the composite local cover Y' → Y → X of the commutation step.

Separatedness (openImmersionCoprods_isSeparated): a coproduct of open immersions f : Y → X is separated. The diagonal Y → Y ×_X Y is an immersion (Mathlib), so it is a closed immersion as soon as its range is closed; the complement of the range is the union of the opens τ₁^{-1}(Uᵢ) ∩ τ₂^{-1}(Uⱼ) for i ≠ j — a point over (Uᵢ, Uᵢ) lies in the image of Uᵢ ×_X Uᵢ → Y ×_X Y, and Uᵢ ×_X Uᵢ ≅ Uᵢ by the diagonal because Uᵢ → X is a monomorphism, so such a point is on the diagonal; a point over (Uᵢ, Uⱼ) with i ≠ j is not, the summands being disjoint. This is what makes X' and X'' triples: X' → Spec k factors through the separated g, and X'' → Spec k through the separated τ₁.

The statements proved here

• The local cover: Triple.exists_finite_localCover is clause (i) at every point plus a finite subcover (CompactSpace X from QuasiCompact (X → Spec k), the ranges of members of M being open); Triple.exists_isLocalCover builds X' = ∐ Uₓᵢ as the pullback triple Triple.pullback of T along g = Sigma.desc, which is a coproduct of open immersions (sigmaDesc), smooth and separated, with X' quasi-compact (a finite coproduct of quasi-compact schemes) and of the relative dimension of X (g étale), and shows X' ∈ LT by clause (ii): X' is the disjoint union of the Uₓᵢ with the restricted data (IsSigmaOf).
• The kernel pair: Triple.exists_kernelPair takes Mathlib's pullback g g with its projections: they are in M by base change, surjective (a point y' lifts to (y', y')), and X'' is Triple.pullback of X' along τ₁; the data along τ₂ agree because τ₁ ≫ g = τ₂ ≫ g; X'' ∈ LT is the hypothesis LocalCoversFibreClosed applied to the cover twice.
• The descent datum: OrderSeqAssignment.pullback_eq_of_kernelPair is two applications of the hypothesis on B.
• Uniqueness (OrderSeqAssignment.globalization_unique): for two extensions and a global T with a point, g^* B̄ᵢ(T) = B̄ᵢ(X') = B(X') along a local cover (X' ∈ GT by hLG), and pullback along the surjective flat g is injective (pullback_injective_of_surjective); on an empty T.X.left both values are nil, every center on the empty scheme being empty (eq_nil_of_noEmptyCenters).
• The instance (globalizationData_isAffineScheme, localCoversFibreClosed_isAffineScheme): every point of a triple lies in an affine open, whose triple is affine and local; the affine triples are closed under finite disjoint unions; and the fibre product of two affine local covers is affine because X is separated over k (g₂ is then an affine morphism and the base change of an affine morphism to an affine scheme is affine). This is the setting of [Kol07, Proposition 37], recovered from Theorem 105.

Lemmas on the class of coproducts of open immersions

theorem Hironaka.Sequence.openImmersionCoprods.isOpen_range {X Y : AlgebraicGeometry.Scheme} {f : Y ⟶ X} (hf : AlgebraicGeometry.openImmersionCoprods f) : IsOpen (Set.range ⇑f)

The range of a coproduct of open immersions is open (the union of the ranges of the summands).

theorem Hironaka.Sequence.openImmersionCoprods.smooth {X Y : AlgebraicGeometry.Scheme} {f : Y ⟶ X} (hf : AlgebraicGeometry.openImmersionCoprods f) : AlgebraicGeometry.Smooth f

A coproduct of open immersions is smooth (it is étale, openImmersionCoprods_etale).

theorem Hironaka.Sequence.openImmersionCoprods.flat {X Y : AlgebraicGeometry.Scheme} {f : Y ⟶ X} (hf : AlgebraicGeometry.openImmersionCoprods f) : AlgebraicGeometry.Flat f

A coproduct of open immersions is flat: flatness is local on the source and the summand inclusions are open immersions.

theorem Hironaka.Sequence.openImmersionCoprods_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : AlgebraicGeometry.openImmersionCoprods f) (hg : AlgebraicGeometry.openImmersionCoprods g) : AlgebraicGeometry.openImmersionCoprods (CategoryTheory.CategoryStruct.comp f g)

A composite of coproducts of open immersions is a coproduct of open immersions: the summands of the source are cut along the summands of the middle scheme.

theorem Hironaka.Sequence.openImmersionCoprods_isSeparated {X Y : AlgebraicGeometry.Scheme} {f : Y ⟶ X} (hf : AlgebraicGeometry.openImmersionCoprods f) : AlgebraicGeometry.IsSeparated f

A coproduct of open immersions f : Y ⟶ X is separated: the diagonal Y → Y ×_X Y is an immersion whose range is closed, its complement being the union of the opens τ₁^{-1}(Uᵢ) ∩ τ₂^{-1}(Uⱼ), i ≠ j, since a point over (Uᵢ, Uᵢ) comes from Uᵢ ×_X Uᵢ ≅ Uᵢ (Uᵢ → X is a monomorphism) and so lies on the diagonal. This is what makes X' → Spec k and X'' → Spec k separated.

No empty centers on the empty scheme means nil

theorem AlgebraicGeometry.Scheme.BlowUpSequence.eq_nil_of_noEmptyCenters {X : Scheme} [IsEmpty ↥X] (S : X.BlowUpSequence) (h : S.NoEmptyCenters) : S = nil X

On the empty scheme every ideal sheaf is ⊤ (two ideal sheaves with equal stalks are equal, vacuously), so a blow-up sequence without empty centers is nil.

The finite local cover and X' = ∐ Uₓᵢ

theorem AlgebraicGeometry.Triple.exists_finite_localCover {k : Type u} [Field k] {GT LT : Triple k → Prop} (D : GlobalizationData openImmersionCoprods GT LT) {T : Triple k} (hT : GT T) : ∃ (σ : Type u) (_ : Finite σ) (Ts : σ → Triple k) (g : (i : σ) → (Ts i).X.left ⟶ T.X.left), (∀ (i : σ), openImmersionCoprods (g i)) ∧ (∀ (i : σ), LT (Ts i)) ∧ (∀ (i : σ), (Ts i).IsPullbackOf T (g i)) ∧ ∀ (x : ↥T.X.left), ∃ (i : σ), x ∈ Set.range ⇑(g i)

Clause (i) of the data of [Kol07, Theorem 105] at every point, and a finite subcover of the quasi-compact T.X.left by the (open) ranges.

theorem AlgebraicGeometry.Triple.exists_isLocalCover {k : Type u} [Field k] {GT LT : Triple k → Prop} [CharZero k] (D : GlobalizationData openImmersionCoprods GT LT) {T : Triple k} (hT : GT T) [Nonempty ↥T.X.left] : ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left), IsLocalCover openImmersionCoprods GT LT T T' g

X' := ∐ᵢ Uₓᵢ with the induced g : X' → X is a local M-cover of a nonempty global triple (the proof of [Kol07, Theorem 105]): the pullback triple along g, in LT by clause (ii) as the disjoint union of the Uₓᵢ with the restricted data.

The kernel pair X'' = X' ×_X X'

theorem AlgebraicGeometry.Triple.exists_kernelPair {k : Type u} [Field k] {GT LT : Triple k → Prop} [CharZero k] (hF : LocalCoversFibreClosed openImmersionCoprods GT LT) {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} (hc : IsLocalCover openImmersionCoprods GT LT T T' g) : ∃ (T'' : Triple k) (τ₁ : T''.X.left ⟶ T'.X.left) (τ₂ : T''.X.left ⟶ T'.X.left), CategoryTheory.IsPullback τ₁ τ₂ g g ∧ T''.IsPullbackOf T' τ₁ ∧ T''.IsPullbackOf T' τ₂ ∧ openImmersionCoprods τ₁ ∧ openImmersionCoprods τ₂ ∧ Function.Surjective ⇑τ₁ ∧ Function.Surjective ⇑τ₂ ∧ LT T''

The kernel pair of a local M-cover as a local triple (the proof of [Kol07, Theorem 105]): X'' = X' ×_X X' with its projections, in M by base change, surjective, with the pullback data of X' along both projections, in LT by the hypothesis LocalCoversFibreClosed.

The classes of Proposition 37 as an instance

theorem AlgebraicGeometry.Triple.globalizationData_isAffineScheme {k : Type u} [Field k] [CharZero k] : GlobalizationData openImmersionCoprods (fun (x : Triple k) => True) IsAffineScheme

The data of [Kol07, Theorem 105] for the classes of [Kol07, Proposition 37] (all triples, and the affine triples): every point of a triple has an affine open neighbourhood, whose triple (the pullback along the open immersion) is affine; the affine triples are closed under finite disjoint unions.

theorem AlgebraicGeometry.Triple.localCoversFibreClosed_isAffineScheme {k : Type u} [Field k] : LocalCoversFibreClosed openImmersionCoprods (fun (x : Triple k) => True) IsAffineScheme

The fibre product over a triple of two affine local covers is affine (as isAffine_coverPair of Hironaka/Resolution/Algebraic/Kol07/Prop37/Prop37Setting.lean): T.X.left is separated over k, so g₂ is an affine morphism, and its base change to the affine T₁.X.left has affine source.

The descent datum (105.4) for whole sequences

theorem Hironaka.OrderSeqAssignment.pullback_eq_of_kernelPair {k : Type u} [Field k] {m : ℕ} {LT : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m LT) (hB : B.CommutesWithSurjectionsIn AlgebraicGeometry.openImmersionCoprods) {T' T'' : AlgebraicGeometry.Triple k} {τ₁ τ₂ : T''.X.left ⟶ T'.X.left} (hM₁ : AlgebraicGeometry.openImmersionCoprods τ₁) (hM₂ : AlgebraicGeometry.openImmersionCoprods τ₂) (hs₁ : Function.Surjective ⇑τ₁) (hs₂ : Function.Surjective ⇑τ₂) (h₁ : T''.IsPullbackOf T' τ₁) (h₂ : T''.IsPullbackOf T' τ₂) (hT' : LT T') (hT'' : LT T'') : (B.seq T' hT').pullback τ₁ = B.seq T'' hT'' ∧ B.seq T'' hT'' = (B.seq T' hT').pullback τ₂

τ₁^* B(X') = B(X'') = τ₂^* B(X') (the compatibility (105.4) in the proof of [Kol07, Theorem 105]), two applications of "B commutes with surjections in M".

Uniqueness of the extension

theorem Hironaka.OrderSeqAssignment.globalization_unique {k : Type u} [Field k] {m : ℕ} {GT LT : AlgebraicGeometry.Triple k → Prop} [CharZero k] (D : AlgebraicGeometry.Triple.GlobalizationData AlgebraicGeometry.openImmersionCoprods GT LT) (hLG : ∀ (T : AlgebraicGeometry.Triple k), LT T → GT T) (B : OrderSeqAssignment k m LT) {B₁ B₂ : OrderSeqAssignment k m GT} (h₁ : ∀ (T : AlgebraicGeometry.Triple k) (hL : LT T) (hG : GT T), B₁.seq T hG = B.seq T hL) (h₂ : ∀ (T : AlgebraicGeometry.Triple k) (hL : LT T) (hG : GT T), B₂.seq T hG = B.seq T hL) (c₁ : B₁.CommutesWithSurjectionsIn AlgebraicGeometry.openImmersionCoprods) (c₂ : B₂.CommutesWithSurjectionsIn AlgebraicGeometry.openImmersionCoprods) : B₁ = B₂

"A unique extension" [Kol07, Theorem 105]: two functors on the global triples agreeing with B on the local ones and commuting with surjections in M are equal. Along a local cover g : X' → X (with X' ∈ GT by hLG) both pull back to B(X'), and pullback along the surjective flat g is injective; on an empty scheme both are nil.