The chart of the shifted coordinates

Kollár's linear change of the (x₁, …, x_r)-coordinates that moves the origin of the chart to another point of the exceptional fibre (the proof of [Kol07, Lemma 61]): for a ∈ Kʳ with lifts ãᵢ ∈ R, the coordinates x'ᵢ = xᵢ − ãᵢ x_r (i < r), x'ⱼ = xⱼ (j ≥ r) generate 𝔪 and P, define the same chart ring (x'ᵢ/x_r = yᵢ − ãᵢ), and the origin of their chart is the point 𝔪'_a = ⟨yᵢ − ãᵢ, x_r, xⱼ⟩ of the fibre. Hironaka/Algebra/Local/Chart.lean proves this with the denominator as a parameter (chartRingOf x' r (x r) = chartRing x r, chartOriginAt). For Lemma 61 at 𝔪'_a (Hironaka/Algebra/Local/Lemma61.lean) the statements about the chart of x' — its origin, its local ring, its Cohen structure — are stated for chartRing x' r, whose ambient ring is R[1/x'_r]; this file provides the R-algebra isomorphism chartRingEquivShift : chartRing x' r ≃ₐ[R] chartRing x r (through R[1/x'_r] ≃ R[1/x_r], x'_r = x_r) and computes it on the generators: yᵢ' ↦ yᵢ − ãᵢ (i < r), yⱼ' ↦ yⱼ (j ≥ r), so that it carries the origin of the chart of x' onto 𝔪'_a.

theorem IsLocalRing.powers_shiftCoords_self {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Submonoid.powers (shiftCoords x r a r) = Submonoid.powers (x r)

theorem IsLocalRing.isLocalization_powers_shiftCoords {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : IsLocalization (Submonoid.powers (shiftCoords x r a r)) (Localization.Away (x r))

R[1/x_r] is also the localization at the powers of x'_r = x_r.

noncomputable def IsLocalRing.awayEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Localization.Away (shiftCoords x r a r) ≃ₐ[R] Localization.Away (x r)

The identification R[1/x'_r] ≃ R[1/x_r] (x'_r = x_r).

Equations

• IsLocalRing.awayEquivShift x r a = IsLocalization.algEquiv (Submonoid.powers (IsLocalRing.shiftCoords x r a r)) (Localization.Away (IsLocalRing.shiftCoords x r a r)) (Localization.Away (x r))

theorem IsLocalRing.awayEquivShift_algebraMap {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (b : R) : (awayEquivShift x r a) ((algebraMap R (Localization.Away (shiftCoords x r a r))) b) = (algebraMap R (Localization.Away (x r))) b

theorem IsLocalRing.awayEquivShift_mk {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (b : R) : (awayEquivShift x r a) (Localization.mk b ⟨shiftCoords x r a r, ⋯⟩) = Localization.mk b ⟨x r, ⋯⟩

theorem IsLocalRing.map_chartRing_awayEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Subalgebra.map (↑(awayEquivShift x r a)) (chartRing (shiftCoords x r a) r) = chartRing x r

The identification carries the chart ring of x' onto the chart ring of x (chartRingOf_shiftCoords).

noncomputable def IsLocalRing.chartRingEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : ↥(chartRing (shiftCoords x r a) r) ≃ₐ[R] ↥(chartRing x r)

The equality of the two chart rings as an isomorphism of R-algebras: chartRing x' r ≃ chartRing x r.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalRing.coe_chartRingEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (z : ↥(chartRing (shiftCoords x r a) r)) : ↑((chartRingEquivShift x r a) z) = (awayEquivShift x r a) ↑z

theorem IsLocalRing.chartRingEquivShift_algebraMap {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (b : R) : (chartRingEquivShift x r a) ((algebraMap R ↥(chartRing (shiftCoords x r a) r)) b) = (algebraMap R ↥(chartRing x r)) b

theorem IsLocalRing.chartRingEquivShift_chartYR_of_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) {i : Fin n} (hi : i < r) : (chartRingEquivShift x r a) (chartYR (shiftCoords x r a) r i) = chartYR x r i - (algebraMap R ↥(chartRing x r)) (a i)

yᵢ' ↦ yᵢ − ãᵢ for i < r.

theorem IsLocalRing.chartRingEquivShift_chartYR_of_not_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) {j : Fin n} (hj : ¬j < r) : (chartRingEquivShift x r a) (chartYR (shiftCoords x r a) r j) = chartYR x r j

yⱼ' ↦ yⱼ for j ≥ r.

theorem IsLocalRing.map_chartOrigin_chartRingEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Ideal.map (chartRingEquivShift x r a) (chartOrigin (shiftCoords x r a) r) = chartOriginAt x r a

The isomorphism carries the origin of the chart of x' onto the point 𝔪'_a (𝔪'_a is the origin of the chart for x', mem_chartOriginAt_iff).

theorem IsLocalRing.chartCenter_shiftCoords {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : chartCenter (shiftCoords x r a) r = chartCenter x r

theorem IsLocalRing.chartRingEquivShift_comp_algebraMap {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : (↑(chartRingEquivShift x r a)).comp (algebraMap R ↥(chartRing (shiftCoords x r a) r)) = algebraMap R ↥(chartRing x r)

theorem IsLocalRing.map_transformIdeal_chartRingEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) : Ideal.map (↑(chartRingEquivShift x r a)) (transformIdeal (shiftCoords x r a) r I m) = transformIdeal x r I m

The transform does not depend on the coordinates: the isomorphism carries the transform of I computed with x' onto the transform computed with x (eq_transformIdeal_of_map_chartCenter_pow_mul_eq).

theorem IsLocalRing.map_primeCompl_chartRingEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) [(chartOrigin (shiftCoords x r a) r).IsPrime] [(chartOriginAt x r a).IsPrime] : Submonoid.map (chartRingEquivShift x r a).toRingEquiv.toMonoidHom (chartOrigin (shiftCoords x r a) r).primeCompl = (chartOriginAt x r a).primeCompl

noncomputable def IsLocalRing.localizationEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) [(chartOrigin (shiftCoords x r a) r).IsPrime] [(chartOriginAt x r a).IsPrime] : Localization.AtPrime (chartOrigin (shiftCoords x r a) r) ≃+* Localization.AtPrime (chartOriginAt x r a)

The isomorphism of the local rings at the origin of the chart of x' and at 𝔪'_a.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalRing.localizationEquivShift_algebraMap {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) [(chartOrigin (shiftCoords x r a) r).IsPrime] [(chartOriginAt x r a).IsPrime] (z : ↥(chartRing (shiftCoords x r a) r)) : (localizationEquivShift x r a) ((algebraMap (↥(chartRing (shiftCoords x r a) r)) (Localization.AtPrime (chartOrigin (shiftCoords x r a) r))) z) = (algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOriginAt x r a))) ((chartRingEquivShift x r a) z)

theorem IsLocalRing.localizationEquivShift_algebraMap_R {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) [(chartOrigin (shiftCoords x r a) r).IsPrime] [(chartOriginAt x r a).IsPrime] (b : R) : (localizationEquivShift x r a) ((algebraMap R (Localization.AtPrime (chartOrigin (shiftCoords x r a) r))) b) = (algebraMap R (Localization.AtPrime (chartOriginAt x r a))) b

theorem IsLocalRing.map_transformIdeal_localizationEquivShift {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) [(chartOrigin (shiftCoords x r a) r).IsPrime] [(chartOriginAt x r a).IsPrime] {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) : Ideal.map (↑(localizationEquivShift x r a)) (Ideal.map (algebraMap (↥(chartRing (shiftCoords x r a) r)) (Localization.AtPrime (chartOrigin (shiftCoords x r a) r))) (transformIdeal (shiftCoords x r a) r I m)) = Ideal.map (algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOriginAt x r a))) (transformIdeal x r I m)