Étale coordinates adapted to a center: the definitions

X is a scheme over a field k (f : X ⟶ Spec k), 𝔸ⁿ_k = Spec k[t_0, …, t_{n-1}] (that is, Spec (MvPolynomial (Fin n) k)), Z an ideal sheaf on X.

• toAffineSpace f U v : U ⟶ 𝔸ⁿ_k, for n sections v of an open U ⊆ X, is the morphism over k whose coordinate functions are the v i: U ⟶ Spec Γ(X, U) followed by Spec of the k-algebra map k[t] → Γ(X, U), t_i ↦ v i (MvPolynomial.aeval v; the k-algebra structure on Γ(X, U) is Scheme.Hom.sectionsAlgebra f U, through f). Kollár's "local coordinates (x_1, …, x_n)" read as a morphism to affine space ([Kol07, Definition 24] and [Kol07, Definition 60]; [TSPA, Tag 054L]). Mathlib's AffineSpace.homOfVector is not used: 𝔸(Fin n; S) forces the index type and the scheme into one universe.
• coordinateSubspace k n r ⊆ 𝔸ⁿ_k is the ideal sheaf of L = V(t_0, …, t_{r-1}), the coordinate subspace of codimension r: specIdealSheaf of the ideal centerIdeal k n r of the center of the model blow-up modelBlowUp k n r.
• EtaleCoordinatesAdapted f n r Z x: an affine open U ∋ x, sections v with toAffineSpace f U v étale, and Z ∩ U = g⁻¹(L) as closed subschemes of U (Z.comap U.ι = L.comap g). This is [Kol07, Definition 24, (4)]: local coordinates z_1, …, z_n at x with "Z = (z_{j_1} = ⋯ = z_{j_s} = 0)" near x, here with the coordinates made an étale chart: the form in which the blow-up of Z is computed locally (B_{Z∩U} U ≅ U ×_{𝔸ⁿ} B_L 𝔸ⁿ, Hironaka/Scheme/Smooth/BlowUpSmoothChart.lean).

noncomputable def AlgebraicGeometry.toAffineSpace {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {n : ℕ} (U : X.Opens) (v : Fin n → ↑(X.presheaf.obj (Opposite.op U))) : ↑U ⟶ Spec ↧(MvPolynomial (Fin n) k)

The morphism U ⟶ 𝔸ⁿ_k = Spec k[t_0, …, t_{n-1}] over k with coordinate functions v 0, …, v (n-1) ∈ Γ(X, U) (Kollár's local coordinates as a morphism to affine space).

Equations

• AlgebraicGeometry.toAffineSpace f U v = CategoryTheory.CategoryStruct.comp U.toSpecΓ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.aeval v).toRingHom))

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.coordinateSubspace (k : Type u) [Field k] (n r : ℕ) : (Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData

The coordinate subspace L = V(t_0, …, t_{r-1}) ⊆ 𝔸ⁿ_k as an ideal sheaf on Spec k[t_0, …, t_{n-1}]: the ideal sheaf of centerIdeal k n r = (t_0, …, t_{r-1}), the center of the model blow-up modelBlowUp k n r.

Equations

• AlgebraicGeometry.coordinateSubspace k n r = AlgebraicGeometry.specIdealSheaf (AlgebraicGeometry.CoordinateSubspace.centerIdeal k n r)

structure AlgebraicGeometry.EtaleCoordinatesAdapted {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n r : ℕ) (Z : X.IdealSheafData) (x : ↥X) : Type u

Étale coordinates at x adapted to Z ([Kol07, Definition 24, (4)]; [Kol07, Definition 60]): an affine open U ∋ x and sections v_0, …, v_{n-1} of U such that the coordinate morphism g = toAffineSpace f U v : U ⟶ 𝔸ⁿ_k is étale and Z ∩ U = g⁻¹(L), L = V(t_0, …, t_{r-1}), as closed subschemes of U.

• U : ↑X.affineOpens

  The affine chart around x.

• mem : x ∈ ↑self.U

  x lies in the chart.

• v : Fin n → ↑(X.presheaf.obj (Opposite.op ↑self.U))

  The coordinate functions.

• etale : Etale (toAffineSpace f (↑self.U) self.v)

  The coordinate morphism U ⟶ 𝔸ⁿ_k is étale.

• adapted : Z.comap (↑self.U).ι = (coordinateSubspace k n r).comap (toAffineSpace f (↑self.U) self.v)

  Adaptedness: Z ∩ U is the pullback of the coordinate subspace V(t_0, …, t_{r-1}).