The local blow-up at an arbitrary point of a chart

[Kol07, Definition 60] and [Hau14, Definitions 4.15–4.16]: for a point x' of B_Z X over x lying in the chart of the coordinate y_ρ — the exceptional ideal at x' is generated by π^* y_ρ — with y a regular system of parameters at x adapted to Z (I_x = (y_0, …, y_{r-1}), ρ = r − 1), the stalk 𝒪_{B,x'} is the localization of the chart ring R' = 𝒪_{X,x}[I_x/y_ρ] = chartRing y ρ at a prime 𝔮 over 𝔪_x, compatibly with π^* (exists_stalk_equiv_localization_atPrime). Hironaka.Scheme.Smooth.LocalBlowUp proves this at the origin of the chart (exists_stalk_equiv_localization_chartOrigin_of_isIso); the same assembly works at every point once the point is located in the chart:

• the blow-up of Spec 𝒪_{X,x} along I_x is the base change of B_Z X along Spec 𝒪_{X,x} → X (exists_isPullback_fromSpecStalk), so x' — which lies over x, the image of the closed point — lifts to a point t of the local blow-up (Mathlib's exists_preimage_of_isPullback), and the stalks agree (isIso_stalkMap_of_isPullback_fromSpecStalk);
• the exceptional ideal of the local blow-up is the pullback of the exceptional ideal of B_Z X, so at t it is generated by the image of y_ρ, and t lies in the chart of y_ρ by the chart membership criterion (affineBlowUp.mem_chart_iff): t = chart_{y_ρ}(q) for a prime q of 𝒪_{X,x}[I_x/y_ρ], and that algebra is chartRing y ρ (affineBlowUpAlgebra_stalkIdeal_eq_chartRing);
• the stalk of the affine blow-up at chart_{y_ρ}(q) is the localization at q (exists_ringEquiv_stalk_chart), compatibly with germs; q lies over 𝔪_x because t lies over the closed point (chart_π).

This is the chart model of a point that Hironaka.Scheme.Snc.InducedCoordinates and Hironaka.Scheme.Snc.ChartOrigin read Hauser's (6)–(9) in.

Sources: [Kol07, Definition 60]; [Hau14, Definition 4.13; Definitions 4.15–4.16]; [TSPA, Tag 0BFL].

theorem AlgebraicGeometry.stalkIdeal_exceptionalIdeal_eq_map_of_isPullback {X : Scheme} (Z : X.IdealSheafData) (x : ↥X) {φ : affineBlowUp (Z.stalkIdeal x) ⟶ Z.blowUp} (H : CategoryTheory.IsPullback φ (affineBlowUp.π (Z.stalkIdeal x)) Z.blowUpπ (X.fromSpecStalk x)) (t : ↥(affineBlowUp (Z.stalkIdeal x))) : (affineBlowUp.exceptionalIdeal (Z.stalkIdeal x)).stalkIdeal t = Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap φ t)) ((Z.comap Z.blowUpπ).stalkIdeal (φ t))

The stalk of the exceptional ideal of the local blow-up at a point t over x', as the image of the stalk of the exceptional ideal of B_Z X at x' under the (iso) stalk map of the base change.

theorem AlgebraicGeometry.stalkMap_stalkMap_germ_eq {X Y B : Scheme} {x : ↥X} (φ : Y ⟶ B) (ψ : Y ⟶ Spec (X.presheaf.stalk x)) (π : B ⟶ X) (hw : CategoryTheory.CategoryStruct.comp φ π = CategoryTheory.CategoryStruct.comp ψ (X.fromSpecStalk x)) (T : ↥Y) (hx' : π (φ T) = x) (V : X.Opens) (hxV : x ∈ V) (s : ↑(X.presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap φ T)) ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π (φ T))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V (π (φ T)) ⋯)) s)) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap ψ T)) ((CategoryTheory.ConcreteCategory.hom ((Spec (X.presheaf.stalk x)).presheaf.germ ⊤ (ψ T) trivial)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso (X.presheaf.stalk x)).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V x hxV)) s)))

Along a base change of Spec 𝒪_{X,x} → X: φ^♯ sends π^* of a germ at π(φ T) = x to ψ^♯ of the germ of the "constant" (stalkMap_germ_eq_of_eq_comp_fromSpecStalk, with the point of the germ rewritten to π (φ T)).

theorem AlgebraicGeometry.map_stalkIdeal_eq_span_of_eq_span {X Y B : Scheme} {x : ↥X} (φ : Y ⟶ B) (ψ : Y ⟶ Spec (X.presheaf.stalk x)) (π : B ⟶ X) (hw : CategoryTheory.CategoryStruct.comp φ π = CategoryTheory.CategoryStruct.comp ψ (X.fromSpecStalk x)) (T : ↥Y) (hx' : π (φ T) = x) (Z : X.IdealSheafData) (V : X.Opens) (hxV : x ∈ V) (s : ↑(X.presheaf.obj (Opposite.op V))) (hF : (Z.comap π).stalkIdeal (φ T) = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π (φ T))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V (π (φ T)) ⋯)) s)}) : Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap φ T)) ((Z.comap π).stalkIdeal (φ T)) = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap ψ T)) ((CategoryTheory.ConcreteCategory.hom ((Spec (X.presheaf.stalk x)).presheaf.germ ⊤ (ψ T) trivial)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso (X.presheaf.stalk x)).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V x hxV)) s)))}

The image under φ^♯ of a principal stalk ideal generated by π^* of a germ.

theorem AlgebraicGeometry.ringEquiv_trans_stalkMap_eq {X Y B : Scheme} {x : ↥X} (φ : Y ⟶ B) (ψ : Y ⟶ Spec (X.presheaf.stalk x)) (π : B ⟶ X) (hw : CategoryTheory.CategoryStruct.comp φ π = CategoryTheory.CategoryStruct.comp ψ (X.fromSpecStalk x)) (T : ↥Y) (hx' : π (φ T) = x) [CategoryTheory.IsIso (Scheme.Hom.stalkMap φ T)] {L : Type u} [CommRing L] (e₁ : ↑(Y.presheaf.stalk T) ≃+* L) (g : ↑(X.presheaf.stalk x) →+* L) (h4 : ∀ (V : X.Opens) (hxV : x ∈ V) (s : ↑(X.presheaf.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap ψ T)) ((CategoryTheory.ConcreteCategory.hom ((Spec (X.presheaf.stalk x)).presheaf.germ ⊤ (ψ T) trivial)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso (X.presheaf.stalk x)).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V x hxV)) s))) = e₁.symm (g ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V x hxV)) s))) (c : ↑(X.presheaf.stalk (π (φ T)))) : ((RingEquiv.ofBijective (CommRingCat.Hom.hom (Scheme.Hom.stalkMap φ T)) ⋯).trans e₁) ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap π (φ T))) c) = g (hx' ▸ c)

The stalk isomorphism of a base change of Spec 𝒪_{X,x} → X, composed with an isomorphism e₁ of the stalk of Y with a ring L under which the germs of constants go to g, sends π^* to g.

theorem AlgebraicGeometry.exists_chart_point_of_isPullback {X : Scheme} (Z : X.IdealSheafData) (x : ↥X) (x' : ↥Z.blowUp) (hx' : Z.blowUpπ x' = x) {b : ↑(X.presheaf.stalk x)} (hmem : b ∈ Z.stalkIdeal x) {φ : affineBlowUp (Z.stalkIdeal x) ⟶ Z.blowUp} (H : CategoryTheory.IsPullback φ (affineBlowUp.π (Z.stalkIdeal x)) Z.blowUpπ (X.fromSpecStalk x)) (V₀ : X.Opens) (hxV₀ : x ∈ V₀) (s₀ : ↑(X.presheaf.obj (Opposite.op V₀))) (hs₀ : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V₀ x hxV₀)) s₀ = b) (hF : (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V₀ (Z.blowUpπ x') ⋯)) s₀)}) : ∃ (q : ↥(Spec ↧↥(affineBlowUpAlgebra (Z.stalkIdeal x) b))), φ ((affineBlowUp.chart (Z.stalkIdeal x) ⟨b, hmem⟩) q) = x' ∧ Ideal.comap (algebraMap ↑(X.presheaf.stalk x) ↥(affineBlowUpAlgebra (Z.stalkIdeal x) b)) q.asIdeal = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)

The lift of a point x' of B_Z X in the chart of b to the local blow-up: a prime q of the chart algebra 𝒪_{X,x}[I_x/b] with φ (chart q) = x', lying over the maximal ideal.

theorem AlgebraicGeometry.exists_stalk_equiv_localization_atPrime_aux {X : Scheme} (Z : X.IdealSheafData) (x : ↥X) (x' : ↥Z.blowUp) (hx' : Z.blowUpπ x' = x) {n r : ℕ} (y : Fin n → ↑(X.presheaf.stalk x)) (hZ : Z.stalkIdeal x = Ideal.span (y '' {i : Fin n | ↑i < r})) (ρ : Fin n) (hρ : ↑ρ + 1 = r) (V₀ : X.Opens) (hxV₀ : x ∈ V₀) (s₀ : ↑(X.presheaf.obj (Opposite.op V₀))) (hs₀ : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V₀ x hxV₀)) s₀ = y ρ) (hF : (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V₀ (Z.blowUpπ x') ⋯)) s₀)}) : ∃ (𝔮 : Ideal ↥(affineBlowUpAlgebra (Z.stalkIdeal x) (y ρ))) (x_1 : 𝔮.IsPrime) (e : ↑(Z.blowUp.presheaf.stalk x') ≃+* Localization.AtPrime 𝔮), Ideal.comap (algebraMap ↑(X.presheaf.stalk x) ↥(affineBlowUpAlgebra (Z.stalkIdeal x) (y ρ))) 𝔮 = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ∀ (c : ↑(X.presheaf.stalk (Z.blowUpπ x'))), e ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) c) = (algebraMap (↥(affineBlowUpAlgebra (Z.stalkIdeal x) (y ρ))) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk x) ↥(affineBlowUpAlgebra (Z.stalkIdeal x) (y ρ))) (hx' ▸ c))

The chart model at an arbitrary point of the chart, in the chart algebra 𝒪_{X,x}[I_x/y_ρ] (the form before the identification with chartRing y ρ), over an abstract base point x with x' ↦ x.

theorem AlgebraicGeometry.exists_stalk_equiv_localization_atPrime {X : Scheme} (Z : X.IdealSheafData) (x' : ↥Z.blowUp) {n r : ℕ} (y : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ x'))) (hZ : Z.stalkIdeal (Z.blowUpπ x') = Ideal.span (y '' {i : Fin n | ↑i < r})) (ρ : Fin n) (hρ : ↑ρ + 1 = r) (hF : (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) (y ρ)}) : ∃ (𝔮 : Ideal ↥(IsLocalRing.chartRing y ρ)) (x : 𝔮.IsPrime) (e : ↑(Z.blowUp.presheaf.stalk x') ≃+* Localization.AtPrime 𝔮), Ideal.comap (algebraMap ↑(X.presheaf.stalk (Z.blowUpπ x')) ↥(IsLocalRing.chartRing y ρ)) 𝔮 = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (Z.blowUpπ x')) ∧ ∀ (c : ↑(X.presheaf.stalk (Z.blowUpπ x'))), e ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) c) = (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk (Z.blowUpπ x')) ↥(IsLocalRing.chartRing y ρ)) c)

The chart model at an arbitrary point of the chart ([Kol07, Definition 60]; [Hau14, Definitions 4.15–4.16]): for x' a point of B_Z X over x in the chart of y_ρ — F_{x'} = (π^* y_ρ) — with y a regular system of parameters at x adapted to Z (I_x = (y_0, …, y_{r-1}), ρ + 1 = r), the stalk 𝒪_{B,x'} is the localization of the chart ring chartRing y ρ at a prime 𝔮 lying over 𝔪_x, compatibly with π^*.