Ring maps out of the chart ring: existence, the chart origin, and flatness

The algebra of a ring map χ : R' → S out of the chart ring R' = R[xᵢ/x_r : i < r] of the chart dividing by x_r ([Kol07, (60.2)]).

• exists_chartRing_hom_of_mul_eq: a ring map ρ : R → S into a domain with ρ(x_r) = w ≠ 0 and ρ(xⱼ) = w · vⱼ (j < r) extends to χ : R' → S with χ(xⱼ / x_r) = vⱼ. It is stated for an arbitrary family of ratios v, so that it applies to coordinates centred at a point of the exceptional divisor other than the origin of the chart.
• comap_maximalIdeal_eq_chartOrigin: if S is local and χ sends the xⱼ / x_r (j < r) and the xᵢ into 𝔪_S, then χ⁻¹(𝔪_S) is the chart origin 𝔪' = (y₀, …, y_{n−1}), a maximal ideal of R' (chartOrigin_isMaximal, Hironaka/Algebra/Local/Chart.lean).
• chartLocalHom: the local homomorphism R'_{𝔪'} → S induced by χ when χ⁻¹(𝔪_S) = 𝔪'.
• flat_comp_algebraMap_adicCompletion: R' → Ŝ is flat as soon as the induced map of completions (R'_{𝔪'})^ → Ŝ is bijective: R' → R'_{𝔪'} is a localization, hence flat; R'_{𝔪'} → (R'_{𝔪'})^ is the completion of a Noetherian local ring, flat by [Mat89, Theorem 8.8] (Mathlib's AdicCompletion.flat_of_isNoetherian); and a bijective ring map is flat. The bijectivity is supplied by Hironaka/Algebra/Local/ChartCompletionHom.lean.

These are the algebraic inputs of the description of the strict transform at a point of the exceptional divisor in Hironaka/Manifold/BlowUp/Transform/StrictSubspaceCompletion.lean and Hironaka/Manifold/BlowUp/Transform/StrictSubspaceProp313.lean ([BM97, Proposition 3.13]), and of the transport of the order bound of [Kol07, Lemma 61] to the analytic stalk (Hironaka/Algebra/Local/ChartOrderFaithful.lean, Hironaka/Resolution/Analytic/GoingUp/MaxOrder.lean). The statements are not in the sources.

theorem IsLocalRing.exists_chartRing_hom_of_mul_eq {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsDomain S] (ρ : R →+* S) {w : S} (hw : w ≠ 0) (v : Fin n → S) (hρr : ρ (x r) = w) (hρj : ∀ j < r, ρ (x j) = w * v j) : ∃ (χ : ↥(chartRing x r) →+* S), (∀ (s : R), χ ((algebraMap R ↥(chartRing x r)) s) = ρ s) ∧ (∀ j < r, χ (chartYR x r j) = v j) ∧ χ ((algebraMap R ↥(chartRing x r)) (x r)) = w

A ring map ρ : R → S into a domain with ρ(x_r) = w ≠ 0 and ρ(xⱼ) = w · vⱼ for j < r extends to the chart ring of [Kol07, (60.2)], xⱼ / x_r ↦ vⱼ.

theorem IsLocalRing.comap_maximalIdeal_eq_chartOrigin {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (χ : ↥(chartRing x r) →+* S) (hY : ∀ j < r, χ (chartYR x r j) ∈ maximalIdeal S) (hX : ∀ (i : Fin n), χ ((algebraMap R ↥(chartRing x r)) (x i)) ∈ maximalIdeal S) : Ideal.comap χ (maximalIdeal S) = chartOrigin x r

If χ : R' → S sends the xⱼ / x_r (j < r) and the xᵢ into 𝔪_S, then χ⁻¹(𝔪_S) is the chart origin 𝔪' = (y₀, …, y_{n−1}), a maximal ideal (chartOrigin_isMaximal).

theorem IsLocalRing.isUnit_of_mem_primeCompl_chartOrigin {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] (χ : ↥(chartRing x r) →+* S) [(chartOrigin x r).IsPrime] (hχ : Ideal.comap χ (maximalIdeal S) = chartOrigin x r) (y : ↥(chartOrigin x r).primeCompl) : IsUnit (χ ↑y)

noncomputable def IsLocalRing.chartLocalHom {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] (χ : ↥(chartRing x r) →+* S) [(chartOrigin x r).IsPrime] (hχ : Ideal.comap χ (maximalIdeal S) = chartOrigin x r) : Localization.AtPrime (chartOrigin x r) →+* S

The local homomorphism R'_{𝔪'} → S induced by χ when χ⁻¹(𝔪_S) = 𝔪'.

Equations

• IsLocalRing.chartLocalHom x r χ hχ = IsLocalization.lift ⋯

theorem IsLocalRing.chartLocalHom_algebraMap {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] (χ : ↥(chartRing x r) →+* S) [(chartOrigin x r).IsPrime] (hχ : Ideal.comap χ (maximalIdeal S) = chartOrigin x r) (z : ↥(chartRing x r)) : (chartLocalHom x r χ hχ) ((algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOrigin x r))) z) = χ z

theorem IsLocalRing.isLocalHom_chartLocalHom {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] (χ : ↥(chartRing x r) →+* S) [(chartOrigin x r).IsPrime] (hχ : Ideal.comap χ (maximalIdeal S) = chartOrigin x r) : IsLocalHom (chartLocalHom x r χ hχ)

theorem IsLocalRing.flat_comp_algebraMap_adicCompletion {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {S : Type u_1} [CommRing S] [IsLocalRing S] [IsRegularLocalRing R] (χ : ↥(chartRing x r) →+* S) [(chartOrigin x r).IsPrime] (hχ : Ideal.comap χ (maximalIdeal S) = chartOrigin x r) (hbij : Function.Bijective ⇑(completionMap (chartLocalHom x r χ hχ))) : ((algebraMap S (AdicCompletion (maximalIdeal S) S)).comp χ).Flat

R' → Ŝ is flat when the induced map of completions (R'_{𝔪'})^ → Ŝ is bijective: R' → R'_{𝔪'} and R'_{𝔪'} → (R'_{𝔪'})^ are flat ([Mat89, Theorem 8.8] for the completion) and the last factor is an isomorphism.