The induced coordinates of a chart at a point

[Hau14, Proposition 5.4 (6)] in its coordinate content at an arbitrary point: at a point a' of the exceptional divisor over a, in the chart of x_j (F_{a'} = (π^* z_j)), the induced coordinates are π^* z_i for i ≤ n − k and i = j, and w_i = π^* z_i / π^* z_j for the other centre coordinates; those vanishing at a' extend to a regular system of parameters of 𝒪_{B,a'} (exists_isRegularSystemOfParameters_induced). At a rational point all of them vanish and they are Hauser's coordinates; at a general point the vanishing ones are part of a system, as in Hironaka.Scheme.Snc.EtaleParameters.

The proof transports to Kollár's chart ring [Kol07, Definition 60]. The reindexing kollarReindex sends Hauser's positions (centre n − k, …, n − 1, chart index j) to Kollár's (centre 0, …, k − 1, chart index ρ = k − 1); exists_stalk_equiv_localization_atPrime of Hironaka.Scheme.Snc.LocalBlowUpPoint identifies 𝒪_{B,a'} with R'_𝔮, R' = chartRing y ρ, compatibly with π^*, and under this identification the induced coordinates are the chart functions y_l/y_ρ, y_ρ, y_m — for a fibre coordinate by cancelling the nonzero π^* z_j in the domain 𝒪_{B,a'} (ringEquiv_apply_eq_of_mul). The chart functions vanishing at 𝔮 extend to a regular system of parameters of R'_𝔮 (exists_span_eq_maximalIdeal_extend_chartYR of Hironaka.Scheme.Snc.ChartDerivations, from the derivations of 𝒪_{X,a} dual to y, exists_derivation_dual of Hironaka.Scheme.Snc.StalkDerivations), and the equivalence carries this back to 𝒪_{B,a'}.

Sources: [Hau14, Proposition 5.4 (6)]; [Hau03, Appendix C (7)]; [Kol07, Definition 60].

def AlgebraicGeometry.kollarIdx {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) : Fin n

Kollár's chart index ρ = k − 1 (zero-based: the last of the k centre coordinates).

Equations

• AlgebraicGeometry.kollarIdx hk hkn = ⟨k - 1, ⋯⟩

theorem AlgebraicGeometry.kollarIdx_val {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) : ↑(kollarIdx hk hkn) = k - 1

noncomputable def AlgebraicGeometry.kollarReindex {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) (j : Fin n) : Fin n ≃ Fin n

Kollár's indexing from Hauser's: the reversal i ↦ n − 1 − i sends the last k positions onto the first k, followed by the transposition putting j at k − 1.

Equations

• AlgebraicGeometry.kollarReindex hk hkn j = Equiv.trans Fin.revPerm (Equiv.swap j.rev (AlgebraicGeometry.kollarIdx hk hkn))

theorem AlgebraicGeometry.kollarReindex_apply_self {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) (j : Fin n) : (kollarReindex hk hkn j) j = kollarIdx hk hkn

theorem AlgebraicGeometry.lt_kollarReindex_iff {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) (j : Fin n) (hj : n - k ≤ ↑j) (i : Fin n) : ↑((kollarReindex hk hkn j) i) < k ↔ n - k ≤ ↑i

theorem AlgebraicGeometry.image_kollarReindex {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) (j : Fin n) (hj : n - k ≤ ↑j) : ⇑(kollarReindex hk hkn j) '' {i : Fin n | n - k ≤ ↑i} = {i : Fin n | ↑i < k}

theorem AlgebraicGeometry.chartYR_of_not_lt {R : Type u} [CommRing R] {n : ℕ} (y : Fin n → R) (ρ : Fin n) {l : Fin n} (hl : ¬l < ρ) : IsLocalRing.chartYR y ρ l = (algebraMap R ↥(IsLocalRing.chartRing y ρ)) (y l)

The chart function y_l, l ≥ ρ, is the constant y_l in the chart ring.

theorem AlgebraicGeometry.chartYR_mul_algebraMap {R : Type u} [CommRing R] {n : ℕ} (y : Fin n → R) (ρ : Fin n) {l : Fin n} (hl : l < ρ) : IsLocalRing.chartYR y ρ l * (algebraMap R ↥(IsLocalRing.chartRing y ρ)) (y ρ) = (algebraMap R ↥(IsLocalRing.chartRing y ρ)) (y l)

y_l · y_ρ = y_l in the chart ring, for the fibre coordinate y_l = y_l/y_ρ, l < ρ.

theorem AlgebraicGeometry.ringEquiv_apply_eq_of_const {R : Type u_1} {S : Type u_2} {R' : Type u_3} {L : Type u_4} [CommRing R] [CommRing S] [CommRing R'] [CommRing L] (e : S ≃+* L) (π : R →+* S) (g : R →+* R') (h : R' →+* L) (hcompat : ∀ (c : R), e (π c) = h (g c)) {w : S} {c : R} (hw : w = π c) {u : R'} (hu : u = g c) : e w = h u

Transport of a constant along e ∘ π = h ∘ g.

theorem AlgebraicGeometry.ringEquiv_apply_eq_of_mul {R : Type u_1} {S : Type u_2} {R' : Type u_3} {L : Type u_4} [CommRing R] [CommRing S] [CommRing R'] [CommRing L] [IsDomain L] (e : S ≃+* L) (π : R →+* S) (g : R →+* R') (h : R' →+* L) (hcompat : ∀ (c : R), e (π c) = h (g c)) {w : S} {ci cj : R} (hT : h (g cj) ≠ 0) (h1 : π ci = w * π cj) {u : R'} (h2 : u * g cj = g ci) : e w = h u

Transport of a ratio along e ∘ π = h ∘ g, cancelling the nonzero denominator.

theorem AlgebraicGeometry.image_eq_of_lt_iff {n kk : ℕ} (σ : Fin n ≃ Fin n) (hσ : ∀ (i : Fin n), ↑(σ i) < kk ↔ n - kk ≤ ↑i) : ⇑σ '' {i : Fin n | n - kk ≤ ↑i} = {i : Fin n | ↑i < kk}

A reindexing sending the last k positions onto the first k maps the centre's index set onto {i | i < k}.

theorem AlgebraicGeometry.exists_chartRing_model {X : Scheme} (Z : X.IdealSheafData) (a' : ↥Z.blowUp) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk a')] {n kk : ℕ} (hk : 1 ≤ kk) {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ a'))} (hZa : Z.stalkIdeal (Z.blowUpπ a') = Ideal.span (z '' {i : Fin n | n - kk ≤ ↑i})) {j : Fin n} (hF : (Z.comap Z.blowUpπ).stalkIdeal a' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j)}) (hne : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j) ≠ 0) (σ : Fin n ≃ Fin n) (hσ : ∀ (i : Fin n), ↑(σ i) < kk ↔ n - kk ≤ ↑i) (ρ : Fin n) (hρ : ↑ρ = kk - 1) (hσj : σ j = ρ) (w : Fin n → ↑(Z.blowUp.presheaf.stalk a')) (hw : ∀ (i : Fin n), ↑i < n - kk ∨ i = j → w i = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z i)) (hw' : ∀ (i : Fin n), n - kk ≤ ↑i → i ≠ j → (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z i) = w i * (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j)) : ∃ (𝔮 : Ideal ↥(IsLocalRing.chartRing (z ∘ ⇑σ.symm) ρ)) (x : 𝔮.IsPrime) (e : ↑(Z.blowUp.presheaf.stalk a') ≃+* Localization.AtPrime 𝔮), Ideal.comap (algebraMap ↑(X.presheaf.stalk (Z.blowUpπ a')) ↥(IsLocalRing.chartRing (z ∘ ⇑σ.symm) ρ)) 𝔮 = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (Z.blowUpπ a')) ∧ (∀ (c : ↑(X.presheaf.stalk (Z.blowUpπ a'))), e ((CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) c) = (algebraMap (↥(IsLocalRing.chartRing (z ∘ ⇑σ.symm) ρ)) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk (Z.blowUpπ a')) ↥(IsLocalRing.chartRing (z ∘ ⇑σ.symm) ρ)) c)) ∧ ∀ (i : Fin n), e (w i) = (algebraMap (↥(IsLocalRing.chartRing (z ∘ ⇑σ.symm) ρ)) (Localization.AtPrime 𝔮)) (IsLocalRing.chartYR (z ∘ ⇑σ.symm) ρ (σ i))

The chart-ring model of the point a': for a reindexing σ of the coordinates sending the centre's positions n − k, …, n − 1 onto 0, …, k − 1 and j to ρ = k − 1 (Kollár's indexing; kollarReindex), and y = z ∘ σ⁻¹, the stalk 𝒪_{B,a'} is (chartRing y ρ)_𝔮 for a prime 𝔮 over 𝔪_a, compatibly with π^*, and the induced coordinates w of the z_j-chart correspond to the chart functions y_{σ i}.

theorem AlgebraicGeometry.exists_isRegularSystemOfParameters_induced {X : Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ Spec ↧k) [Smooth f] (Z : X.IdealSheafData) (a' : ↥Z.blowUp) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk a')] {n kk : ℕ} (hk : 1 ≤ kk) (hkn : kk ≤ n) {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ a'))} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (Z.blowUpπ a')) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk (Z.blowUpπ a'))) (hZa : Z.stalkIdeal (Z.blowUpπ a') = Ideal.span (z '' {i : Fin n | n - kk ≤ ↑i})) {j : Fin n} (hj : n - kk ≤ ↑j) (hF : (Z.comap Z.blowUpπ).stalkIdeal a' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j)}) (hne : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j) ≠ 0) (w : Fin n → ↑(Z.blowUp.presheaf.stalk a')) (hw : ∀ (i : Fin n), ↑i < n - kk ∨ i = j → w i = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z i)) (hw' : ∀ (i : Fin n), n - kk ≤ ↑i → i ≠ j → (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z i) = w i * (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ a')) (z j)) : ∃ (m : ℕ) (z' : Fin m → ↑(Z.blowUp.presheaf.stalk a')), (Ideal.span (Set.range z') = IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk a') ∧ ↑m = ringKrullDim ↑(Z.blowUp.presheaf.stalk a')) ∧ ∃ (σ : { i : Fin n // w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk a') } → Fin m), Function.Injective σ ∧ ∀ (i : { i : Fin n // w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk a') }), z' (σ i) = w ↑i

[Hau14, Proposition 5.4 (6)], the coordinate content at an arbitrary (not necessarily rational) point: the induced coordinates of the z_j-chart vanishing at a' extend to a regular system of parameters of 𝒪_{B,a'}.