Transport of the restricted centres between two smooth closed points

Kollár's localisation argument [Kol07, 4.2; Theorem 27, proof] says that "any two smooth points of X are étale equivalent" as embedded points, so that a property transported by the functoriality of the principalization sequence holds at one smooth point iff it holds at another. Hironaka.Resolution.Algebraic.Kol07.Thm36.IsoOverSmoothLocus uses this for an integral X with the generic point as the reference point. This module states the transport itself, for a scheme X whose smooth locus over k is smooth of ONE relative dimension d (the equidimensionality of the inputs of [Kol07, Theorem 36], for a reduced X: all components have dimension d), and the consequence that one smooth point over which no restricted centre has a point suffices:

• restrictedCenterHasPointOver_iff_of_mem_smoothLocus: for two closed points x, x' of the smooth locus, the restricted centres Z_i ∩ X̄_i of the truncated run have a point over x iff they have one over x'. The pair of embedded points is made étale equivalent by the two-point étale pair of Hironaka.Scheme.Smooth.TwoPointEtalePair on the open U₁ = A ∖ emb(X ∖ X^{ns}) of the ambient, over which X ∩ U₁ = X^{ns} is smooth of relative dimension d, and the pair is completed to surjective étale maps (restrictedCenterHasPointOver_iff_of_etale_pair).
• not_restrictedCenterHasPointOver_of_mem_smoothLocus_of_exists: if some point of the smooth locus has no restricted centre over it, no point of the smooth locus has (closed points of the Jacobson X meet every nonempty locally closed subset, and the set of points over which some restricted centre has a point is closed).

Both are stated for an arbitrary assignment F of a blow-up sequence to every triple that is functorial under smooth surjections (the hypothesis hfun), and applied to F := BP in Hironaka.Resolution.Algebraic.Kol07.Thm36.EqualAbsorbingIndex. The hypothesis on the smooth locus replaces the integrality of X in not_restrictedCenterHasPointOver_of_mem_smoothLocus.

theorem Hironaka.Resolution.restrictedCenterHasPointOver_iff_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (F : (T : AlgebraicGeometry.Triple k) → T.X.left.BlowUpSequence) (hfun : ∀ (T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ TA.X.left) [AlgebraicGeometry.Smooth g], Function.Surjective ⇑g → T'.IsPullbackOf TA g → F T' = (F TA).pullback g) (j : ℕ) {x x' : ↥X} (hx : x ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)) (hx' : x' ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)) (hxc : IsClosed {x}) (hx'c : IsClosed {x'}) (i : Fin ((F TA).take j).length) : AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb x) ↔ AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb x')

Two smooth closed points see the same restricted centres [Kol07, 4.2; Theorem 27, proof]: for a scheme X embedded in the ambient of the triple TA (empty boundary, ideal the ideal of X) whose smooth locus over k is smooth of one relative dimension d, an assignment F of blow-up sequences to triples that is functorial under smooth surjections (hfun), and two closed points x, x' of the smooth locus of X, the restricted centres of the truncation (F TA).take j have a point over emb x iff they have one over emb x'. The two embedded points are étale equivalent through the two-point étale pair on the open U₁ = A ∖ emb(X ∖ X^{ns}) of the ambient (exists_etale_pair_of_isClosedImmersion), and the pair is completed to surjective étale maps (restrictedCenterHasPointOver_iff_of_etale_pair).

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_of_mem_smoothLocus_of_exists {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (F : (T : AlgebraicGeometry.Triple k) → T.X.left.BlowUpSequence) (hfun : ∀ (T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ TA.X.left) [AlgebraicGeometry.Smooth g], Function.Surjective ⇑g → T'.IsPullbackOf TA g → F T' = (F TA).pullback g) (j : ℕ) (ha : ∃ y ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k), ∀ (i : Fin ((F TA).take j).length), ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb y)) {x : ↥X} (hx : x ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)) (i : Fin ((F TA).take j).length) : ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb x)

One smooth point suffices [Kol07, 4.2; Theorem 27, proof]: for X as in restrictedCenterHasPointOver_iff_of_mem_smoothLocus, if some point y of the smooth locus has no restricted centre of the truncation (F TA).take j over it, then no point of the smooth locus has. The set of points over which some restricted centre has a point is closed (isClosed_setOf_restrictedCenterHasPointOver); closed points of the Jacobson X lie in the nonempty locally closed sets X^{ns} ∖ B ∋ y and, for a contradiction, B ∩ X^{ns}, and the two closed points see the same restricted centres.