Two embedded smooth points of equal codimension are étale equivalent

Kollár, in the proof of Theorem 27: for two smooth points x, x' of an embedded X ↪ P, the embeddings (x ∈ X ↪ P) and (x' ∈ X ↪ P) "have isomorphic étale neighborhoods" ([Kol07, Theorem 27], the proof); and "any two smooth points of X are étale equivalent" ([Kol07, 4.2]). In the vocabulary of this library: for a closed subscheme V(Z) smooth of relative dimension n − r in X smooth of relative dimension n over the perfect field k, and two closed points x, x' ∈ V(Z), there is an affine scheme W with a point q and two étale maps ψ, ψ' : W ⟶ X over k, ψ q = x, ψ' q = x', along which Z pulls back to the SAME ideal sheaf Z.comap ψ = Z.comap ψ': the pair of embedded points is one embedded point of W.

The construction: adapted étale coordinates at each point (EtaleCoordinatesAdapted.lean), chosen to VANISH at the point (a regular system of parameters lies in the maximal ideal), so that both coordinate morphisms g : U ⟶ 𝔸ⁿ_k, g' : U' ⟶ 𝔸ⁿ_k send the point to the origin (toAffineSpace_base_eq_origin_iff, Origin.lean) and Z to the same coordinate subspace L = V(t_0, …, t_{r−1}); W := U ×_{𝔸ⁿ} U' is the fibre product (affine, as a fibre product of affine schemes), q a point over (x, x') (Mathlib's exists_preimage_pullback), ψ, ψ' the projections followed by the inclusions, étale by base change, and Z.comap ψ = L.comap (pr₁ ≫ g) = L.comap (pr₂ ≫ g') = Z.comap ψ'.

EtaleNbhdPair (Graph.lean) is the ONE-point version (both maps to the same point, with isomorphic residue fields) and does not apply to two points with different residue fields; the pair here asks nothing of the residue field of q.

• exists_etaleCoordinatesAdapted_germ_mem_maximalIdeal: adapted étale coordinates with the coordinates vanishing at the point (the construction of EtaleCoordinatesAdapted.lean, the vanishing recorded).
• exists_etale_pair_of_isClosed: the two-point étale pair.
• exists_etale_pair_of_isClosedImmersion: the pair for a closed immersion X₁ ⟶ A of smooth schemes and two points of X₁ closed in A.

Used to show that the functorial resolution is an isomorphism over the smooth locus (Hironaka/Resolution/Algebraic/Kol07/Thm36/IsoOverSmoothLocus.lean).

theorem AlgebraicGeometry.exists_etaleCoordinatesAdapted_germ_mem_maximalIdeal {k : Type u} [Field k] [PerfectField k] {X : Scheme} (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 : ↥X} (hxZ : x ∈ Z.support) (hx : IsClosed {x}) : ∃ (c : EtaleCoordinatesAdapted f n r Z x), ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑c.U) x ⋯)) (c.v i) ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)

At a closed point x of a center V(Z) smooth of relative dimension n − r, there are étale coordinates adapted to Z whose coordinate functions all vanish at x: the adapted regular system of parameters lies in the maximal ideal, and the two restrictions of the construction of nonempty_etaleCoordinatesAdapted preserve germs.

theorem AlgebraicGeometry.exists_etale_pair_of_isClosed {k : Type u} [Field k] [PerfectField k] {X : Scheme} (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 x' : ↥X} (hxZ : x ∈ Z.support) (hx'Z : x' ∈ Z.support) (hx : IsClosed {x}) (hx' : IsClosed {x'}) : ∃ (W : Scheme) (q : ↥W) (ψ : W ⟶ X) (ψ' : W ⟶ X), IsAffine W ∧ Etale ψ ∧ Etale ψ' ∧ ψ q = x ∧ ψ' q = x' ∧ Z.comap ψ = Z.comap ψ' ∧ CategoryTheory.CategoryStruct.comp ψ f = CategoryTheory.CategoryStruct.comp ψ' f

Two closed points of a smooth center are étale equivalent as embedded points (the proof of [Kol07, Theorem 27]; [Kol07, 4.2]): an affine scheme W with a point q and two étale maps ψ, ψ' : W ⟶ X over k sending q to x and to x', along which Z pulls back to the same ideal sheaf. W is the fibre product of two adapted coordinate charts over 𝔸ⁿ_k, the coordinates vanishing at the points so that both land at the origin.

The pair for a closed immersion

theorem AlgebraicGeometry.exists_etale_pair_of_isClosedImmersion {k : Type u} [Field k] [PerfectField k] {A : Scheme} (fA : A ⟶ Spec ↧k) (n d : ℕ) [SmoothOfRelativeDimension n fA] {X₁ : Scheme} (emb : X₁ ⟶ A) [IsClosedImmersion emb] [SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp emb fA)] {x x' : ↥X₁} (hx : IsClosed {emb x}) (hx' : IsClosed {emb x'}) : ∃ (W : Scheme) (q : ↥W) (ψ : W ⟶ A) (ψ' : W ⟶ A), IsAffine W ∧ Etale ψ ∧ Etale ψ' ∧ ψ q = emb x ∧ ψ' q = emb x' ∧ (Scheme.Hom.ker emb).comap ψ = (Scheme.Hom.ker emb).comap ψ' ∧ CategoryTheory.CategoryStruct.comp ψ fA = CategoryTheory.CategoryStruct.comp ψ' fA

For a closed immersion emb : X₁ ⟶ A whose source is smooth of relative dimension d ≤ n over k: two points of X₁ whose images are closed in A are étale equivalent as embedded points, the pair of exists_etale_pair_of_isClosed for the kernel emb.ker, whose subscheme is X₁ (emb.toImage is an isomorphism, toImage_imageι).