The setting of Proposition 37: the affine cover of a triple 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 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 X'' = X' ×_X X'. The definitions Triple.affineCover, coverScheme, coverDesc, coverPair, coverFst, coverSnd and the affine class Triple.IsAffineScheme are in Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean; this module proves the elementary facts about them and defines the triples coverTriple and coverPairTriple of X' and X''.

• X' is affine (isAffine_coverScheme): a finite coproduct of affine schemes (Mathlib's instance), the pieces being members of Mathlib's affine cover and the index type the finite subcover's.
• g is a smooth surjection (smooth_coverDesc, surjective_coverDesc): smoothness is local on the source and each piece Uᵢ → X is an open immersion (IsZariskiLocalAtSource.sigmaDesc); the pieces cover X (Cover.iUnion_range).
• X' is a triple's scheme (locallyOfFiniteType_coverScheme, quasiCompact_coverScheme, isSeparated_coverScheme, exists_smoothOfRelativeDimension_coverScheme): X' → Spec k factors as g ≫ (X → Spec k); finite type by composition, quasi-compact and separated because X' is affine over the affine base, and smooth of the relative dimension n of X because each piece is an open subscheme of X (relative dimension 0 + n, locality on the source again).
• X'' is affine (isAffine_coverPair): X' → X → Spec k is an affine morphism and X → Spec k is separated (a triple's ambient scheme is separated over k), so g is an affine morphism (IsAffineHom.of_comp) and the fibre product of g with itself is affine. Kollár's X'' is the disjoint union of the Uᵢ ∩ Uⱼ; that an intersection of two affine opens is affine uses the separatedness of X, a point left implicit in his text.
• τ₁, τ₂ are smooth surjections (smooth_coverFst, …): base change of g; surjectivity from the image of a pullback projection (range_fst_of_isPullback).
• The triples (coverTriple, coverPairTriple): the pullback triple Triple.pullback along g, resp. along τ₁, with the pullback data along τ₂ as well (coverPairTriple_isPullbackOf_snd: τ₁ ≫ g = τ₂ ≫ g and comap_comp); the existence statements package them without the constructions.

theorem Hironaka.MarkedTriple.closedUnderSigma_isAffineScheme {k : Type u} [Field k] : ClosedUnderSigma IsAffineScheme

The affine marked triples are closed under finite disjoint unions ([Kol07, Warning 38] for the domain of Proposition 37): closedUnderSigma_of_triple applied to closedUnderSigma_isAffine (the class is fun T => IsAffine T.X.left by definition).

instance AlgebraicGeometry.Triple.finite_affineCover_I₀ {k : Type u} [Field k] (T : Triple k) : Finite T.affineCover.I₀

The finite subcover has a finite index type.

instance AlgebraicGeometry.Triple.isAffine_affineCover_X {k : Type u} [Field k] (T : Triple k) (i : T.affineCover.I₀) : IsAffine (T.affineCover.X i)

The members of the finite affine cover are affine.

theorem AlgebraicGeometry.Triple.isAffine_coverScheme {k : Type u} [Field k] (T : Triple k) : IsAffine T.coverScheme

X' is affine (the proof of [Kol07, Proposition 37]).

instance AlgebraicGeometry.Triple.instIsAffineCoverScheme {k : Type u} [Field k] (T : Triple k) : IsAffine T.coverScheme

theorem AlgebraicGeometry.Triple.ι_comp_coverDesc {k : Type u} [Field k] (T : Triple k) (i : T.affineCover.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : T.affineCover.I₀) => T.affineCover.X i) i) T.coverDesc = T.affineCover.f i

The piece inclusions: Sigma.ι i ≫ g is the member Uᵢ → X of the cover.

theorem AlgebraicGeometry.Triple.ι_comp_coverDesc_assoc {k : Type u} [Field k] (T : Triple k) (i : T.affineCover.I₀) {Z : Scheme} (h : T.X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (i : T.affineCover.I₀) => T.affineCover.X i) i) (CategoryTheory.CategoryStruct.comp T.coverDesc h) = CategoryTheory.CategoryStruct.comp (T.affineCover.f i) h

The piece inclusions: Sigma.ι i ≫ g is the member Uᵢ → X of the cover.

theorem AlgebraicGeometry.Triple.smooth_coverDesc {k : Type u} [Field k] (T : Triple k) : Smooth T.coverDesc

g is smooth: locality on the source (IsZariskiLocalAtSource.sigmaDesc; the unifier option is Mathlib's own idiom for this lemma, cf. Flat (Sigma.desc f) in Morphisms/Flat.lean).

instance AlgebraicGeometry.Triple.instSmoothCoverDesc {k : Type u} [Field k] (T : Triple k) : Smooth T.coverDesc

theorem AlgebraicGeometry.Triple.smoothOfRelativeDimension_zero_coverDesc {k : Type u} [Field k] (T : Triple k) : SmoothOfRelativeDimension 0 T.coverDesc

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

theorem AlgebraicGeometry.Triple.surjective_coverDesc {k : Type u} [Field k] (T : Triple k) : Function.Surjective ⇑T.coverDesc

g is surjective.

theorem AlgebraicGeometry.Triple.locallyOfFiniteType_coverScheme {k : Type u} [Field k] (T : Triple k) : LocallyOfFiniteType (T.coverScheme ↘ Spec ↧k)

X' is locally of finite type over Spec k.

instance AlgebraicGeometry.Triple.instLocallyOfFiniteTypeOverSchemeCoverSchemeSpecOfInferInstanceOverClass {k : Type u} [Field k] (T : Triple k) : LocallyOfFiniteType (T.coverScheme ↘ Spec ↧k)

theorem AlgebraicGeometry.Triple.quasiCompact_coverScheme {k : Type u} [Field k] (T : Triple k) : QuasiCompact (T.coverScheme ↘ Spec ↧k)

X' is quasi-compact over Spec k.

theorem AlgebraicGeometry.Triple.isSeparated_coverScheme {k : Type u} [Field k] (T : Triple k) : IsSeparated (T.coverScheme ↘ Spec ↧k)

X' is separated over Spec k.

instance AlgebraicGeometry.Triple.instIsSeparatedOverSchemeCoverSchemeSpecOfInferInstanceOverClass {k : Type u} [Field k] (T : Triple k) : IsSeparated (T.coverScheme ↘ Spec ↧k)

theorem AlgebraicGeometry.Triple.coverDesc_comp {k : Type u} [Field k] (T : Triple k) : CategoryTheory.CategoryStruct.comp T.coverDesc (T.X.left ↘ Spec ↧k) = CategoryTheory.Limits.Sigma.desc fun (i : T.affineCover.I₀) => CategoryTheory.CategoryStruct.comp (T.affineCover.f i) (T.X.left ↘ Spec ↧k)

g ≫ (X → Spec k) as a coproduct morphism.

theorem AlgebraicGeometry.Triple.exists_smoothOfRelativeDimension_coverScheme {k : Type u} [Field k] (T : Triple k) : ∃ (n : ℕ), SmoothOfRelativeDimension n (T.coverScheme ↘ Spec ↧k)

X' is smooth over k of the relative dimension of X (the equidimensionality required of a triple, [Kol07, Notation 64]).

noncomputable def AlgebraicGeometry.Triple.coverTriple {k : Type u} [Field k] (T : Triple k) [PerfectField k] : Triple k

The triple (X', g^* I, g^{-1} E) of the proof of [Kol07, Proposition 37]: the pullback of T along g.

Equations

• T.coverTriple = T.pullback ⋯ T.coverDesc

theorem AlgebraicGeometry.Triple.coverTriple_X {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverTriple.X.left = T.coverScheme

theorem AlgebraicGeometry.Triple.coverTriple_I {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverTriple.I = T.I.comap T.coverDesc

theorem AlgebraicGeometry.Triple.coverTriple_E {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverTriple.E = T.E.comap T.coverDesc

theorem AlgebraicGeometry.Triple.isAffine_coverTriple {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverTriple.IsAffineScheme

The triple of X' is affine.

theorem AlgebraicGeometry.Triple.coverTriple_isPullbackOf {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverTriple.IsPullbackOf T T.coverDesc

The triple of X' carries the pullback data of T along g.

theorem AlgebraicGeometry.Triple.exists_isAffine_isPullbackOf {k : Type u} [Field k] (T : Triple k) [PerfectField k] : ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left), T'.IsAffineScheme ∧ Smooth g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g

The setting of the proof of [Kol07, Proposition 37], without the construction: an affine triple with a smooth surjection to T.X.left carrying the pullback data.

theorem AlgebraicGeometry.Triple.isAffine_coverPair {k : Type u} [Field k] (T : Triple k) : IsAffine T.coverPair

X'' is affine (g is an affine morphism since X → Spec k is separated).

instance AlgebraicGeometry.Triple.instIsAffineCoverPair {k : Type u} [Field k] (T : Triple k) : IsAffine T.coverPair

theorem AlgebraicGeometry.Triple.smooth_coverFst {k : Type u} [Field k] (T : Triple k) : Smooth T.coverFst

τ₁ is smooth (base change of g).

theorem AlgebraicGeometry.Triple.smooth_coverSnd {k : Type u} [Field k] (T : Triple k) : Smooth T.coverSnd

τ₂ is smooth (base change of g).

instance AlgebraicGeometry.Triple.instSmoothCoverFst {k : Type u} [Field k] (T : Triple k) : Smooth T.coverFst

instance AlgebraicGeometry.Triple.instSmoothCoverSnd {k : Type u} [Field k] (T : Triple k) : Smooth T.coverSnd

theorem AlgebraicGeometry.Triple.smoothOfRelativeDimension_zero_coverFst {k : Type u} [Field k] (T : Triple k) : SmoothOfRelativeDimension 0 T.coverFst

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

theorem AlgebraicGeometry.Triple.surjective_coverFst {k : Type u} [Field k] (T : Triple k) : Function.Surjective ⇑T.coverFst

τ₁ is surjective.

theorem AlgebraicGeometry.Triple.surjective_coverSnd {k : Type u} [Field k] (T : Triple k) : Function.Surjective ⇑T.coverSnd

τ₂ is surjective.

theorem AlgebraicGeometry.Triple.coverFst_comp_coverDesc {k : Type u} [Field k] (T : Triple k) : CategoryTheory.CategoryStruct.comp T.coverFst T.coverDesc = CategoryTheory.CategoryStruct.comp T.coverSnd T.coverDesc

τ₁ ≫ g = τ₂ ≫ g.

instance AlgebraicGeometry.Triple.instLocallyOfFiniteTypeOverSchemeCoverPairSpecOfInferInstanceOverClass {k : Type u} [Field k] (T : Triple k) : LocallyOfFiniteType (T.coverPair ↘ Spec ↧k)

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

instance AlgebraicGeometry.Triple.instIsSeparatedOverSchemeCoverPairSpecOfInferInstanceOverClass {k : Type u} [Field k] (T : Triple k) : IsSeparated (T.coverPair ↘ Spec ↧k)

theorem AlgebraicGeometry.Triple.exists_smoothOfRelativeDimension_coverPair {k : Type u} [Field k] (T : Triple k) : ∃ (n : ℕ), SmoothOfRelativeDimension n (T.coverPair ↘ Spec ↧k)

X'' is smooth over k of the relative dimension of X.

noncomputable def AlgebraicGeometry.Triple.coverPairTriple {k : Type u} [Field k] (T : Triple k) [PerfectField k] : Triple k

The triple (X'', (g τ₁)^* I, (g τ₁)^{-1} E) of the kernel pair: the pullback of the triple of X' along τ₁.

Equations

• T.coverPairTriple = T.coverTriple.pullback ⋯ T.coverFst

theorem AlgebraicGeometry.Triple.coverPairTriple_X {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverPairTriple.X.left = T.coverPair

theorem AlgebraicGeometry.Triple.isAffine_coverPairTriple {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverPairTriple.IsAffineScheme

The triple of X'' is affine.

theorem AlgebraicGeometry.Triple.coverPairTriple_isPullbackOf_fst {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverPairTriple.IsPullbackOf T.coverTriple T.coverFst

The triple of X'' carries the pullback data of the triple of X' along τ₁.

theorem AlgebraicGeometry.Triple.coverPairTriple_isPullbackOf_snd {k : Type u} [Field k] (T : Triple k) [PerfectField k] : T.coverPairTriple.IsPullbackOf T.coverTriple T.coverSnd

The triple of X'' carries the pullback data of the triple of X' along τ₂ as well: (g τ₁)^* I = (g τ₂)^* I.

theorem AlgebraicGeometry.Triple.exists_prop37Setting {k : Type u} [Field k] (T : Triple k) [PerfectField k] : ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left) (T'' : Triple k) (τ₁ : T''.X.left ⟶ T'.X.left) (τ₂ : T''.X.left ⟶ T'.X.left), T'.IsAffineScheme ∧ Smooth g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g ∧ T''.IsAffineScheme ∧ CategoryTheory.IsPullback τ₁ τ₂ g g ∧ Smooth τ₁ ∧ Smooth τ₂ ∧ Function.Surjective ⇑τ₁ ∧ Function.Surjective ⇑τ₂ ∧ T''.IsPullbackOf T' τ₁ ∧ T''.IsPullbackOf T' τ₂

The setting of the proof of [Kol07, Proposition 37], without the constructions: the affine cover triple, the kernel pair triple, and their maps with their properties.

noncomputable def Hironaka.MarkedTriple.coverTriple {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : MarkedTriple k

The marked triple of X'.

Equations

• T.coverTriple = T.pullback ⋯ T.coverDesc

theorem Hironaka.MarkedTriple.coverTriple_toTriple {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : T.coverTriple.toTriple = T.coverTriple

theorem Hironaka.MarkedTriple.isAffine_coverTriple {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : T.coverTriple.IsAffineScheme

The marked triple of X' is affine.

theorem Hironaka.MarkedTriple.coverTriple_isPullbackOf {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : T.coverTriple.IsPullbackOf T T.coverDesc

The marked triple of X' carries the pullback data of T along g.

theorem Hironaka.MarkedTriple.exists_isAffine_isPullbackOf {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : ∃ (T' : MarkedTriple k) (g : T'.X.left ⟶ T.X.left), T'.IsAffineScheme ∧ AlgebraicGeometry.Smooth g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g

The setting of the proof of [Kol07, Proposition 37] for marked triples, without the construction.

noncomputable def Hironaka.MarkedTriple.coverPairTriple {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : MarkedTriple k

The marked triple of X''.

Equations

• T.coverPairTriple = T.coverTriple.pullback ⋯ T.coverFst

theorem Hironaka.MarkedTriple.coverPairTriple_isPullbackOf_fst {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : T.coverPairTriple.IsPullbackOf T.coverTriple T.coverFst

The marked triple of X'' carries the pullback data of the marked triple of X' along τ₁.

theorem Hironaka.MarkedTriple.coverPairTriple_isPullbackOf_snd {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : T.coverPairTriple.IsPullbackOf T.coverTriple T.coverSnd

… and along τ₂.

theorem Hironaka.MarkedTriple.exists_prop37Setting {k : Type u} [Field k] (T : MarkedTriple k) [PerfectField k] : ∃ (T' : MarkedTriple k) (g : T'.X.left ⟶ T.X.left) (T'' : MarkedTriple k) (τ₁ : T''.X.left ⟶ T'.X.left) (τ₂ : T''.X.left ⟶ T'.X.left), T'.IsAffineScheme ∧ AlgebraicGeometry.Smooth g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g ∧ T''.IsAffineScheme ∧ CategoryTheory.IsPullback τ₁ τ₂ g g ∧ AlgebraicGeometry.Smooth τ₁ ∧ AlgebraicGeometry.Smooth τ₂ ∧ Function.Surjective ⇑τ₁ ∧ Function.Surjective ⇑τ₂ ∧ T''.IsPullbackOf T' τ₁ ∧ T''.IsPullbackOf T' τ₂

The setting of the proof of [Kol07, Proposition 37] for marked triples, without the constructions.