Transport of points between blow-up charts

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Surfaces.ConcretePoints7 8/-!9# Transport of points between blow-up charts10 11Comparison of the two affine charts of a point blow-up through their overlap: the gluing map and12its localization property, transport of maximal ideals, residue fields, local rings and their13completions between the charts and the overlap, together with the localization and14completion algebra this needs and the computation of strict transforms and their intersection15multiplicities on the concrete surface.16 17## Main results18 19* `SurfaceBlowup.blowup_overlap_isLocalization_right`: the overlap is a localization of either20  chart.21* `SurfaceBlowup.overlap_point_residue_field_equiv`,22  `SurfaceBlowup.completed_point_transport_left`, `SurfaceBlowup.completed_point_transport_right`:23  points on the exceptional divisor look the same from both charts.24* `SurfaceBlowup.concrete_strict_transform_generators`,25  `SurfaceBlowup.concrete_infinity_strict_transform_multiplicity`: strict transforms on the26  concrete surface.27 28Provenance: `Thm_SurfaceBlowupV2_` nodes `child_ideal_generator_transverse_finite`,29`concrete_infinity_strict_transform_multiplicity`, `linear_composition_index`,30`local_completion_transport`, `localization_map_{comap_comp,finite_iInf}`,31`finite_support_kernel_localize`, `localization_principal_quotient_commute`, `monomial_span_pow`,32`fixed_tangent_cell_generator_coefficients`, `negative_laurent_twist_has_no_kernel`,33`nonzerodivisor_survives_localization`, `normalization_linear_part_{is_quotient_matrix,34cokernel_length_eq}`, `opposite_untruncated_chart_restriction`,35`actual_blowup_restriction_exists`, `blowup_overlap_{symmetry,isLocalization_right}`,36`overlap_exceptional_point_comap_maximal{,_right}`, `overlap_exceptional_quotient_domain`,37`overlap_point_residue_field_equiv`, `overlap_prime_localization_{left,right}`,38`completed_point_transport_{left,right}`, `pairwise_distinct_irreducible_pow_iInf`,39`polynomial_ideal_of_irreducible_pow_le`, `polynomial_quotient_irreducible_pow_length`,40`principal_ideal_image`, `concrete_strict_transform_generators`,41`principal_ideal_unit_invariance`.42-/43 44open scoped BigOperators ENNReal45 46namespace SurfaceBlowup47 48private theorem transverse_of_concreteSurface_equiv (S : Type) [CommRing S] [IsLocalRing S]49    [IsNoetherianRing S] (O' : Type) [CommRing O'] [IsDomain O'] [IsDiscreteValuationRing O']50    (pi' : O') (hpi' : Irreducible pi') (u' : (TwoSeries O')ˣ) (a' b' : ℕ) (ha' : 0 < a')51    (ψ : S ≃+* ConcreteSurface O' pi' u' a' b') (e g : S) (he : ψ e = surfaceT O' pi' u' a' b')52    (n : ℕ) (hlen : Module.length S (S ⧸ (Ideal.span {g} ⊔ Ideal.span {e})) = (n : ℕ∞))53    (hreg : Function.Injective (fun y : S ↦ e * y)) :54    Function.Injective (fun w : S ⧸ Ideal.span {g} ↦ Ideal.Quotient.mk (Ideal.span {g}) e * w) ∧55    Function.Injective (fun w : S ⧸ Ideal.span {e} ↦ Ideal.Quotient.mk (Ideal.span {e}) g * w) ∧56    ∃ L : ℕ, (IsLocalRing.maximalIdeal S)^L ≤ Ideal.span {g, e} := by57  obtain ⟨q, -⟩ := concrete_surface_quotient_T_equiv O' pi' hpi' u' a' b' ha'58  have hE : ψ.symm (surfaceT O' pi' u' a' b') = e := by rw [← he]; simp59  obtain ⟨h1, -⟩ :=60    concrete_surface_equiv_curve_length_and_regular S O' pi' u' a' b' ψ q g61  rw [hE, Ideal.span_insert, hlen] at h162  have hne : q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (ψ g)) ≠ 0 := by63    intro h064    rw [h0, PowerSeries.order_zero] at h165    exact absurd h1 (by simp)66  let Q : (S ⧸ Ideal.span {e}) ≃+* PowerSeries (IsLocalRing.ResidueField O') :=67    (Ideal.quotientEquiv (Ideal.span {e}) (Ideal.span {surfaceT O' pi' u' a' b'}) ψ68      (by rw [Ideal.map_span, Set.image_singleton]; simp [he])).trans q69  have hQ : Q (Ideal.Quotient.mk (Ideal.span {e}) g) =70      q (Ideal.Quotient.mk (Ideal.span {surfaceT O' pi' u' a' b'}) (ψ g)) := by71    simp [Q]72  exact transverse_of_reduction_ne_zero S e g hreg _ Q (by rw [hQ]; exact hne)73 74/-- Order of the reflected power series. -/75private theorem order_reflected_sum {k K : Type} [Field k] [Field K] (κ : k →+* K) (d : ℕ)76    (r : Fin (d + 1) → k) (hne : ∃ i, r i ≠ 0) :77    (∑ i : Fin (d+1), PowerSeries.C (κ (r i)) * PowerSeries.X ^ (d - i.val) : PowerSeries K).order =78    ((d - (∑ i : Fin (d+1), Polynomial.C (r i) * Polynomial.X^i.val :79      Polynomial k).natDegree : ℕ) : ℕ∞) := by80  set H : Polynomial k := ∑ i : Fin (d+1), Polynomial.C (r i) * Polynomial.X^i.val with hH81  have hcoeff : ∀ i : Fin (d+1), H.coeff i.val = r i := by82    intro i83    rw [hH, Polynomial.finsetSum_coeff, Finset.sum_eq_single i]84    · simp85    · intro j _ hj86      rw [Polynomial.coeff_C_mul_X_pow, if_neg]87      intro h; exact hj (Fin.ext h.symm)88    · simp89  have hdeg : H.natDegree ≤ d := by90    rw [hH]91    refine Polynomial.natDegree_sum_le_of_forall_le _ _ (fun i _ ↦ ?_)92    exact (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (by omega)93  have hH0 : H ≠ 0 := by94    obtain ⟨i, hi⟩ := hne95    intro h; apply hi; rw [← hcoeff i, h, Polynomial.coeff_zero]96  have hF : ∀ m, m ≤ d → PowerSeries.coeff m (∑ i : Fin (d+1), PowerSeries.C (κ (r i)) *97      PowerSeries.X ^ (d - i.val) : PowerSeries K) = κ (H.coeff (d - m)) := by98    intro m hm99    have := hcoeff ⟨d - m, by omega⟩100    simp only at this101    rw [this, map_sum, Finset.sum_eq_single (⟨d - m, by omega⟩ : Fin (d+1))]102    · rw [PowerSeries.coeff_C_mul_X_pow, if_pos (by simp; omega)]103    · intro j _ hj104      rw [PowerSeries.coeff_C_mul_X_pow, if_neg]105      intro h; apply hj; ext; simp; omega106    · simp107  rw [PowerSeries.order_eq_nat]108  refine ⟨?_, fun m hm ↦ ?_⟩109  · rw [hF _ (by omega), show d - (d - H.natDegree) = H.natDegree by omega,110      Polynomial.coeff_natDegree]111    simpa using hH0112  · rw [hF _ (by omega), Polynomial.coeff_eq_zero_of_natDegree_lt (by omega), map_zero]113 114/-- For linear maps `f : M → N` and injective `g : N → P`, the index of the range of `g ∘ f` is the115product of the indices of the ranges of `f` and `g`. -/116theorem linear_composition_index (R M N P : Type) [CommRing R] [AddCommGroup M] [Module R M]117    [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)118    (hg : Function.Injective g) :119    (g.comp f).range.toAddSubgroup.index = f.range.toAddSubgroup.index * g.range.toAddSubgroup.index120    := by121  have h : (g.comp f).range.toAddSubgroup = f.range.toAddSubgroup.map g.toAddMonoidHom := by122    ext y123    simp [LinearMap.mem_range]124  have h2 : g.range.toAddSubgroup = g.toAddMonoidHom.range := by125    ext y126    simp [LinearMap.mem_range]127  rw [h, h2]128  exact AddSubgroup.index_map_of_injective _ (f := g.toAddMonoidHom) hg129 130open AdicCompletion in131private theorem local_completion_transport_factorPow_evalₐ {R : Type} [CommRing R] (I : Ideal R)132    {m n : ℕ} (h : m ≤ n) (x : AdicCompletion I R) :133    Ideal.Quotient.factorPow I h (evalₐ I n x) = evalₐ I m x := by134  obtain ⟨s, rfl⟩ := AdicCompletion.mk_surjective I R x135  simp only [evalₐ_mk]136  have := AdicCauchySequence.mk_eq_mk h s137  rw [Submodule.Quotient.eq] at this138  simp only [Ideal.Quotient.factorPow, Ideal.Quotient.factor_mk]139  rw [Ideal.Quotient.eq]140  simpa using this141 142open AdicCompletion in143private theorem local_completion_transport_lift {A B : Type} [CommRing A] [CommRing B] (I : Ideal A)144    (J : Ideal B) (ψ : A ≃+* B) (h : ∀ n : ℕ, J ^ n = (I ^ n).map ψ) :145    ∃ F : AdicCompletion I A →+* AdicCompletion J B, ∀ (n : ℕ) (x : AdicCompletion I A),146      evalₐ J n (F x) = Ideal.quotientEquiv (I ^ n) (J ^ n) ψ (h n) (evalₐ I n x) := by147  refine ⟨liftRingHom J (fun n ↦ (Ideal.quotientEquiv (I ^ n) (J ^ n) ψ (h n)).toRingHom.comp148    (evalₐ I n).toRingHom) ?_, ?_⟩149  · intro m n hle150    ext x151    simp only [RingHom.coe_comp, Function.comp_apply, RingEquiv.toRingHom_eq_coe,152      AlgHom.toRingHom_eq_coe, RingHom.coe_coe]153    rw [← local_completion_transport_factorPow_evalₐ I hle x]154    obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (evalₐ I n x)155    rw [← ha]156    rfl157  · intro n x158    rw [evalₐ_liftRingHom]159    rfl160 161/-- A ring isomorphism of Noetherian local rings induces an isomorphism of their maximal-adic162completions compatible with the completion maps. -/163private theorem local_completion_transport (S S' : Type) [CommRing S] [CommRing S'] [IsLocalRing S]164    [IsLocalRing S'] [IsNoetherianRing S] [IsNoetherianRing S'] (φ : S ≃+* S') :165    ∃ Φ : LocalCompletion S ≃+* LocalCompletion S', ∀ s : S, Φ166    (localCompletionMap S s) = localCompletionMap S' (φ s) := by167  have hm : (IsLocalRing.maximalIdeal S).map φ = IsLocalRing.maximalIdeal S' := by168    rw [← Ideal.comap_symm]169    exact IsLocalRing.maximalIdeal_comap (φ.symm : S' →+* S)170  have hm' : (IsLocalRing.maximalIdeal S').map φ.symm = IsLocalRing.maximalIdeal S := by171    rw [Ideal.map_symm]172    exact IsLocalRing.maximalIdeal_comap (φ : S →+* S')173  obtain ⟨F, hF⟩ := local_completion_transport_lift (IsLocalRing.maximalIdeal S)174    (IsLocalRing.maximalIdeal S') φ (fun n ↦ by rw [Ideal.map_pow, hm])175  obtain ⟨G, hG⟩ := local_completion_transport_lift (IsLocalRing.maximalIdeal S')176    (IsLocalRing.maximalIdeal S) φ.symm (fun n ↦ by rw [Ideal.map_pow, hm'])177  refine ⟨RingEquiv.ofRingHom F G ?_ ?_, ?_⟩178  · ext1 x179    refine AdicCompletion.ext_evalₐ fun n ↦ ?_180    simp only [RingHom.comp_apply, RingHom.id_apply, hF, hG]181    obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (AdicCompletion.evalₐ _ n x)182    rw [← ha]183    exact congrArg (Ideal.Quotient.mk _) (RingEquiv.apply_symm_apply _ a)184  · ext1 x185    refine AdicCompletion.ext_evalₐ fun n ↦ ?_186    simp only [RingHom.comp_apply, RingHom.id_apply, hF, hG]187    obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (AdicCompletion.evalₐ _ n x)188    rw [← ha]189    exact congrArg (Ideal.Quotient.mk _) (RingEquiv.symm_apply_apply _ a)190  · intro s191    refine AdicCompletion.ext_evalₐ fun n ↦ ?_192    simp only [RingEquiv.ofRingHom_apply, hF, localCompletionMap]193    rw [AlgHom.commutes, AlgHom.commutes, Ideal.Quotient.algebraMap_eq,194      Ideal.Quotient.algebraMap_eq]195    rfl196 197/-- Extending the contraction of `J` along `S → T` composed with the localization `A → S` recovers198the contraction of `J` to `S`. -/199private theorem localization_map_comap_comp (A S : Type) [CommRing A] [CommRing S] [Algebra A S]200    (M : Submonoid A) [IsLocalization M S] (T : Type) [CommRing T] (ψ : S →+* T) (J : Ideal T) :201    (J.comap (ψ.comp (algebraMap A S))).map (algebraMap A S) = J.comap ψ := by202  rw [← Ideal.comap_comap]203  exact IsLocalization.map_under M S (J.comap ψ)204 205/-- Extension of ideals along a localization commutes with finite infima. -/206private theorem localization_map_finite_iInf (A S : Type) [CommRing A] [CommRing S] [Algebra A S]207    (M : Submonoid A) [IsLocalization M S] (ι : Type) [Finite ι] (I : ι → Ideal A) :208    (⨅ i, I i).map (algebraMap A S) = ⨅ i, (I i).map (algebraMap A S) := by209  classical210  have := Fintype.ofFinite ι211  simp only [← Finset.inf_univ_eq_iInf]212  induction (Finset.univ : Finset ι) using Finset.induction_on with213  | empty => simp only [Finset.inf_empty]; exact Ideal.map_top _214  | insert a s ha ih =>215    rw [Finset.inf_insert, Finset.inf_insert, IsLocalization.map_inf M, ih]216 217/-- Localizing a finite-support kernel: the extension to `S` of the finite-support kernel is the218infimum, over the points `i` that survive in `S`, of the transported completed ideals, the other219points collapsing to the unit ideal. -/220theorem finite_support_kernel_localize (A S : Type) [CommRing A] [CommRing S] [Algebra A S]221    (M : Submonoid A) [IsLocalization M S] (ι : Type) [Finite ι] (P : ι → Ideal A)222    [∀ i, (P i).IsPrime] (J : ∀ i, Ideal (CompletedLocalAt A (P i))) (σ : ι → Prop)223    (T : ι → Type) [∀ i, CommRing (T i)] (ψ : ∀ i, S →+* T i)224    (Φ : ∀ i, CompletedLocalAt A (P i) ≃+* T i)225    (hΦ : ∀ i, σ i → ∀ a : A, Φ i (completedPointMap A (P i) a) = ψ i (algebraMap A S a))226    (hcollapse : ∀ i, ¬ σ i → ∃ m ∈ M, m ∈ P i) (L : ι → ℕ)227    (hL : ∀ i, (P i)^(L i) ≤ (J i).comap (completedPointMap A (P i))) :228    (finiteSupportKernel A ι P J).map (algebraMap A S) = ⨅ i : {i // σ i},229    ((J i.val).map (Φ i.val)).comap (ψ i.val) := by230  have key : ∀ i, σ i → ((J i).comap (completedPointMap A (P i))).map (algebraMap A S)231      = ((J i).map (Φ i)).comap (ψ i) := by232    intro i hi233    have hc : (J i).comap (completedPointMap A (P i))234        = ((J i).map (Φ i)).comap ((ψ i).comp (algebraMap A S)) := by235      ext x236      rw [← Ideal.comap_symm, Ideal.mem_comap, Ideal.mem_comap, Ideal.mem_comap,237        RingHom.comp_apply, ← hΦ i hi]238      simp239    rw [hc]240    exact localization_map_comap_comp A S M (T i) (ψ i) _241  have top : ∀ i, ¬ σ i → ((J i).comap (completedPointMap A (P i))).map (algebraMap A S) = ⊤ := by242    intro i hi243    obtain ⟨m, hm, hmP⟩ := hcollapse i hi244    exact contracted_ideal_map_localization_top A S M (P i) _ (L i) (hL i) m hm hmP245  unfold finiteSupportKernel246  rw [localization_map_finite_iInf A S M ι]247  apply le_antisymm248  · exact le_iInf fun i ↦ iInf_le_of_le i.val (by rw [key i.val i.property])249  · refine le_iInf fun i ↦ ?_250    by_cases h : σ i251    · exact iInf_le_of_le ⟨i, h⟩ (by rw [key i h])252    · rw [top i h]; exact le_top253 254/-- Localizing at `z` commutes with taking the principal power quotient `A ⧸ (e)^j`. -/255theorem localization_principal_quotient_commute (A : Type) [CommRing A] (e z : A) (j : ℕ) :256    ∃ L : PrincipalPowerQuotient (Localization.Away z)257    (algebraMap A (Localization.Away z) e) j ≃+* Localization.Away258    (Ideal.Quotient.mk ((Ideal.span {e})^j) z), ∀ a : A, L259    (Ideal.Quotient.mk ((Ideal.span {algebraMap A (Localization.Away z) e})^j)260      (algebraMap A (Localization.Away z) a)) = algebraMap (PrincipalPowerQuotient A e j)261    (Localization.Away (Ideal.Quotient.mk ((Ideal.span {e})^j) z))262    (Ideal.Quotient.mk ((Ideal.span {e})^j) a) := by263  let φ0 : A →+* Localization.Away (Ideal.Quotient.mk ((Ideal.span {e})^j) z) :=264    (algebraMap (A ⧸ (Ideal.span {e})^j) _).comp (Ideal.Quotient.mk ((Ideal.span {e})^j))265  have hφ0 : IsUnit (φ0 z) :=266    IsLocalization.Away.algebraMap_isUnit (Ideal.Quotient.mk ((Ideal.span {e})^j) z)267  let φ : Localization.Away z →+* Localization.Away (Ideal.Quotient.mk ((Ideal.span {e})^j) z) :=268    IsLocalization.Away.lift z hφ0269  have hφ : ∀ a : A, φ (algebraMap A _ a) = φ0 a := fun a ↦ IsLocalization.Away.lift_eq z hφ0 a270  have hker : ∀ x ∈ (Ideal.span {algebraMap A (Localization.Away z) e})^j, φ x = 0 := by271    intro x hx272    rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx273    obtain ⟨y, rfl⟩ := hx274    have : (Ideal.Quotient.mk ((Ideal.span {e})^j) e) ^ j = 0 := by275      rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem, Ideal.span_singleton_pow]276      exact Ideal.mem_span_singleton_self _277    rw [map_mul, map_pow, hφ]278    simp only [φ0, RingHom.comp_apply]279    rw [← map_pow, this, map_zero, zero_mul]280  let f := Ideal.Quotient.lift _ φ hker281  have hf : ∀ a : A, f (Ideal.Quotient.mk _ (algebraMap A _ a)) =282      algebraMap (A ⧸ (Ideal.span {e})^j) _ (Ideal.Quotient.mk _ a) := hφ283  let ψ0 : A →+* Localization.Away z ⧸ (Ideal.span {algebraMap A (Localization.Away z) e})^j :=284    (Ideal.Quotient.mk _).comp (algebraMap A _)285  have hψ0 : ∀ x ∈ (Ideal.span {e})^j, ψ0 x = 0 := by286    intro x hx287    rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx288    obtain ⟨y, rfl⟩ := hx289    simp only [ψ0, RingHom.comp_apply, map_mul, map_pow]290    rw [← map_pow, ← map_pow, Ideal.Quotient.eq_zero_iff_mem.mpr, zero_mul]291    rw [Ideal.span_singleton_pow, map_pow]292    exact Ideal.mem_span_singleton_self _293  let ψ := Ideal.Quotient.lift _ ψ0 hψ0294  have hψu : IsUnit (ψ (Ideal.Quotient.mk _ z)) := by295    simp only [ψ, Ideal.Quotient.lift_mk, ψ0, RingHom.comp_apply]296    exact (IsLocalization.Away.algebraMap_isUnit z).map _297  let g : Localization.Away (Ideal.Quotient.mk ((Ideal.span {e})^j) z) →+* _ :=298    IsLocalization.Away.lift (Ideal.Quotient.mk _ z) hψu299  have hg : ∀ a : A, g (algebraMap (A ⧸ (Ideal.span {e})^j) _ (Ideal.Quotient.mk _ a)) =300      Ideal.Quotient.mk _ (algebraMap A (Localization.Away z) a) :=301    fun a ↦ IsLocalization.Away.lift_eq _ hψu _302  have hgf : g.comp f = RingHom.id _ :=303    Ideal.Quotient.ringHom_ext <| IsLocalization.ringHom_ext (Submonoid.powers z) <|304      RingHom.ext fun a ↦ by simp only [RingHom.comp_apply, RingHom.id_apply, hf, hg]305  have hfg : f.comp g = RingHom.id _ :=306    IsLocalization.ringHom_ext (Submonoid.powers (Ideal.Quotient.mk ((Ideal.span {e})^j) z)) <|307      Ideal.Quotient.ringHom_ext <|308        RingHom.ext fun a ↦ by simp only [RingHom.comp_apply, RingHom.id_apply, hf, hg]309  exact ⟨RingEquiv.ofRingHom f g hfg hgf, hf⟩310 311/-- Every element of `(t, x)^j` is a homogeneous combination `∑ cᵢ t^(j-i) xⁱ` of degree-`j`312monomials. -/313theorem monomial_span_pow (R : Type) [CommRing R] (t x : R) (j : ℕ) (r : R)314    (hr : r ∈ (Ideal.span {t,x}) ^ j) :315    ∃ c : Fin (j+1) → R, r = ∑ i : Fin (j+1), c i * t^(j - i.val) * x^i.val := by316  have key : ∀ n : ℕ, (Ideal.span {t,x})^n ≤317      Ideal.span (Set.range fun i : Fin (n+1) ↦ t^(n - i.val) * x^i.val) := by318    intro n319    induction n with320    | zero => simp321    | succ n ih =>322      rw [pow_succ']323      refine (Ideal.mul_mono_right ih).trans ?_324      rw [Ideal.span_mul_span', Ideal.span_le]325      rintro _ ⟨a, ha, b, ⟨i, rfl⟩, rfl⟩326      simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha327      rcases ha with rfl | rfl328      · apply Ideal.subset_span329        refine ⟨⟨i.val, by omega⟩, ?_⟩330        have hi := i.isLt331        simp only332        rw [show n + 1 - i.val = (n - i.val) + 1 by omega, pow_succ]333        ring334      · apply Ideal.subset_span335        refine ⟨⟨i.val + 1, by omega⟩, ?_⟩336        have hi := i.isLt337        simp only338        rw [show n + 1 - (i.val + 1) = n - i.val by omega, pow_succ]339        ring340  have h := key j hr341  rw [Ideal.mem_span_range_iff_exists_fun] at h342  obtain ⟨c, hc⟩ := h343  exact ⟨c, by rw [← hc]; simp [mul_assoc]⟩344 345/-- An ideal of a fixed-tangent cell is principal, generated by a form `∑ cᵢ t^(d-i) xⁱ` whose346coefficients reduce to those of a polynomial `H` with homogeneous divisor `Dv`, and some347coefficient is a unit. -/348theorem fixed_tangent_cell_generator_coefficients (O R : Type) [CommRing O] [IsDomain O]349    [IsDiscreteValuationRing O] [CommRing R] [IsDomain R] [Algebra O R] [IsRegularLocalRing R]350    (S : SurfaceData O R) (s : State) (d : ℕ) (Dv : ExceptionalDivisor (IsLocalRing.ResidueField R))351    (J : Ideal R) (hJ : J ∈ fixedTangentCell O R S s d Dv) :352    ∃ (f : R) (c : Fin (d+1) → R) (H : Polynomial (IsLocalRing.ResidueField R)), J = Ideal.span353    {f} ∧ f = ∑ i : Fin (d+1), c i * S.t^(d - i.val) * S.x^i.val ∧ HasHomogeneousDivisor354    (IsLocalRing.ResidueField R) d H Dv ∧ (∀ i : Fin (d+1), IsLocalRing.residue R (c i) =355      H.coeff i.val) ∧ ∃ i : Fin (d+1), c i ∉ Ideal.span {S.t, S.x} := by356  obtain ⟨-, f, H, hJf, hH, hδ⟩ := hJ357  rw [← S.parameters] at hδ358  obtain ⟨c', hc'⟩ := monomial_span_pow R S.t S.x (d+1) _ hδ359  have htm : S.t ∈ IsLocalRing.maximalIdeal R := S.parameters ▸ Ideal.subset_span (by simp)360  have hxm : S.x ∈ IsLocalRing.maximalIdeal R := S.parameters ▸ Ideal.subset_span (by simp)361  have hrep : ∀ y, IsLocalRing.residue R (residueRepresentative R y) = y := fun y ↦362    Function.rightInverse_invFun IsLocalRing.residue_surjective y363  let c : Fin (d+1) → R := fun i ↦ residueRepresentative R (H.coeff i.val) + S.t * c' i.castSucc364    + (if i = Fin.last d then S.x * c' (Fin.last (d+1)) else 0)365  have hres : ∀ i : Fin (d+1), IsLocalRing.residue R (c i) = H.coeff i.val := by366    intro i367    have ht : IsLocalRing.residue R S.t = 0 := (IsLocalRing.residue_eq_zero_iff _).2 htm368    have hx : IsLocalRing.residue R S.x = 0 := (IsLocalRing.residue_eq_zero_iff _).2 hxm369    simp only [c]370    split_ifs <;> simp [map_add, map_mul, ht, hx, hrep]371  refine ⟨f, c, H, hJf, ?_, hH, hres, ?_⟩372  · have hf : f = tangentLift O R S d H + (f - tangentLift O R S d H) := by ring373    rw [hf, hc', Fin.sum_univ_castSucc, tangentLift]374    simp only [c, add_mul, Finset.sum_add_distrib]375    have h1 : (∑ i : Fin (d+1),376        c' i.castSucc * S.t ^ (d + 1 - (i.castSucc : ℕ)) * S.x ^ (i.castSucc : ℕ))377        = ∑ i : Fin (d+1), S.t * c' i.castSucc * S.t ^ (d - (i : ℕ)) * S.x ^ (i : ℕ) := by378      apply Finset.sum_congr rfl379      intro i _380      simp only [Fin.val_castSucc]381      have : d + 1 - i.val = (d - i.val) + 1 := by omega382      rw [this, pow_succ]; ring383    have h2 : (∑ i : Fin (d+1), (if i = Fin.last d then S.x * c' (Fin.last (d + 1)) else 0)384        * S.t ^ (d - (i : ℕ)) * S.x ^ (i : ℕ))385        = c' (Fin.last (d + 1)) * S.t ^ (d + 1 - ((Fin.last (d + 1) : Fin (d+2)) : ℕ))386          * S.x ^ ((Fin.last (d + 1) : Fin (d+2)) : ℕ) := by387      rw [Finset.sum_eq_single (Fin.last d)]388      · simp [pow_succ]; ring389      · intro b _ hb; simp [hb]390      · simp391    rw [h1, h2]; ring392  · refine ⟨⟨H.natDegree, by have := hH.2.1; omega⟩, ?_⟩393    rw [S.parameters, ← IsLocalRing.residue_eq_zero_iff, hres]394    simp only395    rw [Polynomial.coeff_natDegree]396    exact Polynomial.leadingCoeff_ne_zero.2 hH.1397 398/-- For `m < 0`, `P(T) = T^m · Q(T⁻¹)` in `k[T, T⁻¹]` forces `P = Q = 0`. -/399theorem negative_laurent_twist_has_no_kernel (k : Type) [CommRing k] (m : ℤ) (hm : m < 0)400    (P Q : Polynomial k) (h : P.toLaurent - LaurentPolynomial.T m *401      (LaurentPolynomial.invert (R := k) Q.toLaurent) = 0) : P = 0 ∧ Q = 0 := by402  have hc : ∀ n : ℤ, P.toLaurent.coeff n = Q.toLaurent.coeff (m - n) := by403    intro n404    have := congrArg (fun f ↦ f.coeff n) (sub_eq_zero.mp h)405    simp only [LaurentPolynomial.T, AddMonoidAlgebra.coeff_single_mul_apply, one_mul,406      LaurentPolynomial.invert_apply] at this407    rw [this]; congr 1; ring408  have hL : ∀ (f : Polynomial k) (i : ℕ), f.toLaurent.coeff (i : ℤ) = f.coeff i := by409    intro f i410    rw [LaurentPolynomial.coeff_toLaurent]411    exact Finsupp.mapDomain_apply Nat.castEmbedding.injective _ i412  have hN : ∀ (f : Polynomial k) (n : ℤ), n < 0 → f.toLaurent.coeff n = 0 := by413    intro f n hn414    rw [LaurentPolynomial.coeff_toLaurent]415    apply Finsupp.mapDomain_of_notMem_range416    rintro ⟨i, rfl⟩417    simp at hn418    omega419  constructor420  · ext i421    rw [← hL, hc, hN _ _ (by omega)]; simp422  · ext i423    have := hc (m - i)424    rw [hN _ _ (by omega), sub_sub_cancel, hL] at this425    simp [← this]426 427/-- A nonzerodivisor of `A` remains a nonzerodivisor in the localization `A[1/z]`. -/428theorem nonzerodivisor_survives_localization (A : Type) [CommRing A] (e z : A)429    (he : Function.Injective (fun a : A ↦ e*a)) :430    Function.Injective431      (fun a : Localization.Away z ↦ algebraMap A (Localization.Away z) e * a) := by432  have key : ∀ w : Localization.Away z, algebraMap A (Localization.Away z) e * w = 0 → w = 0 := by433    intro w hw434    obtain ⟨⟨a, s⟩, hs⟩ := IsLocalization.surj (Submonoid.powers z) w435    simp only at hs436    have h1 : algebraMap A (Localization.Away z) (e * a) = 0 := by437      rw [map_mul, ← hs, ← mul_assoc, hw, zero_mul]438    obtain ⟨m, hm⟩ := (IsLocalization.map_eq_zero_iff (Submonoid.powers z) _ _).1 h1439    have h2 : (m : A) * a = 0 := by440      apply he441      simp only [mul_zero]442      rw [← hm]; ring443    have h3 : algebraMap A (Localization.Away z) a = 0 :=444      (IsLocalization.map_eq_zero_iff (Submonoid.powers z) _ _).2 ⟨m, h2⟩445    rw [h3] at hs446    exact (IsLocalization.map_units (Localization.Away z) s).mul_left_eq_zero.1 hs447  exact fun x y hxy ↦ sub_eq_zero.1 (key (x - y) (by simp only at hxy; rw [mul_sub, hxy, sub_self]))448 449/-- The linear part of the normalization map, evaluated at a coordinate vector `z`, is the first450coordinate of any lift `w` of the image of `z` under the quotient map `phi`. -/451private theorem normalization_linear_part_is_quotient_matrix (O R C : Type) [CommRing O]452    [CommRing R]453    [CommRing C] [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g c : C) (n : ℕ)454    (b : Fin n → R) (bc : Fin n → C) (E : C ≃ₗ[O] ((Fin n → O) × C))455    (hE : ∀ w, E.symm w = divisionMap g bc w)456    (phi : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}))457    (hphi : ∀ h : R, phi (Ideal.Quotient.mk (Ideal.span {f}) h) =458      Ideal.Quotient.mk (Ideal.span {g}) (c * alpha h)) (z : Fin n → O) (w : C)459    (hw : Ideal.Quotient.mk (Ideal.span {g}) w =460      phi (Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z))) :461    normalizationLinearPart E (pulledVariation alpha c b) z = (E w).1 := by462  have hlin : coordinateLinear b z = coordinateLift b z := by463    simp [coordinateLinear, coordinateLift]464  have hH : pulledVariation alpha c b z = c * alpha (coordinateLift b z) := by465    simp [pulledVariation, hlin]466  rw [hphi, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at hw467  obtain ⟨v, hv⟩ := hw468  have hw' : w = c * alpha (coordinateLift b z) + g * v := by rw [mul_comm g, hv]; ring469  have hgv : E (g * v) = (0, v) := by470    apply E.symm.injective471    rw [LinearEquiv.symm_apply_apply, hE]472    simp [divisionMap, coordinateLift]473  simp only [normalizationLinearPart, LinearMap.comp_apply, LinearMap.fst_apply,474    LinearEquiv.coe_coe, hH, hw', map_add, hgv, Prod.fst_add, add_zero]475 476/-- The cokernel of the linear part of the normalization map has the same `O`-length as the cokernel477of the quotient map `phi`, and it is injective whenever `phi` is. -/478theorem normalization_linear_part_cokernel_length_eq (O R C : Type) [CommRing O] [CommRing R]479    [CommRing C] [Algebra O R] [Algebra O C] (alpha : R →ₐ[O] C) (f : R) (g e c : C) (d : ℕ)480    (_hf : alpha f = e ^ d * g) (n : ℕ) (pi : O) (s : ℕ)481    (_hpi : (algebraMap O C pi) ^ s = e ^ d * c)482    (b : Fin n → R) (bc : Fin n → C) (E : C ≃ₗ[O] ((Fin n → O) × C))483    (hE : ∀ w, E.symm w = divisionMap g bc w)484    (phi : (R ⧸ Ideal.span {f}) →ₗ[O] (C ⧸ Ideal.span {g}))485    (hphi : ∀ h : R, phi (Ideal.Quotient.mk (Ideal.span {f}) h) =486      Ideal.Quotient.mk (Ideal.span {g}) (c * alpha h))487    (EB : (R ⧸ Ideal.span {f}) ≃ₗ[O] (Fin n → O))488    (hEB : ∀ z : Fin n → O, EB.symm z = Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z)) :489    Module.length O ((Fin n → O) ⧸ LinearMap.range490      (normalizationLinearPart E (pulledVariation alpha c b))) = Module.length O491    ((C ⧸ Ideal.span {g}) ⧸ LinearMap.range phi) ∧492    (Function.Injective phi → Function.Injective493      (normalizationLinearPart E (pulledVariation alpha c b))) := by494  obtain ⟨EC, hEC⟩ := division_equiv_child_coordinates O C n g bc E hE495  have hD : ∀ z, normalizationLinearPart E (pulledVariation alpha c b) z496      = EC (phi (EB.symm z)) := by497    intro z498    obtain ⟨w, hw⟩ := Ideal.Quotient.mk_surjective499      (phi (Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z)))500    rw [normalization_linear_part_is_quotient_matrix O R C alpha f g c n501      b bc E hE phi hphi z w hw, ← hEC, hw, hEB]502  have hcomp : normalizationLinearPart E (pulledVariation alpha c b)503      = (EC.toLinearMap ∘ₗ phi) ∘ₗ EB.symm.toLinearMap := by504    ext z; simp [hD]505  have hrange : LinearMap.range (normalizationLinearPart E (pulledVariation alpha c b))506      = (LinearMap.range phi).map EC.toLinearMap := by507    rw [hcomp, LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range EB.symm),508      LinearMap.range_comp]509  refine ⟨?_, fun h ↦ ?_⟩510  · exact (Submodule.Quotient.equiv _ _ EC.symm.symm hrange.symm).length_eq.symm511  · rw [hcomp]512    exact (EC.injective.comp h).comp EB.symm.injective513 514/-- The opposite chart maps into the overlap, compatibly with the base and sending its slope to the515inverse of the slope. -/516private theorem opposite_untruncated_chart_restriction (R : Type) [CommRing R] (t x : R) :517    ∃ beta : (BlowupChart R x t) →+* (BlowupOverlap R t x),518    (∀ r : R, beta (chartBase R x t r) = (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))519      (chartBase R t x r)) ∧ beta (chartSlope R x t) = IsLocalization.Away.invSelf520    (chartSlope R t x) := by521  set a : R →+* BlowupOverlap R t x :=522    (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)).comp (chartBase R t x) with ha523  have hrel := blowup_chart_relation R t x524  have hinv := IsLocalization.Away.mul_invSelf (S := BlowupOverlap R t x) (chartSlope R t x)525  have hz : a x * IsLocalization.Away.invSelf (chartSlope R t x) = a t := by526    simp only [ha, RingHom.comp_apply, ← hrel, map_mul]527    rw [mul_assoc, hinv, mul_one]528  obtain ⟨psi, h1, h2⟩ := blowup_chart_universal R (BlowupOverlap R t x) x t a529    (IsLocalization.Away.invSelf (chartSlope R t x)) hz530  exact ⟨psi, fun r ↦ by rw [h1]; rfl, h2⟩531 532/-- A blow-up restriction (the gluing map of the opposite chart into the overlap) exists. -/533theorem actual_blowup_restriction_exists (R : Type) [CommRing R] (t x : R) :534    Nonempty (BlowupRestriction R t x) := by535  obtain ⟨beta, hbase, hslope⟩ := opposite_untruncated_chart_restriction R t x536  have hc : ∀ r : R, beta (algebraMap R (BlowupChart R x t) r) =537      algebraMap R (BlowupOverlap R t x) r := by538    intro r539    have h1 : algebraMap R (BlowupChart R x t) r = chartBase R x t r := rfl540    have h2 : algebraMap R (BlowupOverlap R t x) r =541        algebraMap (BlowupChart R t x) (BlowupOverlap R t x) (chartBase R t x r) := by542      rw [IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x)]543      rfl544    rw [h1, h2, hbase]545  exact ⟨{ right := { beta with commutes' := hc }, slope := hslope }⟩546 547/-- The overlaps of the two charts are isomorphic, compatibly with the base maps and exchanging the548slope with its inverse. -/549private theorem blowup_overlap_symmetry (R : Type) [CommRing R] (t x : R) :550    ∃ e : BlowupOverlap R x t ≃+* BlowupOverlap R t x,551    (∀ r : R, e ((algebraMap (BlowupChart R x t) (BlowupOverlap R x t)) (chartBase R x t r)) =552      (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x r)) ∧ e553    ((algebraMap (BlowupChart R x t) (BlowupOverlap R x t)) (chartSlope R x t)) =554    IsLocalization.Away.invSelf (chartSlope R t x) := by555  obtain ⟨b1, hb1, hs1⟩ := opposite_untruncated_chart_restriction R t x556  obtain ⟨b2, hb2, hs2⟩ := opposite_untruncated_chart_restriction R x t557  have u1 : IsUnit (b1 (chartSlope R x t)) := by558    rw [hs1]559    exact IsUnit.of_mul_eq_one_right _ (IsLocalization.Away.mul_invSelf (chartSlope R t x))560  have u2 : IsUnit (b2 (chartSlope R t x)) := by561    rw [hs2]562    exact IsUnit.of_mul_eq_one_right _ (IsLocalization.Away.mul_invSelf (chartSlope R x t))563  let e1 : BlowupOverlap R x t →+* BlowupOverlap R t x :=564    IsLocalization.Away.lift (chartSlope R x t) u1565  let e2 : BlowupOverlap R t x →+* BlowupOverlap R x t :=566    IsLocalization.Away.lift (chartSlope R t x) u2567  have he1 : ∀ a, e1 (algebraMap _ _ a) = b1 a := fun a ↦568    IsLocalization.Away.lift_eq (chartSlope R x t) u1 a569  have he2 : ∀ a, e2 (algebraMap _ _ a) = b2 a := fun a ↦570    IsLocalization.Away.lift_eq (chartSlope R t x) u2 a571  have inv_map : ∀ {S T : Type} [CommRing S] [CommRing T] (s : S)572      (f : Localization.Away s →+* T) (w : T),573      f (algebraMap S _ s) * w = 1 →574      f (IsLocalization.Away.invSelf s) = w := by575    intro S T _ _ s f w hw576    have h1 : f (algebraMap S _ s) * f (IsLocalization.Away.invSelf s) = 1 := by577      rw [← map_mul, IsLocalization.Away.mul_invSelf, map_one]578    linear_combination w * h1 - f (IsLocalization.Away.invSelf s) * hw579  have h21 : e2.comp e1 = RingHom.id _ := by580    apply IsLocalization.ringHom_ext (Submonoid.powers (chartSlope R x t))581    apply blowup_chart_ringHom_ext582    · exact fun r ↦ by simp only [RingHom.comp_apply, RingHom.id_apply, he1, hb1, he2, hb2]583    · simp only [RingHom.comp_apply, RingHom.id_apply, he1, hs1]584      exact inv_map _ _ _ (by rw [he2, hs2, mul_comm, IsLocalization.Away.mul_invSelf])585  have h12 : e1.comp e2 = RingHom.id _ := by586    apply IsLocalization.ringHom_ext (Submonoid.powers (chartSlope R t x))587    apply blowup_chart_ringHom_ext588    · exact fun r ↦ by simp only [RingHom.comp_apply, RingHom.id_apply, he1, hb1, he2, hb2]589    · simp only [RingHom.comp_apply, RingHom.id_apply, he2, hs2]590      exact inv_map _ _ _ (by rw [he1, hs1, mul_comm, IsLocalization.Away.mul_invSelf])591  exact ⟨RingEquiv.ofRingHom e1 e2 h12 h21, fun r ↦ (he1 _).trans (hb1 r), (he1 _).trans hs1⟩592 593/-- Via the gluing map, the overlap is the localization of the opposite chart away from its594slope. -/595theorem blowup_overlap_isLocalization_right (R : Type) [CommRing R] (t x : R)596    (beta : BlowupRestriction R t x) :597    @IsLocalization.Away (BlowupChart R x t) _ (chartSlope R x t)598    (BlowupOverlap R t x) _ beta.right.toRingHom.toAlgebra := by599  obtain ⟨e, he1, he2⟩ := blowup_overlap_symmetry R t x600  have h : e.toRingHom.comp (algebraMap (BlowupChart R x t) (BlowupOverlap R x t)) =601      beta.right.toRingHom := by602    apply blowup_chart_ringHom_ext R (BlowupOverlap R t x) x t603    · intro r604      have h1 : e ((algebraMap (BlowupChart R x t) (BlowupOverlap R x t)) (chartBase R x t r)) =605          algebraMap R (BlowupOverlap R t x) r := by606        rw [he1]607        exact (IsScalarTower.algebraMap_apply R (BlowupChart R t x) (BlowupOverlap R t x) r).symm608      have h2 : beta.right (chartBase R x t r) = algebraMap R (BlowupOverlap R t x) r :=609        beta.right.commutes r610      exact h1.trans h2.symm611    · exact he2.trans beta.slope.symm612  have key :=613    (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers (chartSlope R x t)) e).mp614    (inferInstance : IsLocalization.Away (chartSlope R x t) (BlowupOverlap R x t))615  rw [← h]616  exact key617 618/-- A maximal ideal of a localization `B` of the chart away from the slope, whose contraction619contains the exceptional parameter `t`, contracts to a maximal ideal of the chart. -/620private theorem comap_isMaximal_of_exceptional (R : Type) [CommRing R] (t x : R)621    [(Ideal.span ({t,x} : Set R)).IsMaximal] (B : Type) [CommRing B] [Algebra (BlowupChart R t x) B]622    [IsLocalization.Away (chartSlope R t x) B] (Q : Ideal B) [Q.IsMaximal]623    (htP : chartBase R t x t ∈ Q.comap (algebraMap (BlowupChart R t x) B)) :624    (Q.comap (algebraMap (BlowupChart R t x) B)).IsMaximal := by625  set P := Q.comap (algebraMap (BlowupChart R t x) B)626  let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _627  obtain ⟨e0, hC, hX⟩ := exceptional_chart_is_affine_line R t x628  let ψ : BlowupChart R t x →+* Polynomial (R ⧸ Ideal.span ({t,x} : Set R)) :=629    e0.toRingHom.comp (Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1))630  have hψs : Function.Surjective ψ :=631    e0.surjective.comp Ideal.Quotient.mk_surjective632  have hψZ : ψ (chartSlope R t x) = Polynomial.X := hX633  have hker : RingHom.ker ψ ≤ P := fun a ha ↦ by634    have h1 : e0 (Ideal.Quotient.mk (exceptionalLevelIdeal R t x 1) a) = 0 := ha635    rw [map_eq_zero_iff _ e0.injective, Ideal.Quotient.eq_zero_iff_mem, exceptionalLevelIdeal,636      pow_one] at h1637    exact (Ideal.span_le.mpr (by simpa using htP)) h1638  have hmapP : (P.map ψ).IsPrime := Ideal.map_isPrime_of_surjective hψs hker639  rw [← sup_eq_left.mpr hker, ← Ideal.comap_map_of_surjective' ψ hψs P]640  have key : ∃ f ∈ P.map ψ, f ≠ 0 := by641    by_cases h1 : chartSlope R t x - 1 ∈ P642    · refine ⟨ψ (chartSlope R t x - 1), Ideal.mem_map_of_mem _ h1, ?_⟩643      rw [map_sub, map_one, hψZ]644      exact Polynomial.X_sub_C_ne_zero 1645    · obtain ⟨y, i, hi, hy⟩ := Ideal.IsMaximal.exists_inv (inferInstance : Q.IsMaximal) h1646      obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (chartSlope R t x)) y647      have hg : a * (chartSlope R t x - 1) - (s : BlowupChart R t x) ∈ P := by648        change algebraMap (BlowupChart R t x) B _ ∈ Q649        have hs := IsLocalization.mk'_spec B a s650        have : algebraMap (BlowupChart R t x) B651            (a * (chartSlope R t x - 1) - (s : BlowupChart R t x))652            = - (algebraMap (BlowupChart R t x) B s * i) := by653          rw [map_sub, map_mul, ← hs]654          linear_combination (algebraMap (BlowupChart R t x) B s) * hy655        rw [this]656        exact Q.neg_mem_iff.mpr (Q.mul_mem_left _ hi)657      refine ⟨_, Ideal.mem_map_of_mem _ hg, ?_⟩658      obtain ⟨n, hn⟩ := s.2659      intro h0660      have := congrArg (Polynomial.eval 1) h0661      rw [map_sub, map_mul, ← hn, map_pow, map_sub, map_one, hψZ] at this662      simp at this663  obtain ⟨f, hf, hf0⟩ := key664  have : (P.map ψ).IsMaximal :=665    IsPrime.to_maximal_ideal fun hbot ↦ hf0 (by rwa [hbot, Ideal.mem_bot] at hf)666  exact Ideal.comap_isMaximal_of_surjective _ hψs667 668/-- A maximal ideal of the overlap containing the exceptional parameter contracts to a maximal ideal669of the chart that contains `t` but not the slope. -/670theorem overlap_exceptional_point_comap_maximal (R : Type) [CommRing R] (t x : R)671    [(Ideal.span ({t,x} : Set R)).IsMaximal] (Q : Ideal (BlowupOverlap R t x)) [Q.IsMaximal]672    (hQ : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t) ∈ Q) :673    (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).IsMaximal ∧674    chartSlope R t x ∉ Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) ∧675    chartBase R t x t ∈ Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) := by676  exact ⟨comap_isMaximal_of_exceptional R t x _ Q hQ, fun h ↦ Ideal.IsMaximal.ne_top ‹_›677    (Ideal.eq_top_of_isUnit_mem Q h (IsLocalization.Away.algebraMap_isUnit _)), hQ⟩678 679/-- A maximal ideal of the overlap containing the exceptional parameter contracts, along the gluing680map, to a maximal ideal of the opposite chart that contains `x` but not its slope. -/681theorem overlap_exceptional_point_comap_maximal_right (R : Type) [CommRing R] (t x : R)682    [(Ideal.span ({t,x} : Set R)).IsMaximal] (beta : BlowupRestriction R t x)683    (Q : Ideal (BlowupOverlap R t x)) [Q.IsMaximal]684    (hQ : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t) ∈ Q) :685    (Q.comap beta.right.toRingHom).IsMaximal ∧ chartSlope R x t ∉ Q.comap beta.right.toRingHom ∧686    chartBase R x t x ∈ Q.comap beta.right.toRingHom := by687  set P := Q.comap beta.right.toRingHom with hPdef688  have htP : chartBase R x t x ∈ P := by689    change beta.right (chartBase R x t x) ∈ Q690    rw [show beta.right (chartBase R x t x) = algebraMap R (BlowupOverlap R t x) x from691      beta.right.commutes x, IsScalarTower.algebraMap_apply R (BlowupChart R t x),692      show algebraMap R (BlowupChart R t x) x = chartBase R t x t * chartSlope R t x from693      (blowup_chart_relation R t x).symm, map_mul]694    exact Q.mul_mem_right _ hQ695  have hZP : chartSlope R x t ∉ P := fun h ↦ by696    have h' : beta.right (chartSlope R x t) ∈ Q := h697    rw [beta.slope] at h'698    exact Ideal.IsMaximal.ne_top ‹_› (Ideal.eq_top_of_isUnit_mem Q h'699      (.of_mul_eq_one_right _ (IsLocalization.Away.mul_invSelf (chartSlope R t x))))700  refine ⟨?_, hZP, htP⟩701  let _ := beta.right.toRingHom.toAlgebra702  have := blowup_overlap_isLocalization_right R t x beta703  have : (Ideal.span ({x,t} : Set R)).IsMaximal := by rw [Set.pair_comm]; infer_instance704  exact comap_isMaximal_of_exceptional R x t (BlowupOverlap R t x) Q htP705 706private theorem localizationAway_quotient_congr {S : Type} [CommRing S] (I J : Ideal S) (h : I = J)707    (z : S) :708    ∃ F : Localization.Away (Ideal.Quotient.mk I z) ≃+* Localization.Away709    (Ideal.Quotient.mk J z), ∀ a : S, F (algebraMap _ _ (Ideal.Quotient.mk I a)) = algebraMap _ _710    (Ideal.Quotient.mk J a) := by711  subst h; exact ⟨RingEquiv.refl _, fun _ ↦ rfl⟩712 713/-- The exceptional divisor of the overlap is the Laurent line `k[Z, Z⁻¹]` over the residue field714`k = R/(t, x)`, with constants coming from `R` and the slope going to `Z`. -/715private theorem overlap_exceptional_quotient_equiv_laurent (R : Type) [CommRing R] (t x : R) :716    ∃ E : BlowupOverlap R t x ⧸ Ideal.span {overlapException R t x} ≃+*717      LaurentPolynomial (R ⧸ Ideal.span ({t,x} : Set R)),718      (∀ r : R, E (Ideal.Quotient.mk _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)719        (chartBase R t x r))) = LaurentPolynomial.C (Ideal.Quotient.mk _ r)) ∧720      E (Ideal.Quotient.mk _ (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)721        (chartSlope R t x))) = LaurentPolynomial.T 1 := by722  set A := BlowupChart R t x723  set C := BlowupOverlap R t x724  obtain ⟨L, hL⟩ :=725    localization_principal_quotient_commute A (chartBase R t x t) (chartSlope R t x) 1726  have hI : (Ideal.span {chartBase R t x t})^1 = exceptionalLevelIdeal R t x 1 := by727    simp [exceptionalLevelIdeal]728  obtain ⟨F, hF⟩ := localizationAway_quotient_congr _ _ hI (chartSlope R t x)729  obtain ⟨E0, hE0C, hE0T⟩ := exceptional_overlap_is_laurent_line R t x730  have hJ : Ideal.span {overlapException R t x} =731      (Ideal.span {algebraMap A C (chartBase R t x t)})^1 := by732    simp [overlapException, A, C]733  let E := ((Ideal.quotEquivOfEq hJ).trans L).trans (F.trans E0)734  have hE : ∀ a : A, E (Ideal.Quotient.mk _ (algebraMap A C a)) =735      E0 (levelOverlapMap R t x 1 (Ideal.Quotient.mk _ a)) := by736    intro a737    simp only [E, RingEquiv.trans_apply, Ideal.quotEquivOfEq_mk]738    rw [hL]; exact congrArg E0 (hF a)739  exact ⟨E, fun r ↦ (hE _).trans (hE0C r), (hE _).trans hE0T⟩740 741/-- The exceptional divisor of the overlap is integral, and an element of the opposite chart742vanishing on it lies in the exceptional ideal `(x)` of that chart. -/743theorem overlap_exceptional_quotient_domain (R : Type) [CommRing R] (t x : R)744    [(Ideal.span ({t,x} : Set R)).IsMaximal] (_hreg : RegularParameterPair R t x)745    (beta : BlowupRestriction R t x) :746    IsDomain (BlowupOverlap R t x ⧸ Ideal.span {overlapException R t x}) ∧ ∀ b : BlowupChart R x t,747    Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right b) = 0 → b ∈ Ideal.span748    {chartBase R x t x} := by749  -- Both exceptional curves are identified with (open subsets of) `ℙ¹_k`: the overlap one with750  -- `k[Z, Z⁻¹]`, the chart one with `k[W]`, and the gluing becomes `W ↦ Z⁻¹`, which is injective.751  set A := BlowupChart R t x752  set C := BlowupOverlap R t x753  set k := R ⧸ Ideal.span ({t,x} : Set R)754  set e' := overlapException R t x755  obtain ⟨E, hEC, hET⟩ := overlap_exceptional_quotient_equiv_laurent R t x756  refine ⟨MulEquiv.isDomain _ E.toMulEquiv, fun b hb ↦ ?_⟩757  obtain ⟨P, hPC, hPX⟩ := exceptional_chart_is_affine_line R x t758  have hK : Ideal.span ({t,x} : Set R) = Ideal.span ({x,t} : Set R) := by rw [Set.pair_comm]759  let κ : k ≃+* (R ⧸ Ideal.span ({x,t} : Set R)) := Ideal.quotEquivOfEq hK760  have hbase : ∀ r : R, beta.right (chartBase R x t r) = algebraMap A C (chartBase R t x r) := by761    intro r762    have h1 : chartBase R x t r = algebraMap R (BlowupChart R x t) r := rfl763    rw [h1, beta.right.commutes, IsScalarTower.algebraMap_apply R A C]; rfl764  have hx : beta.right (chartBase R x t x) ∈ Ideal.span {e'} := by765    rw [hbase, ← blowup_chart_relation, map_mul, Ideal.mem_span_singleton]766    exact ⟨_, rfl⟩767  let f0 : BlowupChart R x t →+* C ⧸ Ideal.span {e'} :=768    (Ideal.Quotient.mk (Ideal.span {e'})).comp beta.right.toRingHom769  have hlift : ∀ a ∈ exceptionalLevelIdeal R x t 1, f0 a = 0 := by770    intro a ha771    simp only [exceptionalLevelIdeal, pow_one, Ideal.mem_span_singleton] at ha772    obtain ⟨c, rfl⟩ := ha773    simp only [f0, RingHom.comp_apply, map_mul, AlgHom.toRingHom_eq_coe, RingHom.coe_coe]774    rw [Ideal.Quotient.eq_zero_iff_mem.mpr hx, zero_mul]775  let g : ExceptionalChartLevel R x t 1 →+* LaurentPolynomial k :=776    E.toRingHom.comp (Ideal.Quotient.lift _ f0 hlift)777  have key : (g.comp P.symm.toRingHom).comp (Polynomial.mapRingHom κ.toRingHom) =778      (LaurentPolynomial.invert :779        LaurentPolynomial k ≃ₐ[k] LaurentPolynomial k).toRingEquiv.toRingHom.comp780        Polynomial.toLaurent := by781    have hg : ∀ a : BlowupChart R x t,782        g (Ideal.Quotient.mk _ a) = E (Ideal.Quotient.mk _ (beta.right a)) := fun a ↦ rfl783    apply Polynomial.ringHom_ext784    · intro a785      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective a786      have h1 : P.symm (Polynomial.C (Ideal.Quotient.mk (Ideal.span ({x,t} : Set R)) r)) =787          levelBase R x t 1 r := by788        rw [RingEquiv.symm_apply_eq, hPC]789      simp only [RingHom.comp_apply, Polynomial.coe_mapRingHom, Polynomial.map_C,790        RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, κ,791        Polynomial.toLaurent_C, AlgEquiv.coe_ringEquiv, LaurentPolynomial.invert_C]792      have h2 : levelBase R x t 1 r = Ideal.Quotient.mk _ (chartBase R x t r) := rfl793      rw [Ideal.quotEquivOfEq_mk, h1, h2, hg, hbase]794      exact hEC r795    · have h1 : P.symm Polynomial.X = levelSlope R x t 1 := by796        rw [RingEquiv.symm_apply_eq, hPX]797      simp only [RingHom.comp_apply, Polynomial.coe_mapRingHom, Polynomial.map_X,798        RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, h1,799        Polynomial.toLaurent_X, AlgEquiv.coe_ringEquiv, LaurentPolynomial.invert_T]800      have h2 : levelSlope R x t 1 = Ideal.Quotient.mk _ (chartSlope R x t) := rfl801      rw [h2, hg, beta.slope]802      have hm : LaurentPolynomial.T 1 *803          E (Ideal.Quotient.mk _ (IsLocalization.Away.invSelf (chartSlope R t x) : C)) = 1 := by804        rw [← hET, ← map_mul, ← map_mul, IsLocalization.Away.mul_invSelf, map_one, map_one]805      exact (left_inv_eq_right_inv (by rw [← LaurentPolynomial.T_add]; simp) hm).symm806  have hb0 : g (Ideal.Quotient.mk _ b) = 0 := by807    simp only [g, f0, RingHom.comp_apply, Ideal.Quotient.lift_mk, AlgHom.toRingHom_eq_coe,808      RingHom.coe_coe, hb, map_zero]809  set p := Polynomial.mapRingHom κ.symm.toRingHom (P (Ideal.Quotient.mk _ b))810  have hmm : (Polynomial.mapRingHom κ.toRingHom) p = P (Ideal.Quotient.mk _ b) := by811    simp only [p, Polynomial.coe_mapRingHom, Polynomial.map_map]812    convert Polynomial.map_id813    ext a; simp814  have hp : p = 0 := by815    have := congrArg (fun h ↦ h p) key816    simp only [RingHom.comp_apply] at this817    rw [hmm] at this818    simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, RingEquiv.symm_apply_apply,819      hb0] at this820    rwa [eq_comm, map_eq_zero_iff _ (LaurentPolynomial.invert.toRingEquiv).injective,821      map_eq_zero_iff _ Polynomial.toLaurent_injective] at this822  have hq : Ideal.Quotient.mk (exceptionalLevelIdeal R x t 1) b = 0 :=823    P.injective (by rw [map_zero, ← hmm, hp, map_zero])824  rw [Ideal.Quotient.eq_zero_iff_mem] at hq825  simpa [exceptionalLevelIdeal] using hq826 827private theorem quotientMap_surjective_of_away {A C : Type} [CommRing A] [CommRing C] (f : A →+* C)828    (s : A) (hsurj : ∀ c : C, ∃ a : A, ∃ n : ℕ, c * f s ^ n = f a) (Q : Ideal C)829    (hP : (Q.comap f).IsMaximal) (hs : s ∉ Q.comap f) :830    Function.Surjective (Ideal.quotientMap Q f le_rfl) := by831  intro c'832  obtain ⟨c, rfl⟩ := Ideal.Quotient.mk_surjective c'833  obtain ⟨a, n, hc⟩ := hsurj c834  have hs' : Ideal.Quotient.mk (Q.comap f) (s ^ n) ≠ 0 := by835    rw [Ne, Ideal.Quotient.eq_zero_iff_mem]836    exact fun h ↦ hs (hP.isPrime.mem_of_pow_mem n h)837  let _ := Ideal.Quotient.field (Q.comap f)838  obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (Ideal.Quotient.mk (Q.comap f) (s ^ n))⁻¹839  have h1 : Ideal.Quotient.mk (Q.comap f) (u * s ^ n) = 1 := by840    rw [map_mul, hu, inv_mul_cancel₀ hs']841  have h2 : u * s ^ n - 1 ∈ Q.comap f := by842    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, h1, map_one, sub_self]843  refine ⟨Ideal.Quotient.mk _ (a * u), ?_⟩844  rw [Ideal.quotientMap_mk, Ideal.Quotient.eq]845  have : f (a * u) - c = c * f (u * s ^ n - 1) := by846    rw [map_mul, ← hc, map_sub, map_mul, map_pow, map_one]; ring847  rw [this]848  exact Q.mul_mem_left _ h2849 850/-- At a maximal ideal of the overlap on the exceptional divisor, both charts have the same residue851field as the overlap, and hence the same residue length over `R`. -/852theorem overlap_point_residue_field_equiv (R : Type) [CommRing R] (t x : R)853    [(Ideal.span ({t,x} : Set R)).IsMaximal] (beta : BlowupRestriction R t x)854    (Q : Ideal (BlowupOverlap R t x)) [Q.IsMaximal]855    (hQ : (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (chartBase R t x t) ∈ Q) :856    (∃ φ : (BlowupChart R t x ⧸ Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) ≃+*857      (BlowupOverlap R t x ⧸ Q), ∀ a : BlowupChart R t x,858      φ (Ideal.Quotient.mk (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) a) =859      Ideal.Quotient.mk Q ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a)) ∧860    (∃ ψ : (BlowupChart R x t ⧸ Q.comap beta.right.toRingHom) ≃+* (BlowupOverlap R t x ⧸ Q),861      ∀ b : BlowupChart R x t, ψ (Ideal.Quotient.mk (Q.comap beta.right.toRingHom) b) =862      Ideal.Quotient.mk Q (beta.right b)) ∧ Module.length R863    (BlowupChart R t x ⧸ Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) =864    Module.length R (BlowupChart R x t ⧸ Q.comap beta.right.toRingHom) := by865  obtain ⟨hPl, hsl, -⟩ := overlap_exceptional_point_comap_maximal R t x Q hQ866  obtain ⟨hPr, hsr, -⟩ :=867    overlap_exceptional_point_comap_maximal_right R t x beta Q hQ868  set fl := algebraMap (BlowupChart R t x) (BlowupOverlap R t x) with hfl869  set fr := beta.right.toRingHom with hfr870  have surjl : ∀ c : BlowupOverlap R t x, ∃ a, ∃ n : ℕ, c * fl (chartSlope R t x) ^ n = fl a := by871    intro c872    obtain ⟨⟨a, ⟨_, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers (chartSlope R t x)) c873    exact ⟨a, n, by simpa [map_pow] using h⟩874  have surjr : ∀ c : BlowupOverlap R t x, ∃ a, ∃ n : ℕ, c * fr (chartSlope R x t) ^ n = fr a := by875    intro c876    let _ := fr.toAlgebra877    have := blowup_overlap_isLocalization_right R t x beta878    obtain ⟨⟨a, ⟨_, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers (chartSlope R x t)) c879    exact ⟨a, n, by simpa [map_pow, RingHom.algebraMap_toAlgebra] using h⟩880  let φ := RingEquiv.ofBijective (Ideal.quotientMap Q fl le_rfl)881    ⟨Ideal.quotientMap_injective, quotientMap_surjective_of_away fl _ surjl Q hPl hsl⟩882  let ψ := RingEquiv.ofBijective (Ideal.quotientMap Q fr le_rfl)883    ⟨Ideal.quotientMap_injective, quotientMap_surjective_of_away fr _ surjr Q hPr hsr⟩884  have hφ : ∀ a, φ (Ideal.Quotient.mk _ a) = Ideal.Quotient.mk Q (fl a) := fun a ↦ rfl885  have hψ : ∀ b, ψ (Ideal.Quotient.mk _ b) = Ideal.Quotient.mk Q (fr b) := fun b ↦ rfl886  refine ⟨⟨φ, hφ⟩, ⟨ψ, hψ⟩, ?_⟩887  rw [(AlgEquiv.ofRingEquiv (R := R) (f := φ) fun r ↦ congrArg (Ideal.Quotient.mk Q)888      (IsScalarTower.algebraMap_apply R _ _ r).symm).toLinearEquiv.length_eq,889    (AlgEquiv.ofRingEquiv (R := R) (f := ψ) fun r ↦ congrArg (Ideal.Quotient.mk Q)890      (beta.right.commutes r)).toLinearEquiv.length_eq]891 892/-- At a prime of the overlap, the local ring of the overlap is the local ring of the chart at the893contracted prime. -/894private theorem overlap_prime_localization_left (R : Type) [CommRing R] (t x : R)895    (Q : Ideal (BlowupOverlap R t x)) [Q.IsPrime] :896    ∃ φ : Localization.AtPrime Q ≃+* Localization.AtPrime897    (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))), ∀ a : BlowupChart R t x, φ898    (algebraMap (BlowupOverlap R t x) (Localization.AtPrime Q)899      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a)) = algebraMap (BlowupChart R t x)900    (Localization.AtPrime (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))) a := by901  let e := IsLocalization.localizationLocalizationAtPrimeIsoLocalization902    (Submonoid.powers (chartSlope R t x)) Q903  refine ⟨e.symm.toRingEquiv, fun a ↦ ?_⟩904  have h := e.symm.commutes a905  simp [← IsScalarTower.algebraMap_apply] at h ⊢906 907/-- At a prime of the overlap, the completed local ring of the overlap is the completed local ring908of the chart at the contracted prime. -/909theorem completed_point_transport_left (R : Type) [CommRing R] (t x : R)910    [IsNoetherianRing (BlowupChart R t x)] (Q : Ideal (BlowupOverlap R t x)) [Q.IsPrime] :911    ∃ Φ : CompletedLocalAt (BlowupOverlap R t x) Q ≃+* CompletedLocalAt (BlowupChart R t x)912    (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))), ∀ a : BlowupChart R t x, Φ913    (completedPointMap (BlowupOverlap R t x) Q914      ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) a)) = completedPointMap915    (BlowupChart R t x) (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))) a := by916  obtain ⟨φ, hφ⟩ := overlap_prime_localization_left R t x Q917  have : IsNoetherianRing (BlowupOverlap R t x) :=918    IsLocalization.isNoetherianRing (Submonoid.powers (chartSlope R t x)) _ inferInstance919  have : IsNoetherianRing (Localization.AtPrime Q) :=920    IsLocalization.isNoetherianRing Q.primeCompl _ inferInstance921  have : IsNoetherianRing (Localization.AtPrime922      (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))) :=923    IsLocalization.isNoetherianRing924      (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x))).primeCompl _ inferInstance925  obtain ⟨Φ, hΦ⟩ := local_completion_transport (Localization.AtPrime Q)926    (Localization.AtPrime (Q.comap (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)))) φ927  refine ⟨Φ, fun a ↦ ?_⟩928  simp only [completedPointMap, RingHom.comp_apply]929  rw [hΦ, hφ]930 931/-- At a prime of the overlap, the local ring of the overlap is the local ring of the opposite chart932at the prime contracted along the gluing map. -/933private theorem overlap_prime_localization_right (R : Type) [CommRing R] (t x : R)934    (beta : BlowupRestriction R t x) (Q : Ideal (BlowupOverlap R t x)) [Q.IsPrime] :935    ∃ ψ : Localization.AtPrime Q ≃+* Localization.AtPrime936    (Q.comap beta.right.toRingHom), ∀ b : BlowupChart R x t, ψ937    (algebraMap (BlowupOverlap R t x) (Localization.AtPrime Q) (beta.right b)) = algebraMap938    (BlowupChart R x t) (Localization.AtPrime (Q.comap beta.right.toRingHom)) b := by939  let _ : Algebra (BlowupChart R x t) (BlowupOverlap R t x) := beta.right.toRingHom.toAlgebra940  have _ := blowup_overlap_isLocalization_right R t x beta941  have _ : IsScalarTower (BlowupChart R x t) (BlowupOverlap R t x) (Localization.AtPrime Q) :=942    inferInstance943  have hL : IsLocalization.AtPrime (Localization.AtPrime Q)944      (Q.comap (algebraMap (BlowupChart R x t) (BlowupOverlap R t x))) :=945    IsLocalization.isLocalization_isLocalization_atPrime_isLocalization946      (Submonoid.powers (chartSlope R x t)) (Localization.AtPrime Q) Q947  let e := IsLocalization.algEquiv948    (Q.comap (algebraMap (BlowupChart R x t) (BlowupOverlap R t x))).primeCompl949    (Localization.AtPrime (Q.comap beta.right.toRingHom)) (Localization.AtPrime Q)950  refine ⟨e.symm.toRingEquiv, fun b ↦ ?_⟩951  exact e.symm.commutes b952 953/-- At a prime of the overlap, the completed local ring of the overlap is the completed local ring954of the opposite chart at the prime contracted along the gluing map. -/955theorem completed_point_transport_right (R : Type) [CommRing R] (t x : R)956    [IsNoetherianRing (BlowupChart R x t)] (beta : BlowupRestriction R t x)957    (Q : Ideal (BlowupOverlap R t x)) [Q.IsPrime] :958    ∃ Ψ : CompletedLocalAt (BlowupOverlap R t x) Q ≃+* CompletedLocalAt (BlowupChart R x t)959    (Q.comap beta.right.toRingHom), ∀ b : BlowupChart R x t, Ψ960    (completedPointMap (BlowupOverlap R t x) Q (beta.right b)) = completedPointMap961    (BlowupChart R x t) (Q.comap beta.right.toRingHom) b := by962  obtain ⟨φ, hφ⟩ := overlap_prime_localization_right R t x beta Q963  have hloc := blowup_overlap_isLocalization_right R t x beta964  have : IsNoetherianRing (BlowupOverlap R t x) := by965    let : Algebra (BlowupChart R x t) (BlowupOverlap R t x) := beta.right.toRingHom.toAlgebra966    exact IsLocalization.isNoetherianRing (Submonoid.powers (chartSlope R x t)) _ inferInstance967  have : IsNoetherianRing (Localization.AtPrime Q) :=968    IsLocalization.isNoetherianRing Q.primeCompl _ inferInstance969  have : IsNoetherianRing (Localization.AtPrime (Q.comap beta.right.toRingHom)) :=970    IsLocalization.isNoetherianRing (Q.comap beta.right.toRingHom).primeCompl _ inferInstance971  obtain ⟨Φ, hΦ⟩ :=972    local_completion_transport (Localization.AtPrime Q)973      (Localization.AtPrime (Q.comap beta.right.toRingHom)) φ974  refine ⟨Φ, fun b ↦ ?_⟩975  simp only [completedPointMap, RingHom.comp_apply]976  rw [hΦ, hφ]977 978/-- For pairwise distinct monic irreducible polynomials `φᵢ`, the intersection of the ideals979`(φᵢ^rᵢ)` is generated by `∏ φᵢ^rᵢ`. -/980theorem pairwise_distinct_irreducible_pow_iInf (k : Type) [Field k] (ι : Type) [Fintype ι]981    (φ : ι → Polynomial k) (hm : ∀ i, (φ i).Monic) (hirr : ∀ i, Irreducible (φ i))982    (hinj : Function.Injective φ) (r : ι → ℕ) :983    (⨅ i, Ideal.span {φ i ^ r i}) = Ideal.span {∏ i, φ i ^ r i} := by984  apply Ideal.iInf_span_singleton985  intro i j hij986  exact (distinct_monic_irreducible_coprime k _ _ (hm i) (hm j) (hirr i) (hirr j)987    (fun h ↦ hij (hinj h))).pow988 989/-- An ideal of `k[X]` containing a power `φ^L` of an irreducible polynomial is `(φ^r)` for some `r990≤ L`. -/991theorem polynomial_ideal_of_irreducible_pow_le (k : Type) [Field k] (φ : Polynomial k)992    (hφ : Irreducible φ) (J : Ideal (Polynomial k)) (L : ℕ) (hL : Ideal.span {φ^L} ≤ J) :993    ∃ r : ℕ, r ≤ L ∧ J = Ideal.span {φ^r} := by994  have hp : Prime φ := hφ.prime995  have hmem : φ ^ L ∈ J := hL (Ideal.mem_span_singleton_self _)996  have hd : Submodule.IsPrincipal.generator J ∣ φ ^ L :=997    (Submodule.IsPrincipal.mem_iff_generator_dvd J).1 hmem998  obtain ⟨r, hr, hass⟩ := (dvd_prime_pow hp L).1 hd999  refine ⟨r, hr, ?_⟩1000  rw [← Ideal.span_singleton_eq_span_singleton.2 hass, Ideal.span_singleton_generator]1001 1002/-- For irreducible `φ`, `k[X] ⧸ (φ^r)` has length `r` over `k[X]` and dimension `r · deg φ` over1003`k`. -/1004theorem polynomial_quotient_irreducible_pow_length (k : Type) [Field k] (φ : Polynomial k)1005    (hφ : Irreducible φ) (r : ℕ) :1006    Module.length (Polynomial k) (Polynomial k ⧸ Ideal.span {φ^r}) = (r : ℕ∞) ∧ Module.finrank k1007    (Polynomial k ⧸ Ideal.span {φ^r}) = r * φ.natDegree := by1008  refine ⟨?_, by rw [finrank_quotient_span_eq_natDegree, Polynomial.natDegree_pow]⟩1009  have hmax : (Ideal.span {φ}).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible hφ1010  have h1 : Module.length (Polynomial k) (Polynomial k ⧸ Ideal.span {φ}) = 1 := by1011    have : IsSimpleModule (Polynomial k) (Polynomial k ⧸ Ideal.span {φ}) :=1012      isSimpleModule_iff_quot_maximal.mpr ⟨_, hmax, ⟨LinearEquiv.refl _ _⟩⟩1013    exact Module.length_eq_one _ _1014  have hφ0 : φ ≠ 0 := hφ.ne_zero1015  induction r with1016  | zero =>1017    have : Subsingleton (Polynomial k ⧸ Ideal.span {φ ^ 0}) := by1018      rw [pow_zero, Ideal.span_singleton_one]1019      exact Ideal.Quotient.subsingleton_iff.mpr rfl1020    exact Module.length_eq_zero1021  | succ r ih =>1022    let P := Polynomial k1023    let I : Submodule P P := Ideal.span {φ ^ r}1024    let J : Submodule P P := Ideal.span {φ ^ (r + 1)}1025    let S : Submodule P P := Ideal.span {φ}1026    have hJI : J ≤ I := Ideal.span_singleton_le_span_singleton.mpr (pow_dvd_pow φ (Nat.le_succ r))1027    let m : P →ₗ[P] P ⧸ J := J.mkQ ∘ₗ LinearMap.mulLeft P (φ ^ r)1028    have hm : S ≤ LinearMap.ker m := by1029      intro a ha1030      obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp ha1031      simp only [LinearMap.mem_ker, m, LinearMap.coe_comp, Function.comp_apply,1032        LinearMap.mulLeft_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]1033      exact Ideal.mem_span_singleton.mpr ⟨b, by ring⟩1034    let f : P ⧸ S →ₗ[P] P ⧸ J := S.liftQ m hm1035    let g : P ⧸ J →ₗ[P] P ⧸ I := Submodule.factor hJI1036    have hf : Function.Injective f := by1037      rw [← LinearMap.ker_eq_bot, eq_bot_iff]1038      intro x hx1039      obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective S x1040      simp only [LinearMap.mem_ker, f, Submodule.liftQ_apply, m, LinearMap.coe_comp,1041        Function.comp_apply, LinearMap.mulLeft_apply, Submodule.mkQ_apply,1042        Submodule.Quotient.mk_eq_zero, J] at hx1043      obtain ⟨c, hc⟩ := Ideal.mem_span_singleton.mp hx1044      have : a = φ * c := by1045        have h' : φ ^ r * a = φ ^ r * (φ * c) := by rw [hc]; ring1046        exact mul_left_cancel₀ (pow_ne_zero r hφ0) h'1047      simp only [Submodule.mem_bot, Submodule.Quotient.mk_eq_zero]1048      exact Ideal.mem_span_singleton.mpr ⟨c, this⟩1049    have hg : Function.Surjective g := Submodule.factor_surjective hJI1050    have H : Function.Exact f g := by1051      intro y1052      obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective J y1053      change (Submodule.Quotient.mk a : P ⧸ I) = 0 ↔ _1054      rw [Submodule.Quotient.mk_eq_zero, Set.mem_range]1055      constructor1056      · intro ha1057        obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton.mp ha1058        exact ⟨Submodule.Quotient.mk b, rfl⟩1059      · rintro ⟨x, hx⟩1060        obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective S x1061        simp only [f, Submodule.liftQ_apply, m, LinearMap.coe_comp, Function.comp_apply,1062          LinearMap.mulLeft_apply, Submodule.mkQ_apply] at hx1063        rw [← sub_eq_zero, ← Submodule.Quotient.mk_sub, Submodule.Quotient.mk_eq_zero] at hx1064        have := I.sub_mem (Ideal.mem_span_singleton.mpr ⟨b, rfl⟩ : φ ^ r * b ∈ I) (hJI hx)1065        simpa using this1066    rw [Module.length_eq_add_of_exact f g hf hg H, h1, ih]1067    push_cast; ring1068 1069/-- The image of a principal ideal under a ring homomorphism is principal, generated by the image of1070the generator. -/1071theorem principal_ideal_image (R A : Type) [CommRing R] [CommRing A] (phi : R →+* A) (f : R) :1072    (Ideal.span {f}).map phi = Ideal.span {phi f} := by1073  rw [Ideal.map_span, Set.image_singleton]1074 1075private theorem map_span_colon_pow {R S : Type} [CommRing R] [CommRing S] (φ : R →+* S) (e F : S)1076    (d : ℕ) (f : R) (h : φ f = e ^ d * F) (inj : Function.Injective (fun y : S ↦ e * y)) :1077    ((Ideal.span {f}).map φ).colon {e ^ d} = Ideal.span {F} := by1078  have injd : IsLeftRegular (e ^ d) := IsLeftRegular.pow d inj1079  rw [principal_ideal_image, h]1080  ext u1081  rw [Submodule.mem_colon_singleton, Ideal.mem_span_singleton', Ideal.mem_span_singleton']1082  constructor1083  · rintro ⟨w, hw⟩1084    refine ⟨w, injd ?_⟩1085    have : w * (e ^ d * F) = u * e ^ d := hw1086    change e ^ d * (w * F) = e ^ d * u1087    rw [← mul_assoc, mul_comm (e ^ d) w, mul_assoc, this]; ring1088  · rintro ⟨w, hw⟩1089    exact ⟨w, by change w * (e ^ d * F) = u • e ^ d; rw [smul_eq_mul, ← hw]; ring⟩1090 1091private theorem chartBase_eq_pow_mul (R : Type) [CommRing R] (t x : R) (d : ℕ) (f : R)1092    (c : Fin (d + 1) → R) (hc : f = ∑ i : Fin (d + 1), c i * t ^ (d - i.val) * x ^ i.val) :1093    chartBase R t x f = chartBase R t x t ^ d * ∑ i : Fin (d+1), algebraMap R (BlowupChart R t x)1094    (c i) * (chartSlope R t x)^i.val := by1095  subst hc1096  rw [map_sum, Finset.mul_sum]1097  refine Finset.sum_congr rfl fun i _ ↦ ?_1098  have hi : i.val ≤ d := Nat.lt_succ_iff.mp i.isLt1099  have hx : chartBase R t x x = chartBase R t x t * chartSlope R t x :=1100    (blowup_chart_relation R t x).symm1101  have hd : chartBase R t x t ^ d =1102      chartBase R t x t ^ (d - i.val) * chartBase R t x t ^ i.val := by1103    rw [← pow_add]; congr 1; omega1104  simp only [map_mul, map_pow, hx, mul_pow, hd]1105  change _ = _ * (chartBase R t x (c i) * _)1106  ring1107 1108private theorem chartBase_eq_pow_mul_opposite (R : Type) [CommRing R] (t x : R) (d : ℕ) (f : R)1109    (c : Fin (d + 1) → R) (hc : f = ∑ i : Fin (d + 1), c i * t ^ (d - i.val) * x ^ i.val) :1110    chartBase R x t f = chartBase R x t x ^ d * ∑ i : Fin (d+1), algebraMap R (BlowupChart R x t)1111    (c i) * (chartSlope R x t)^(d - i.val) := by1112  subst hc1113  rw [map_sum, Finset.mul_sum]1114  refine Finset.sum_congr rfl fun i _ ↦ ?_1115  have hi : i.val ≤ d := Nat.lt_succ_iff.mp i.isLt1116  have ht : chartBase R x t t = chartBase R x t x * chartSlope R x t :=1117    (blowup_chart_relation R x t).symm1118  have hd : chartBase R x t x ^ d =1119      chartBase R x t x ^ (d - i.val) * chartBase R x t x ^ i.val := by1120    rw [← pow_add]; congr 1; omega1121  simp only [map_mul, map_pow, ht, mul_pow, hd]1122  change _ = _ * (chartBase R x t (c i) * _)1123  ring1124 1125/-! ### Strict transforms on the concrete surface -/1126 1127private theorem maximalIdeal_completedLocalAt (A : Type) [CommRing A] (Q : Ideal A) [Q.IsPrime]1128    [IsNoetherianRing A] :1129    IsLocalRing.maximalIdeal (CompletedLocalAt A Q) =1130      (IsLocalRing.maximalIdeal (Localization.AtPrime Q)).map1131        (localCompletionMap (Localization.AtPrime Q)) := by1132  have : IsNoetherianRing (Localization.AtPrime Q) :=1133    IsLocalization.isNoetherianRing Q.primeCompl _ inferInstance1134  exact AdicCompletion.maximalIdeal_eq_map1135 1136section ConcreteSurface1137 1138variable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]1139  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (pi : O)1140  (hpi : Irreducible pi) (u : (TwoSeries O)ˣ) (a b : ℕ) (ha : 0 < a)1141 1142-- Abbreviations for the concrete surface and its two parameters.1143local notation "𝒮" => ConcreteSurface O pi u a b1144local notation "𝒯" => surfaceT O pi u a b1145local notation "𝒳" => surfaceX O pi u a b1146 1147include hpi ha1148 1149/-- On the concrete surface, a child generator at an exceptional point of either chart (left point1150or point at infinity) whose curve meets the exceptional divisor with finite length is transverse1151to it: the two multiplications are injective and the curve ideal contains a power of the maximal1152ideal. -/1153theorem child_ideal_generator_transverse_finite (P : Ideal (BlowupChart 𝒮 𝒯 𝒳)) [P.IsMaximal]1154    [P.IsPrime] (hP : chartBase 𝒮 𝒯 𝒳 𝒯 ∈ P) (g : CompletedLocalAt (BlowupChart 𝒮 𝒯 𝒳) P)1155    (n : ℕ) (hg : Module.length (CompletedLocalAt (BlowupChart 𝒮 𝒯 𝒳) P)1156      (CompletedLocalAt (BlowupChart 𝒮 𝒯 𝒳) P ⧸ (Ideal.span {g} ⊔1157        Ideal.span {completedPointMap (BlowupChart 𝒮 𝒯 𝒳) P (chartBase 𝒮 𝒯 𝒳 𝒯)})) = (n : ℕ∞))1158    (Pinf : Ideal (BlowupChart 𝒮 𝒳 𝒯)) [Pinf.IsMaximal] [Pinf.IsPrime]1159    (hx : chartBase 𝒮 𝒳 𝒯 𝒳 ∈ Pinf) (hW : chartSlope 𝒮 𝒳 𝒯 ∈ Pinf)1160    (ginf : CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) Pinf) (m : ℕ)1161    (hginf : Module.length (CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) Pinf)1162      (CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) Pinf ⧸ (Ideal.span {ginf} ⊔1163        Ideal.span {completedPointMap (BlowupChart 𝒮 𝒳 𝒯) Pinf (chartBase 𝒮 𝒳 𝒯 𝒳)})) =1164        (m : ℕ∞)) :1165    (Function.Injective (fun w : CompletedLocalAt (BlowupChart 𝒮 𝒯 𝒳) P ⧸ Ideal.span {g} =>1166        Ideal.Quotient.mk (Ideal.span {g})1167          (completedPointMap (BlowupChart 𝒮 𝒯 𝒳) P (chartBase 𝒮 𝒯 𝒳 𝒯)) * w) ∧1168      Function.Injective (fun w : CompletedLocalAt (BlowupChart 𝒮 𝒯 𝒳) P ⧸1169          Ideal.span {completedPointMap (BlowupChart 𝒮 𝒯 𝒳) P (chartBase 𝒮 𝒯 𝒳 𝒯)} =>1170        Ideal.Quotient.mk1171          (Ideal.span {completedPointMap (BlowupChart 𝒮 𝒯 𝒳) P (chartBase 𝒮 𝒯 𝒳 𝒯)}) g * w) ∧1172      ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime P)).map1173          (localCompletionMap (Localization.AtPrime P)))^L ≤1174        finiteLocalCurveIdeal (BlowupChart 𝒮 𝒯 𝒳) P (chartBase 𝒮 𝒯 𝒳 𝒯) g 1) ∧1175    (Function.Injective (fun w : CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) Pinf ⧸ Ideal.span {ginf} =>1176        Ideal.Quotient.mk (Ideal.span {ginf})1177          (completedPointMap (BlowupChart 𝒮 𝒳 𝒯) Pinf (chartBase 𝒮 𝒳 𝒯 𝒳)) * w) ∧1178      Function.Injective (fun w : CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) Pinf ⧸1179          Ideal.span {completedPointMap (BlowupChart 𝒮 𝒳 𝒯) Pinf (chartBase 𝒮 𝒳 𝒯 𝒳)} =>1180        Ideal.Quotient.mk1181          (Ideal.span {completedPointMap (BlowupChart 𝒮 𝒳 𝒯) Pinf (chartBase 𝒮 𝒳 𝒯 𝒳)}) ginf * w) ∧1182      ∃ L : ℕ, ((IsLocalRing.maximalIdeal (Localization.AtPrime Pinf)).map1183          (localCompletionMap (Localization.AtPrime Pinf)))^L ≤1184        finiteLocalCurveIdeal (BlowupChart 𝒮 𝒳 𝒯) Pinf (chartBase 𝒮 𝒳 𝒯 𝒳) ginf 1) := by1185  have := blowupChart_concrete_isNoetherianRing O pi u a b 𝒯 𝒳1186  have := blowupChart_concrete_isNoetherianRing O pi u a b 𝒳 𝒯1187  obtain ⟨O', _, _, _, _, _, pi', u', a', b', hpi', ha', ψ, hψ⟩ :=1188    concrete_left_point_completion_is_surface O pi hpi u a b ha P hP1189  obtain ⟨_, -, _, -⟩ := concrete_left_point_completion_instances O pi hpi u a b ha P hP1190  obtain ⟨-, ⟨ψi, hψi⟩, _, ⟨_, -⟩, hregi⟩ :=1191    concrete_infinity_point_completion O pi hpi u a b ha Pinf hx hW1192  have key := transverse_of_concreteSurface_equiv _ O' pi' hpi' u' a' b' ha' ψ _ g hψ n hg1193    (concrete_left_point_exceptional_regular O pi hpi u a b ha P hP)1194  have keyi := transverse_of_concreteSurface_equiv _ O pi hpi (xSubstUnit O u) (a + b) a1195    (Nat.add_pos_left ha b) ψi _ ginf hψi m hginf hregi1196  obtain ⟨L, hL⟩ := key.2.21197  obtain ⟨Li, hLi⟩ := keyi.2.21198  exact ⟨⟨key.1, key.2.1, L, by simpa [← maximalIdeal_completedLocalAt _ P, finiteLocalCurveIdeal]1199      using hL⟩,1200    ⟨keyi.1, keyi.2.1, Li, by1201      simpa [← maximalIdeal_completedLocalAt _ Pinf, finiteLocalCurveIdeal] using hLi⟩⟩1202 1203/-- At the point at infinity of the concrete surface, the intersection length of the strict1204transform of `∑ cᵢ tᵈ⁻ⁱ xⁱ` with the exceptional divisor is `d - deg H`, where `H = ∑ c̄ᵢ Zⁱ` is1205the residue polynomial. -/1206theorem concrete_infinity_strict_transform_multiplicity (d : ℕ) (c : Fin (d + 1) → 𝒮)1207    (hne : ∃ i : Fin (d + 1), c i ∉ Ideal.span {𝒯, 𝒳}) [IsLocalRing 𝒮]1208    (P : Ideal (BlowupChart 𝒮 𝒳 𝒯)) [P.IsMaximal] [P.IsPrime]1209    (hx : chartBase 𝒮 𝒳 𝒯 𝒳 ∈ P) (hW : chartSlope 𝒮 𝒳 𝒯 ∈ P) :1210    Module.length (CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) P)1211      (CompletedLocalAt (BlowupChart 𝒮 𝒳 𝒯) P ⧸1212        Ideal.span {completedPointMap (BlowupChart 𝒮 𝒳 𝒯) P1213          (∑ i : Fin (d+1),1214            algebraMap 𝒮 (BlowupChart 𝒮 𝒳 𝒯) (c i) * chartSlope 𝒮 𝒳 𝒯 ^ (d - i.val)),1215        completedPointMap (BlowupChart 𝒮 𝒳 𝒯) P (chartBase 𝒮 𝒳 𝒯 𝒳)}) =1216    ((d - (∑ i : Fin (d+1), Polynomial.C (IsLocalRing.residue 𝒮 (c i)) * Polynomial.X^i.val :1217      Polynomial (IsLocalRing.ResidueField 𝒮)).natDegree : ℕ) : ℕ∞) := by1218  have hP := (concrete_infinity_point_completion O pi hpi u a b ha P hx hW).11219  obtain ⟨ψ, hb, hs, -⟩ := x_chart_infinity_completion_equiv O pi hpi u a b ha P hP1220  obtain ⟨q, hq⟩ := concrete_surface_quotient_T_equiv O pi hpi (xSubstUnit O u) (a + b) a (by omega)1221  obtain ⟨e0, he0⟩ := concrete_surface_quotient_parameters_equiv O pi hpi u a b ha1222  have hmax := concrete_surface_maximalIdeal_eq O pi hpi u a b ha1223  let κ : IsLocalRing.ResidueField 𝒮 ≃+* IsLocalRing.ResidueField O :=1224    (Ideal.quotEquivOfEq hmax).trans e01225  have hκ : ∀ s : TwoSeries O, κ (IsLocalRing.residue _ (surfaceMk O pi u a b s)) =1226      IsLocalRing.residue O (MvPowerSeries.constantCoeff s) := fun s ↦ by1227    change e0 (Ideal.quotEquivOfEq hmax (Ideal.Quotient.mk _ (surfaceMk O pi u a b s))) = _1228    rw [Ideal.quotEquivOfEq_mk]1229    exact he0 s1230  have hxT : ψ (completedPointMap _ P (chartBase _ _ _ 𝒳)) =1231      surfaceT O pi (xSubstUnit O u) (a + b) a := by1232    have h := hb (axisX O)1233    rwa [(chartSubst_apply_generators O 0).2.2.2.2.2.1] at h1234  rw [← RingEquiv.symm_apply_apply ψ (completedPointMap _ P (chartBase _ _ _ 𝒳)), hxT,1235    (concrete_surface_equiv_curve_length_and_regular _ O pi (xSubstUnit O u) (a + b) a ψ q _).1]1236  let Ψ : BlowupChart 𝒮 𝒳 𝒯 →+* PowerSeries (IsLocalRing.ResidueField O) :=1237    q.toRingHom.comp ((Ideal.Quotient.mk _).comp (ψ.toRingHom.comp (completedPointMap _ P)))1238  have hΨc : ∀ r : 𝒮, Ψ (algebraMap _ _ r) = PowerSeries.C (κ (IsLocalRing.residue _ r)) :=1239      fun r ↦ by1240    obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective r1241    change q (Ideal.Quotient.mk _ (ψ (completedPointMap _ P (chartBase _ _ _1242      (surfaceMk O pi u a b s))))) = _1243    rw [hb, hq, residueKillT_xChartSubst O pi hpi]; exact congrArg _ (hκ s).symm1244  have hΨW : Ψ (chartSlope _ _ _) = PowerSeries.X := by1245    change q (Ideal.Quotient.mk _ (ψ (completedPointMap _ P _))) = _1246    rw [hs, show surfaceX O pi (xSubstUnit O u) (a + b) a = surfaceMk _ _ _ _ _ (axisX O) from rfl,1247      hq, (residueKillT_apply_ker O pi hpi).2.2.1]1248  rw [show ∀ y, q (Ideal.Quotient.mk _ (ψ (completedPointMap _ P y))) = Ψ y from fun _ ↦ rfl]1249  simp only [map_sum, map_mul, map_pow, hΨc, hΨW]1250  obtain ⟨i, hi⟩ := hne1251  refine order_reflected_sum κ.toRingHom d _ ⟨i, ?_⟩1252  rwa [Ne, IsLocalRing.residue_eq_zero_iff, hmax]1253 1254/-- On the concrete surface, the strict transform of `(∑ cᵢ t^(d-i) xⁱ)` is generated by `∑ cᵢ zⁱ`1255at a left exceptional point and by `∑ cᵢ w^(d-i)` at the point at infinity. -/1256theorem concrete_strict_transform_generators (d : ℕ) (f : 𝒮) (c : Fin (d + 1) → 𝒮)1257    (hc : f = ∑ i : Fin (d + 1), c i * 𝒯 ^ (d - i.val) * 𝒳 ^ i.val) (P : Ideal (BlowupChart 𝒮 𝒯 𝒳))1258    [P.IsMaximal] [P.IsPrime] (hP : chartBase 𝒮 𝒯 𝒳 𝒯 ∈ P) (Pinf : Ideal (BlowupChart 𝒮 𝒳 𝒯))1259    [Pinf.IsMaximal] [Pinf.IsPrime] (hx : chartBase 𝒮 𝒳 𝒯 𝒳 ∈ Pinf)1260    (hW : chartSlope 𝒮 𝒳 𝒯 ∈ Pinf) :1261    strictTransformAt 𝒮 𝒯 𝒳 P d (Ideal.span {f}) = Ideal.span {completedPointMap1262      (BlowupChart 𝒮 𝒯 𝒳) P1263      (∑ i : Fin (d+1), algebraMap 𝒮 (BlowupChart 𝒮 𝒯 𝒳) (c i) * chartSlope 𝒮 𝒯 𝒳 ^ i.val)} ∧1264    strictTransformAt 𝒮 𝒳 𝒯 Pinf d (Ideal.span {f}) = Ideal.span {completedPointMap1265      (BlowupChart 𝒮 𝒳 𝒯) Pinf1266      (∑ i : Fin (d+1),1267        algebraMap 𝒮 (BlowupChart 𝒮 𝒳 𝒯) (c i) * chartSlope 𝒮 𝒳 𝒯 ^ (d - i.val))} := by1268  obtain ⟨_, _, _, inj⟩ :=1269    (concrete_infinity_point_completion O pi hpi u a b ha Pinf hx hW).21270  refine ⟨map_span_colon_pow _ _ _ d f ?_1271    (concrete_left_point_exceptional_regular O pi hpi u a b ha P hP),1272    map_span_colon_pow _ _ _ d f ?_ inj⟩ <;> simp only [RingHom.comp_apply] <;>1273    rw [← map_pow, ← map_mul]1274  exacts [congrArg _ (chartBase_eq_pow_mul _ _ _ d f c hc),1275    congrArg _ (chartBase_eq_pow_mul_opposite _ _ _ d f c hc)]1276 1277end ConcreteSurface1278 1279/-- Multiplying the generator of a principal ideal by a unit does not change the ideal. -/1280theorem principal_ideal_unit_invariance (R : Type) [CommRing R] (f : R) (u : Rˣ) :1281    Ideal.span {(u : R)*f} = Ideal.span {f} :=1282  Ideal.span_singleton_mul_left_unit u.isUnit f1283 1284end SurfaceBlowup