The standard charts of a smooth blow-up: the ideal of the center and the chart coordinates

E : EtaleCoordinatesAdapted f n r Z x is a chart of étale coordinates adapted to Z, J = E.centerIdeal = (v_0, …, v_{r-1}) ⊆ Γ(U) Kollár's (x_1, …, x_r) [Kol07, Definition 60], and Γ(U)[J/x_j] the chart ring of x_j (the affine blow-up algebra of Hauser's local blow-up, [Hau14, Definition 4.16]).

• Z(U) = J (ideal_eq_centerIdeal), from Z ∩ U = g⁻¹(L) (E.adapted) and the ideal of the coordinate subspace pulled back along the coordinate morphism g (toAffineSpace_appTop_X).
• Kollár's x_i = y_i x_j for i < r with y_i = x_i/x_j (the coordinates (60.2) of [Kol07, Definition 60]; the local parameters at a point of the exceptional divisor in the proof of [Wlo05, Lemma 2.6.3]), an identity in Γ(U)[1/x_j] (algebraMap_eq_ratio_mul).
• 𝒪_{B_ZX,x'} is a regular local ring of dimension n − trdeg_k κ(x') at every point x' (isRegularLocalRing_stalk_blowUp, ringKrullDim_stalk_blowUp_add_trdeg), from the smoothness of B_Z X of relative dimension n (BlowUpSmooth.lean) with the comparison of regular and smooth points (Hironaka/Algebra/RegularSmooth/).

Used for the charts and stalks of a smooth blow-up in ChartIso.lean, Hironaka/Scheme/Snc/ChartSncData.lean, Hironaka/Scheme/Snc/ChartStalk.lean and Hironaka/Resolution/Algebraic/Wlo05/EmbeddedChainColon.lean.

theorem AlgebraicGeometry.algebraMap_eq_ratio_mul {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n r : ℕ} {Z : X.IdealSheafData} {x : ↥X} (E : EtaleCoordinatesAdapted f n r Z x) {j : Fin n} (hj : ↑j < r) {i : Fin n} (hi : ↑i < r) : (algebraMap ↑(X.presheaf.obj (Opposite.op ↑E.U)) ↥(affineBlowUpAlgebra E.centerIdeal ↑(E.coord j hj))) (E.v i) = affineBlowUpAlgebra.ratio E.centerIdeal (E.coord j hj) (E.coord i hi) * (algebraMap ↑(X.presheaf.obj (Opposite.op ↑E.U)) ↥(affineBlowUpAlgebra E.centerIdeal ↑(E.coord j hj))) (E.v j)

In the chart of x_j, x_i = y_i x_j for i < r, where y_i = x_i/x_j (the coordinates (60.2) of [Kol07, Definition 60]; the proof of [Wlo05, Lemma 2.6.3]).

theorem AlgebraicGeometry.isRegularLocalRing_stalk_blowUp {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) (x' : ↥Z.blowUp) : IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk x')

The local rings of B_Z X are regular (B_Z X is smooth over k).

theorem AlgebraicGeometry.ringKrullDim_stalk_blowUp_add_trdeg {k : Type u} [Field k] {X : Scheme} [PerfectField k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hrn : r ≤ n) (x' : ↥Z.blowUp) : ringKrullDim ↑(Z.blowUp.presheaf.stalk x') + ↑(Cardinal.toENat (Algebra.trdeg k (IsLocalRing.ResidueField ↑(Z.blowUp.presheaf.stalk x')))) = ↑n

dim 𝒪_{B_ZX,x'} + trdeg_k κ(x') = n (B_Z X is smooth of relative dimension n over k; [TSPA, Tag 0A21]).

theorem AlgebraicGeometry.ι_appLE_top_eq_topIso_inv {X : Scheme} (U : X.Opens) (e : ⊤ ≤ (TopologicalSpace.Opens.map U.ι.base).obj U) : Scheme.Hom.appLE U.ι U ⊤ e = U.topIso.inv

The restriction Γ(X, U) → Γ(U, ⊤) along U.ι is the canonical isomorphism topIso.inv.

theorem AlgebraicGeometry.ideal_eq_centerIdeal {k : Type u} [Field k] {X : Scheme} {f : X ⟶ Spec ↧k} {n r : ℕ} {Z : X.IdealSheafData} {x : ↥X} (E : EtaleCoordinatesAdapted f n r Z x) : Z.ideal E.U = E.centerIdeal

On the sections of the chart U, the ideal of Z ∩ U is J = (v_0, …, v_{r-1}) (Kollár's "Z = (x_1 = ⋯ = x_r = 0)", [Kol07, Definition 60]): from Z ∩ U = g⁻¹(L) and the pull-back of the coordinate functions along g (toAffineSpace_appTop_X).