Kollár's Lemma 41: the local ambient lift of a smooth morphism

exists_smooth_ambient_lift is [Kol07, Lemma 41]: for h : Y ⟶ X smooth, y : Y and a closed immersion emb : X ⟶ A, there are opens UA ∋ emb (h y) of A and V ∋ y of Y, a scheme AY over k, a smooth surjective hA : AY ⟶ UA of constant relative dimension and a closed immersion j : V ⟶ AY with IsPullback j (h.resLE (emb ⁻¹ᵁ UA) V hV) hA (emb.resLE UA (emb ⁻¹ᵁ UA) le_rfl): a smooth morphism to an embedded scheme is, locally, the restriction of a smooth morphism between ambient schemes.

The proof, by the local structure of smooth algebras rather than Kollár's general projection.

1. Affine reduction. An affine UA₀ ∋ emb (h y) (exists_isAffineOpen_mem_and_subset); X₀ := emb ⁻¹ᵁ UA₀ is affine (closed immersions are affine, IsAffineOpen.preimage); an affine V₀ ∋ y inside h ⁻¹ᵁ X₀.
2. The local presentation. Mathlib's Smooth h says that Γ(X, X₀) → Γ(Y, V₀) is a smooth ring map (Smooth.smooth_appLE), hence locally standard smooth (RingHom.smooth_iff_locally_isStandardSmooth): on a basic open V := D(t) ∋ y of V₀ the map Γ(X, X₀) → Γ(Y, V) is standard smooth (exists_basicOpen_isStandardSmooth_appLE), with a submersive presentation P. This replaces Kollár's writing of Y near y as an open of a hypersurface in X × 𝔸^{d+1} after a general projection, which needs an infinite field.
3. The lifted ambient (Hironaka/Algebra/Smooth/StandardSmoothLift.lean). Γ(A, UA₀) ↠ Γ(X, X₀) (Scheme.Hom.app_surjective) lifts the relations of P (Kollár's extension of the coefficients φ_I to Φ_I on the ambient); AY := Spec (T[1/Δ]) is standard smooth of relative dimension P.dimension over Γ(A, UA₀); Spec Γ(Y, V) = Spec Γ(X, X₀) ×_{Spec Γ(A, UA₀)} Spec T (isPullback_SpecMap_of_isPushout) is cut at the open D(Δ) (IsPullback.of_comp_mono_fst) and transported along the isoSpecs to the resLE square (exists_affine_ambient, SpecMap_appLE_isoSpec_inv); j is a closed immersion since T[1/Δ] → Γ(Y, V) is surjective.
4. Shrinking to a surjection. The image of AY → UA₀ ↪ A is open (smooth morphisms are flat and locally of finite presentation, hence universally open); UA is that image, hA the lift of AY → UA₀ to UA (IsOpenImmersion.lift), surjective by construction and still smooth of the same relative dimension (MorphismProperty.IsStableUnderBaseChange along the square IsPullback (𝟙 AY) hA hA₀ (A.homOfLE _)); V ≤ h ⁻¹ᵁ (emb ⁻¹ᵁ UA) since emb ∘ h factors through hA ∘ j on V; the square over UA is the restriction of the square over UA₀ (IsPullback.of_right against the homOfLE square of emb).
5. Over k (exists_smooth_ambient_lift). AY ↘ Spec k := hA ≫ (UA.ι ≫ (A ↘ Spec k)); as an affine scheme over the affine Spec k, AY is quasi-compact and separated over k (isAffineHom_of_isAffine).

The hypotheses [CharZero k], [LocallyOfFiniteType], [h.IsOver], [emb.IsOver] of the main statement are Kollár's setting for Lemma 41 (schemes of finite type over a field of characteristic zero, morphisms over k) and are kept so that the theorem reads as printed; the proof does not need them, because it replaces Kollár's general projection, which needs the field infinite, by Mathlib's local structure of smooth algebras, valid over any base: the field-free form exists_smooth_ambient_lift' is proved first and the main statement is its specialisation. The conclusion adds to Kollár's the quasi-compactness and separatedness of AY over k and the constancy of the relative dimension of hA, all read off his construction; AY is in fact affine, which the statement does not record. Compare [Wlo05, Lemma 4.9.1], the extension of an étale morphism of embedded affine varieties to the ambient spaces. The smooth charts of the functorial resolution use the field-free form (Hironaka/Resolution/Algebraic/Kol07/Thm36/SmoothCharts.lean).

theorem CategoryTheory.IsPullback.of_comp_mono_fst {C : Type u_1} [Category.{u_2, u_1} C] {P X X' Y Z : C} {fst : P ⟶ X} {i : X ⟶ X'} [Mono i] {snd : P ⟶ Y} {f : X' ⟶ Z} {g : Y ⟶ Z} (H : IsPullback (CategoryStruct.comp fst i) snd f g) : IsPullback fst snd (CategoryStruct.comp i f) g

A pullback square whose top map factors through a mono can be cut at the mono: Spec S = Spec R ×_{Spec R'} Spec T and Spec S → Spec T lands in the open D(Δ), so Spec S = Spec R ×_{Spec R'} D(Δ).

theorem AlgebraicGeometry.SpecMap_appLE_isoSpec_inv {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.Hom.appLE f U V e)) hU.isoSpec.inv = CategoryTheory.CategoryStruct.comp hV.isoSpec.inv (Scheme.Hom.resLE f U V e)

Spec.map (f.appLE U V e) ≫ hU.isoSpec.inv = hV.isoSpec.inv ≫ f.resLE U V e for affine opens: the comparison of the affine Spec square with the resLE square.

theorem AlgebraicGeometry.exists_basicOpen_isStandardSmooth_appLE {X Y : Scheme} (h : Y ⟶ X) [Smooth h] {U : X.Opens} (hU : IsAffineOpen U) {V₀ : Y.Opens} (hV₀ : IsAffineOpen V₀) (e : V₀ ≤ (TopologicalSpace.Opens.map h.base).obj U) {y : ↥Y} (hy : y ∈ V₀) : ∃ (t : ↑(Y.presheaf.obj (Opposite.op V₀))), y ∈ Y.basicOpen t ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE h U (Y.basicOpen t) ⋯)).IsStandardSmooth

Given affine U ⊆ X and affine V₀ ⊆ h ⁻¹ᵁ U containing y, there is a basic open D(t) ⊆ V₀ containing y with Γ(X, U) → Γ(Y, D(t)) standard smooth: Mathlib's Smooth h is RingHom.Smooth of every affine appLE, and a smooth ring map is locally standard smooth on the target (the local presentation of Y near y in the proof of [Kol07, Lemma 41]).

theorem AlgebraicGeometry.exists_affine_ambient {X Y A : Scheme} (h : Y ⟶ X) (emb : X ⟶ A) [IsClosedImmersion emb] {UA : A.Opens} (hUA : IsAffineOpen UA) {V : Y.Opens} (hV : IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map h.base).obj ((TopologicalSpace.Opens.map emb.base).obj UA)) (hstd : (CommRingCat.Hom.hom (Scheme.Hom.appLE h ((TopologicalSpace.Opens.map emb.base).obj UA) V e)).IsStandardSmooth) : ∃ (AY : Scheme) (_ : IsAffine AY) (hA : AY ⟶ ↑UA) (_ : Smooth hA) (_ : ∃ (d : ℕ), SmoothOfRelativeDimension d hA) (j : ↑V ⟶ AY) (_ : IsClosedImmersion j), CategoryTheory.IsPullback j (Scheme.Hom.resLE h ((TopologicalSpace.Opens.map emb.base).obj UA) V e) hA (Scheme.Hom.resLE emb UA ((TopologicalSpace.Opens.map emb.base).obj UA) ⋯)

The affine chart of [Kol07, Lemma 41]: over an affine UA ⊆ A with Γ(X, emb ⁻¹ᵁ UA) → Γ(Y, V) standard smooth, the lifted presentation gives an affine AY = Spec (T[1/Δ]), smooth of relative dimension P.dimension over UA, and a closed immersion V ↪ AY making V the fibre product emb ⁻¹ᵁ UA ×_{UA} AY.

theorem AlgebraicGeometry.exists_smooth_ambient_lift' {X Y A : Scheme} (h : Y ⟶ X) [Smooth h] (y : ↥Y) (emb : X ⟶ A) [IsClosedImmersion emb] : ∃ (UA : A.Opens) (V : Y.Opens) (_ : y ∈ V) (hV : V ≤ (TopologicalSpace.Opens.map h.base).obj ((TopologicalSpace.Opens.map emb.base).obj UA)) (AY : Scheme) (_ : IsAffine AY) (hA : AY ⟶ ↑UA) (_ : Smooth hA) (_ : ∃ (d : ℕ), SmoothOfRelativeDimension d hA) (_ : Function.Surjective ⇑hA) (j : ↑V ⟶ AY) (_ : IsClosedImmersion j), CategoryTheory.IsPullback j (Scheme.Hom.resLE h ((TopologicalSpace.Opens.map emb.base).obj UA) V hV) hA (Scheme.Hom.resLE emb UA ((TopologicalSpace.Opens.map emb.base).obj UA) ⋯)

[Kol07, Lemma 41] without the base field: the affine chart shrunk to the (open) image of AY → UA, so that hA is surjective; AY is affine.

theorem AlgebraicGeometry.exists_smooth_ambient_lift {k : Type u} [Field k] (X Y : Scheme) (h : Y ⟶ X) [Smooth h] (y : ↥Y) (A : Scheme) [A.Over (Spec ↧k)] (emb : X ⟶ A) [IsClosedImmersion emb] : ∃ (UA : A.Opens) (V : Y.Opens) (_ : y ∈ V) (hV : V ≤ (TopologicalSpace.Opens.map h.base).obj ((TopologicalSpace.Opens.map emb.base).obj UA)) (AY : Scheme) (x : AY.Over (Spec ↧k)) (_ : QuasiCompact (AY ↘ Spec ↧k)) (_ : IsSeparated (AY ↘ Spec ↧k)) (hA : AY ⟶ ↑UA) (_ : Smooth hA) (_ : ∃ (d : ℕ), SmoothOfRelativeDimension d hA) (_ : Function.Surjective ⇑hA) (j : ↑V ⟶ AY) (_ : IsClosedImmersion j), CategoryTheory.CategoryStruct.comp hA (CategoryTheory.CategoryStruct.comp UA.ι (A ↘ Spec ↧k)) = AY ↘ Spec ↧k ∧ CategoryTheory.IsPullback j (Scheme.Hom.resLE h ((TopologicalSpace.Opens.map emb.base).obj UA) V hV) hA (Scheme.Hom.resLE emb UA ((TopologicalSpace.Opens.map emb.base).obj UA) ⋯)

[Kol07, Lemma 41], over the base field k: for h : Y ⟶ X smooth, y : Y and a closed immersion emb : X ⟶ A of schemes over k, opens UA ∋ emb (h y), V ∋ y, a scheme AY over k (through hA and UA; quasi-compact and separated over k as an affine scheme over the affine Spec k), a smooth surjective hA : AY ⟶ UA of constant relative dimension and a closed immersion j : V ⟶ AY making V the fibre product of emb ⁻¹ᵁ UA and AY over UA.