The charts of Lemma 41, shrunk to basic opens

For a smooth h : Y ⟶ X of relative dimension d between schemes with closed immersions embX : X ⟶ AX and embY : Y ⟶ AY into ambients (AY affine), every point y ∈ Y lies in a chart (Chart h embX embY d): an affine open W of Y, given as a scheme with its open immersion e : W ⟶ Y, together with

• the fibre square of [Kol07, Lemma 41] (exists_smooth_ambient_lift'), restricted to W: an affine B smooth of relative dimension d over AX and a closed immersion j : W ⟶ B with IsPullback j (e ≫ h) q embX;
• the square on the side of Y: a global section G of AY with W = embY ⁻¹ᵁ D(G), so that W is the fibre product of Y and the basic open D(G) over AY, IsPullback jY e (D(G)).ι embY.

These are exactly the squares that admissibleEmbedding_sigma (Hironaka.Resolution.Algebraic.Kol07.Thm36.SigmaCharts) takes for the coproduct Z := ∐ Wᵢ of finitely many charts covering Y, on both sides: the ambient ∐ D(Gᵢ) over AY (relative dimension 0) and the ambient ∐ Bᵢ over AX (relative dimension d). This is how "(34.1) is a local property" is used in the proof of [Kol07, Theorem 36] to derive the functoriality of the resolution of an affine scheme under smooth morphisms from that of the principalization sequence (Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineFunctoriality).

The construction

Lemma 41 at y gives an open V ∋ y of Y, an affine AY₁ smooth of some relative dimension d' over an affine open UA of AX, a closed immersion j₁ : V ⟶ AY₁ and the fibre square over UA. Since embY is an embedding, V is the preimage of an open of AY, which contains a basic open D(G) ∋ embY y (isBasis_basicOpen); W := embY ⁻¹ᵁ D(G) = D(g) for g := embY^♯ G is an affine open of Y inside V. On V it is the basic open D(t) of t := g|_V; lifting t along the surjection Γ(AY₁) → Γ(V) of the closed immersion j₁ (Scheme.Hom.app_surjective) to t̃ gives the affine basic open B := D(t̃) ⊆ AY₁ with j₁ ⁻¹ᵁ B = D(t), so W is also an open of V and j := j₁|_W : W ⟶ B is the restriction of a closed immersion. The square over AX is the square of Lemma 41 pasted with the restriction squares of embX to UA and of j₁ to B (isPullback_morphismRestrict, IsPullback.paste_vert); the square over AY is Mathlib's IsOpenImmersion.isPullback on embY ⁻¹ᵁ D(G) = W. Finally d' = d: the map V → X ∩ UA is both the base change of AY₁ → UA (relative dimension d') and a restriction of h (relative dimension d), and V ∋ y is nonempty (SmoothOfRelativeDimension.eq_of_nonempty).

structure Hironaka.Resolution.Chart {X Y AX AY : AlgebraicGeometry.Scheme} (h : Y ⟶ X) (embX : X ⟶ AX) (embY : Y ⟶ AY) (d : ℕ) : Type (u + 1)

A chart of the smooth h : Y ⟶ X over the closed immersions embX, embY (the fibre square of [Kol07, Lemma 41], shrunk to a basic open of Y): an affine open W of Y (a scheme with its open immersion e), a fibre square over embX with an affine B smooth of relative dimension d over AX, and the basic open D(G) of AY cutting W out of Y, with its fibre square over embY.

• W : AlgebraicGeometry.Scheme

  The chart, an affine open of Y.

• e : self.W ⟶ Y

  The open immersion of the chart into Y.

• isOpenImmersion_e : AlgebraicGeometry.IsOpenImmersion self.e
• isAffine_W : AlgebraicGeometry.IsAffine self.W
• B : AlgebraicGeometry.Scheme

  The affine ambient of the chart over AX.

• isAffine_B : AlgebraicGeometry.IsAffine self.B
• q : self.B ⟶ AX

  The smooth map of ambients, of relative dimension d.

• smoothOfRelativeDimension_q : AlgebraicGeometry.SmoothOfRelativeDimension d self.q
• j : self.W ⟶ self.B

  The closed immersion of the chart into its ambient.

• isClosedImmersion_j : AlgebraicGeometry.IsClosedImmersion self.j
• sqX : CategoryTheory.IsPullback self.j (CategoryTheory.CategoryStruct.comp self.e h) self.q embX

  The fibre square of [Kol07, Lemma 41]: W = X ×_{AX} B.

• G : ↑(AY.presheaf.obj (Opposite.op ⊤))

  The global section of AY whose basic open cuts W out of Y.

• jY : self.W ⟶ ↑(AY.basicOpen self.G)

  The closed immersion of the chart into the basic open D(G).

• isClosedImmersion_jY : AlgebraicGeometry.IsClosedImmersion self.jY
• sqY : CategoryTheory.IsPullback self.jY self.e (AY.basicOpen self.G).ι embY

  The Y-side fibre square: W = Y ×_{AY} D(G).

theorem Hironaka.Resolution.exists_chart_mem {X Y AX AY : AlgebraicGeometry.Scheme} (h : Y ⟶ X) (d : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension d h] (embX : X ⟶ AX) [AlgebraicGeometry.IsClosedImmersion embX] (embY : Y ⟶ AY) [AlgebraicGeometry.IsClosedImmersion embY] [AlgebraicGeometry.IsAffine AY] (y : ↥Y) : ∃ (c : Chart h embX embY d), y ∈ Set.range ⇑c.e

Every point of Y lies in a chart ("(34.1) is a local property", [Kol07, Theorem 36, proof], with the fibre square of [Kol07, Lemma 41] shrunk to a basic open); the relative dimension of the chart is that of h by SmoothOfRelativeDimension.eq_of_nonempty.