The surjective completion of an étale pair

The functoriality package [Kol07, 34.1] gives the commutation of a blow-up sequence functor with smooth surjections outright (its first bullet; for the principalization functor this is clause (4) of [Kol07, Theorem 35]), and with a general smooth morphism only up to the deletion of empty blow-ups (the second bullet). To use the first bullet alone, an étale pair ψ, ψ' : W ⟶ A over k with I.comap ψ = I.comap ψ' is completed to a surjective étale pair hψ, hψ' : Y ⟶ A by adding the pieces of the finite affine cover of A (Triple.affineCover), Y := W ⨿ ∐ᵢ Uᵢ. Y is affine (a finite coproduct of affine schemes), hence separated and quasi-compact over k, smooth of the relative dimension of A (locality on the source), and the triple T_Y := Triple.pullback TA _ hψ carries the pullback data of TA along both hψ and hψ': the ideals agree on every piece of the coproduct (eq_of_comap_eq_of_covers), the boundary is empty, and the structure maps agree (Sigma.hom_ext). So BP T_Y = (BP TA).pullback hψ = (BP TA).pullback hψ': one sequence, two readings, with the same indices, and a truncation can then be taken on the base sequence. This is the device by which the resolution functor is shown to be an isomorphism over the smooth locus; it is in the spirit of the passage from affine schemes to all schemes in [Kol07, Proposition 37].

• completionScheme W TA: ∐ (Option TA.affineCover.I₀) with W at none.
• completionDesc ψ: Sigma.desc of ψ and the cover maps; étale for étale ψ (IsZariskiLocalAtSource.sigmaDesc), surjective (the cover), and the structure maps of two such completions agree when ψ ≫ str = ψ' ≫ str.
• exists_completion_isPullbackOf: the completion triple and the two pullback-data facts, with a point y over q for both maps.

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.completionFamily {k : Type u} [Field k] (W : AlgebraicGeometry.Scheme) (TA : AlgebraicGeometry.Triple k) : Option TA.affineCover.I₀ → AlgebraicGeometry.Scheme

The family of schemes of the completion: W at none, the pieces of the finite affine cover of TA.X.left at some i.

Equations

• Hironaka.Sequence.completionFamily W TA none = W
• Hironaka.Sequence.completionFamily W TA (some i) = TA.affineCover.X i

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.completionHom {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) (o : Option TA.affineCover.I₀) : completionFamily W TA o ⟶ TA.X.left

The components of the completion map: ψ on W, the cover maps on the pieces.

Equations

• Hironaka.Sequence.completionHom ψ none = ψ
• Hironaka.Sequence.completionHom ψ (some i) = TA.affineCover.f i

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.completionScheme {k : Type u} [Field k] (W : AlgebraicGeometry.Scheme) (TA : AlgebraicGeometry.Triple k) : AlgebraicGeometry.Scheme

The completion scheme Y := W ⨿ ∐ᵢ Uᵢ.

Equations

• Hironaka.Sequence.completionScheme W TA = ∐ Hironaka.Sequence.completionFamily W TA

noncomputable def Hironaka.Sequence.completionDesc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) : completionScheme W TA ⟶ TA.X.left

The map of the completion: ψ on W, the cover maps on the pieces.

Equations

• Hironaka.Sequence.completionDesc ψ = CategoryTheory.Limits.Sigma.desc (Hironaka.Sequence.completionHom ψ)

theorem Hironaka.Sequence.ι_none_comp_completionDesc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (completionFamily W TA) none) (completionDesc ψ) = ψ

theorem Hironaka.Sequence.ι_none_comp_completionDesc_assoc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) {Z : AlgebraicGeometry.Scheme} (h : TA.X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (completionFamily W TA) none) (CategoryTheory.CategoryStruct.comp (completionDesc ψ) h) = CategoryTheory.CategoryStruct.comp ψ h

theorem Hironaka.Sequence.ι_some_comp_completionDesc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) (i : TA.affineCover.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (completionFamily W TA) (some i)) (completionDesc ψ) = TA.affineCover.f i

theorem Hironaka.Sequence.ι_some_comp_completionDesc_assoc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) (i : TA.affineCover.I₀) {Z : AlgebraicGeometry.Scheme} (h : TA.X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (completionFamily W TA) (some i)) (CategoryTheory.CategoryStruct.comp (completionDesc ψ) h) = CategoryTheory.CategoryStruct.comp (TA.affineCover.f i) h

instance Hironaka.Sequence.isAffine_completionFamily {k : Type u} [Field k] (W : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine W] (TA : AlgebraicGeometry.Triple k) (o : Option TA.affineCover.I₀) : AlgebraicGeometry.IsAffine (completionFamily W TA o)

instance Hironaka.Sequence.isAffine_completionScheme {k : Type u} [Field k] (W : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine W] (TA : AlgebraicGeometry.Triple k) : AlgebraicGeometry.IsAffine (completionScheme W TA)

theorem Hironaka.Sequence.etale_completionDesc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) [AlgebraicGeometry.Etale ψ] : AlgebraicGeometry.Etale (completionDesc ψ)

The completion of an étale map is étale (locality on the source; the cover maps are open immersions).

theorem Hironaka.Sequence.surjective_completionDesc {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) : Function.Surjective ⇑(completionDesc ψ)

The completion is surjective: the cover pieces already cover TA.X.left.

theorem Hironaka.Sequence.completionDesc_comp_over {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ ψ' : W ⟶ TA.X.left) (h : CategoryTheory.CategoryStruct.comp ψ (TA.X.left ↘ AlgebraicGeometry.Spec ↧k) = CategoryTheory.CategoryStruct.comp ψ' (TA.X.left ↘ AlgebraicGeometry.Spec ↧k)) : CategoryTheory.CategoryStruct.comp (completionDesc ψ) (TA.X.left ↘ AlgebraicGeometry.Spec ↧k) = CategoryTheory.CategoryStruct.comp (completionDesc ψ') (TA.X.left ↘ AlgebraicGeometry.Spec ↧k)

Two completions have the same composite with the structure map when the two étale maps do.

theorem Hironaka.Sequence.comap_completionDesc_eq {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ ψ' : W ⟶ TA.X.left) (I : TA.X.left.IdealSheafData) (h : I.comap ψ = I.comap ψ') : I.comap (completionDesc ψ) = I.comap (completionDesc ψ')

Two completions pull an ideal sheaf back to the same ideal sheaf when the two étale maps do (extensionality of ideal sheaves along the open cover by the pieces).

theorem AlgebraicGeometry.Scheme.DivisorFamily.comap_eq_comap_of_isEmpty {X Y : Scheme} (E : X.DivisorFamily) (h h' : Y ⟶ X) (hE : IsEmpty E.ι) : E.comap h = E.comap h'

The inverse images of a divisor family with an empty index type along two morphisms agree.

The completion triple

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.completionOver {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) : (completionScheme W TA).Over (AlgebraicGeometry.Spec ↧k)

The completion scheme is a scheme over Spec k through the completion of ψ.

Equations

• Hironaka.Sequence.completionOver ψ = { hom := CategoryTheory.CategoryStruct.comp (Hironaka.Sequence.completionDesc ψ) (TA.X.left ↘ AlgebraicGeometry.Spec ↧k) }

theorem Hironaka.Sequence.exists_smoothOfRelativeDimension_completion {k : Type u} [Field k] {W : AlgebraicGeometry.Scheme} {TA : AlgebraicGeometry.Triple k} (ψ : W ⟶ TA.X.left) [AlgebraicGeometry.Etale ψ] : ∃ (n : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension n (completionScheme W TA ↘ AlgebraicGeometry.Spec ↧k)

The completion scheme is smooth of the relative dimension of TA.X.left over k, when ψ is étale (each piece is étale over TA.X.left; locality on the source).

theorem Hironaka.Sequence.exists_completion_isPullbackOf {k : Type u} [Field k] [CharZero k] {W : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine W] {TA : AlgebraicGeometry.Triple k} (ψ ψ' : W ⟶ TA.X.left) [AlgebraicGeometry.Etale ψ] [AlgebraicGeometry.Etale ψ'] (hover : CategoryTheory.CategoryStruct.comp ψ (TA.X.left ↘ AlgebraicGeometry.Spec ↧k) = CategoryTheory.CategoryStruct.comp ψ' (TA.X.left ↘ AlgebraicGeometry.Spec ↧k)) (hI : TA.I.comap ψ = TA.I.comap ψ') (hE : IsEmpty TA.E.ι) : ∃ (T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ TA.X.left) (g' : T'.X.left ⟶ TA.X.left), AlgebraicGeometry.Etale g ∧ AlgebraicGeometry.Etale g' ∧ Function.Surjective ⇑g ∧ Function.Surjective ⇑g' ∧ T'.IsPullbackOf TA g ∧ T'.IsPullbackOf TA g' ∧ ∀ (q : ↥W), ∃ (y : ↥T'.X.left), g y = ψ q ∧ g' y = ψ' q

The surjective completion of an étale pair, which makes the first bullet of [Kol07, 34.1] (commutation with smooth surjections) applicable. For étale ψ, ψ' : W ⟶ TA.X.left with the same composite to Spec k and the same inverse image of TA.I, and TA.E empty, there are a triple T' and surjective étale maps g, g' : T'.X.left ⟶ TA.X.left along both of which T' carries the pullback data of TA, and every q : W has a point y : T'.X.left with g y = ψ q, g' y = ψ' q.