The standard charts of a smooth blow-up: the definitions

For a chart E : EtaleCoordinatesAdapted f n r Z x (an affine open U ∋ x with étale coordinates v and Z ∩ U = V(v_0, …, v_{r-1})), Kollár's ideal (x_1, …, x_r) of the center on U [Kol07, Definition 60] is E.centerIdeal = (v_0, …, v_{r-1}) ⊆ Γ(X, U), and E.coord j hj is x_j as an element of it: the generator whose chart Spec Γ(U)[J/x_j] ⟶ B_J (affineBlowUp.chart, the chart of Hauser's local blow-up [Hau14, Definition 4.16]) is the standard chart of x_j, on which Kollár's coordinates (60.2) live. Germs of elements of an affine ring at a point of Spec are AlgebraicGeometry.specGerm.

noncomputable def AlgebraicGeometry.EtaleCoordinatesAdapted.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) : Ideal ↑(X.presheaf.obj (Opposite.op ↑E.U))

Kollár's ideal (x_1, …, x_r) of the center [Kol07, Definition 60]: the ideal J = (v_0, …, v_{r-1}) of Γ(X, U) generated by the first r coordinates of the chart, the ideal of Z ∩ U.

Equations

• E.centerIdeal = Ideal.span (Set.range fun (i : { i : Fin n // ↑i < r }) => E.v ↑i)

theorem AlgebraicGeometry.EtaleCoordinatesAdapted.v_mem_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) {j : Fin n} (hj : ↑j < r) : E.v j ∈ E.centerIdeal

noncomputable def AlgebraicGeometry.EtaleCoordinatesAdapted.coord {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) : ↥E.centerIdeal

x_j (j < r) as an element of J, the generator of the standard chart of x_j.

Equations

• E.coord j hj = ⟨E.v j, ⋯⟩

@[simp]

theorem AlgebraicGeometry.EtaleCoordinatesAdapted.coe_coord {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) : ↑(E.coord j hj) = E.v j