/-
Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)
-/
import SurfaceBlowup.Blowup.DivisorPoints
import SurfaceBlowup.Recursion.Termination

/-!
# Strict transforms give a bijection on a fixed tangent cell

For a regular local surface with regular parameters `t, x`, the level-one generators of the two
chart kernels of a two-chart curve datum glue (after normalization by a unit) to a global function
`f`. For the concrete surfaces `ConcreteSurface O pi u a b` this shows that the strict transform
map on the fixed tangent cell is injective; combined with the existence of curve data for
prescribed child ideals, it is a bijection onto the product of the child ideal sets.

## Main results

* `SurfaceBlowup.two_chart_global_function_exists`: a two-chart curve datum on a complete regular
  local surface comes from a global function.
* `SurfaceBlowup.concrete_two_chart_glued_generators_exist`: the same for the concrete surfaces.
* `SurfaceBlowup.strict_transform_injOn_fixed_tangent_cell`: the strict transform map is injective
  on the fixed tangent cell.
* `SurfaceBlowup.strict_transform_bijOn_child_ideals`: it is a bijection onto the product of the
  child ideal sets.

## Implementation notes

Statements about the concrete surfaces `ConcreteSurface O pi u a b` are written with the local
notations `tChart`, `tExc`, ... for the blow-up charts and their data; see the notation section.

Provenance: Lemma 4.2 and Proposition 5.1 of the source paper;
`Thm_SurfaceBlowupV2_{two_chart_level_one_coefficients_left,
two_chart_right_level_one_kernel_polynomial, two_chart_level_one_coefficients_right,
two_chart_level_one_normalization, two_chart_global_function_exists, concrete_two_chart_lemma_4_2,
prop_5_1_injOn, prop_5_1_bijOn}`.
-/

namespace SurfaceBlowup

open scoped BigOperators ENNReal

/-! ### Notation for the concrete surfaces

Local notations for the charts of the blow-up of `R = ConcreteSurface O pi u a b` at its
closed point `(t, x)`, taking the surface data as explicit arguments. -/

/-- The `t`-chart `R[x/t]` of the blow-up of the concrete surface at `(t, x)`. -/
local notation:max "tChart" O:max pi:max u:max a:max b:max =>
  BlowupChart (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The structure map `R → R[x/t]`. -/
local notation:max "tBase" O:max pi:max u:max a:max b:max =>
  chartBase (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The slope `x/t` in the `t`-chart. -/
local notation:max "tSlope" O:max pi:max u:max a:max b:max =>
  chartSlope (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The exceptional ideal `(t)` of the `t`-chart. -/
local notation:max "tExc" O:max pi:max u:max a:max b:max =>
  chartExceptional (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)

/-- The exceptional ideal `(x)` of the `x`-chart. -/
local notation:max "xExc" O:max pi:max u:max a:max b:max =>
  chartExceptional (ConcreteSurface O pi u a b) (surfaceX O pi u a b) (surfaceT O pi u a b)

/-- If `e : A ⧸ J ≃ k[X]` (with `k = R ⧸ I` a field) sends constants to constants and `w` to `X`,
and the image of the principal ideal `(F mod J)` is generated by `P`, then `F` is congruent
mod `J` to `∑ cᵢ wⁱ` (`i ≤ deg P`) where `cᵢ mod I = u · P.coeff i` for a nonzero `u`. -/
private theorem exists_coeffs_of_map_span_eq {R A : Type} [CommRing R] [CommRing A] [Algebra R A]
    {I : Ideal R} [I.IsMaximal] {J : Ideal A} {w : A} (e : (A ⧸ J) ≃+* Polynomial (R ⧸ I))
    (he : ∀ r : R, e (Ideal.Quotient.mk J (algebraMap R A r)) =
      Polynomial.C (Ideal.Quotient.mk I r))
    (hw : e (Ideal.Quotient.mk J w) = Polynomial.X) (F : A) (P : Polynomial (R ⧸ I))
    (hker : (Ideal.span {Ideal.Quotient.mk J F}).map e = Ideal.span {P}) :
    ∃ c : Fin (P.natDegree + 1) → R,
      F - ∑ i : Fin (P.natDegree + 1), algebraMap R A (c i) * w ^ i.val ∈ J ∧
      ∃ u : R ⧸ I, u ≠ 0 ∧ ∀ i, Ideal.Quotient.mk I (c i) = P.coeff i * u := by
  let _ : Field (R ⧸ I) := Ideal.Quotient.field _
  rw [Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hker
  obtain ⟨v, hv⟩ := hker
  obtain ⟨c, hc, hcv⟩ := Polynomial.isUnit_iff.mp v.isUnit
  choose a ha using fun i : Fin (P.natDegree + 1) =>
    Ideal.Quotient.mk_surjective (I := I) (P.coeff i.val * c⁻¹)
  refine ⟨a, ?_, c⁻¹, inv_ne_zero hc.ne_zero, ha⟩
  rw [← Ideal.Quotient.eq]
  apply e.injective
  have heF : e (Ideal.Quotient.mk J F) = P * Polynomial.C c⁻¹ := by
    rw [← hv, ← hcv, mul_assoc, ← Polynomial.C_mul, mul_inv_cancel₀ hc.ne_zero, Polynomial.C_1,
      mul_one]
  simp only [heF, map_sum, map_mul, map_pow, hw, he, ha]
  conv_lhs => rw [P.as_sum_range_C_mul_X_pow]
  rw [Finset.sum_mul, Fin.sum_univ_eq_sum_range
    (fun i => Polynomial.C (P.coeff i) * Polynomial.C c⁻¹ * Polynomial.X ^ i)]
  exact Finset.sum_congr rfl fun i _ => by ring

/-- Level-one coefficients in the left chart: the generator `FA` of the level-one left kernel is
congruent mod the exceptional ideal to `∑ cA i · slope^i`, whose first `r` coefficients lie in
`(t, x)`, with `r` the multiplicity at the points over `x/t = 0` and `m` the weighted degree. -/
private theorem two_chart_level_one_coefficients_left (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R t x)]
    (FA : BlowupChart R t x) (hFA : leftLevelKernel D 1 =
    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^1) FA}) :
    ∃ (m r : ℕ) (cA : Fin (m+1) → R), FA - ∑ i : Fin (m+1), algebraMap R (BlowupChart R t x) (cA i)
        * (chartSlope R t x)^i.val ∈ chartExceptional R t x ∧
        (∀ i : Fin (m+1), i.val < r → cA i ∈ Ideal.span {t,x}) ∧
        (∀ i : Fin (m+1), i.val = r → cA i ∉ Ideal.span {t,x}) ∧ r ≤ m ∧ r = ∑ᶠ k : D.ι0,
        leftMultiplicity D (Sum.inr k) ∧ m = ∑ᶠ s : D.ι ⊕ D.ι0, leftResidueDegree D s *
        leftMultiplicity D s := by
  classical
  let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _
  have : Fintype D.ι := @Fintype.ofFinite _ D.fin
  have : Fintype D.ι0 := @Fintype.ofFinite _ D.fin0
  obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x
  obtain ⟨φ, hφ, -, hne, hX, hdeg, -, hker⟩ :=
    two_chart_left_level_one_kernel_polynomial R t x beta D e he heZ
  have gen : ∀ J : Ideal (BlowupChart R t x), J = chartExceptional R t x →
      (leftKernel D 1).map (Ideal.Quotient.mk J) = Ideal.span {Ideal.Quotient.mk J FA} →
      (leftKernel D 1).map (Ideal.Quotient.mk (chartExceptional R t x)) =
        Ideal.span {Ideal.Quotient.mk (chartExceptional R t x) FA} := by
    rintro J rfl h; exact h
  set Pol := ∏ᶠ s, φ s ^ leftMultiplicity D s with hPol
  set r := ∑ᶠ k : D.ι0, leftMultiplicity D (Sum.inr k) with hr
  set Q := ∏ i : D.ι, φ (Sum.inl i) ^ leftMultiplicity D (Sum.inl i) with hQ
  rw [gen _ (pow_one _) hFA] at hker
  obtain ⟨cA, hgA, u, hu, hcA⟩ := exists_coeffs_of_map_span_eq e he heZ FA _ hker
  have hPolXQ : Pol = Polynomial.X ^ r * Q := by
    rw [hPol, finprod_eq_prod_of_fintype, Fintype.prod_sum_type, hr, finsum_eq_sum_of_fintype,
      mul_comm]
    congr 1
    simp only [hX]
    exact Finset.prod_pow_eq_pow_sum _ _ _
  have hQ0 : Q.coeff 0 ≠ 0 := by
    rw [Polynomial.coeff_zero_eq_eval_zero, hQ, Polynomial.eval_prod]
    refine Finset.prod_ne_zero_iff.mpr fun i _ => ?_
    rw [Polynomial.eval_pow]
    refine pow_ne_zero _ fun h0 => ?_
    rw [← Polynomial.coeff_zero_eq_eval_zero, ← Polynomial.X_dvd_iff] at h0
    obtain ⟨g, hg⟩ := h0
    obtain ⟨hmon, hirr⟩ := hφ (Sum.inl i)
    rcases hirr.isUnit_or_isUnit hg with h | h
    · exact Polynomial.not_isUnit_X h
    · rw [(Polynomial.monic_X.of_mul_monic_left (hg ▸ hmon)).isUnit_iff] at h
      exact hne i (by rw [hg, h, mul_one])
  have hrP : Pol.coeff r ≠ 0 := by
    rw [hPolXQ, Polynomial.coeff_X_pow_mul']; simpa using hQ0
  refine ⟨Pol.natDegree, r, cA, hgA, fun i hi => ?_, fun i hi => ?_,
    Polynomial.le_natDegree_of_ne_zero hrP, hr, ?_⟩
  · have hlow : ∀ j, j < r → Pol.coeff j = 0 := fun j hj => by
      rw [hPolXQ, Polynomial.coeff_X_pow_mul']; simp [Nat.not_le.mpr hj]
    rw [← Ideal.Quotient.eq_zero_iff_mem, hcA, hlow _ hi, zero_mul]
  · rw [← Ideal.Quotient.eq_zero_iff_mem, hcA, hi]
    exact mul_ne_zero hrP hu
  · rw [hPol, finprod_eq_prod_of_fintype, finsum_eq_sum_of_fintype,
      Polynomial.natDegree_prod_of_monic _ _ fun s _ => (hφ s).1.pow _]
    refine Finset.sum_congr rfl fun s _ => ?_
    rw [(hφ s).1.natDegree_pow, hdeg, mul_comm]

/-- The level-one right kernel, transported to `k[X]` along an identification of the right
exceptional line, is generated by `∏ ψₛ ^ multₛ` for distinct monic irreducibles `ψₛ`, with
`ψ = X` exactly at the points at infinity. -/
private theorem two_chart_right_level_one_kernel_polynomial (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R x t)]
    (eB : (BlowupChart R x t ⧸ chartExceptional R x t) ≃+*
    Polynomial (R ⧸ Ideal.span ({t,x} : Set R)))
    (heB : ∀ r : R, eB (Ideal.Quotient.mk (chartExceptional R x t) (chartBase R x t r)) =
    Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r))
    (heW : eB (Ideal.Quotient.mk (chartExceptional R x t) (chartSlope R x t)) = Polynomial.X) :
    ∃ ψ : D.ι ⊕ D.ιinf → Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),
        (∀ s, (ψ s).Monic ∧ Irreducible (ψ s)) ∧ Function.Injective ψ ∧
        (∀ i, ψ (Sum.inl i) ≠ Polynomial.X) ∧ (∀ l, ψ (Sum.inr l) = Polynomial.X) ∧
        (∀ s, (ψ s).natDegree = rightResidueDegree D s) ∧ (∀ l, rightResidueDegree D (Sum.inr l) =
        1) ∧ ((rightKernel D 1).map (Ideal.Quotient.mk (chartExceptional R x t))).map eB =
        Ideal.span {∏ᶠ s, ψ s ^ rightMultiplicity D s}  := by
  obtain ⟨hmax, hinjP, htP⟩ := two_chart_right_points_maximal R t x beta D
  obtain ⟨ψ, m, hψ, hinj, hslope, hlen, hm, hker⟩ := level_one_kernel_polynomial R x t _
    Ideal.span_pair_comm eB heB heW (rightPoint D) hinjP htP (rightData D)
    (two_chart_right_data_transverse_finite R t x beta D 1).2
  have hmult : rightMultiplicity D = m := funext fun s => by
    unfold rightMultiplicity rightLevelIdeal; rw [hm s]; rfl
  have hdeg : ∀ s, (ψ s).natDegree = rightResidueDegree D s := by
    intro s; unfold rightResidueDegree; rw [hlen s]; rfl
  have hX : ∀ l, ψ (Sum.inr l) = Polynomial.X := fun l => (hslope (Sum.inr l)).1 (D.slopeinf l)
  refine ⟨ψ, hψ, hinj, fun i hi => ?_, hX, hdeg, fun l => ?_, by rw [hmult]; exact hker⟩
  · have hQ := D.onE i
    have := D.maximal i
    exact (overlap_exceptional_point_comap_maximal_right R t x beta (D.Q i) hQ).2.1
      ((hslope (Sum.inl i)).2 hi)
  · rw [← hdeg, hX]; exact Polynomial.natDegree_X

/-- The exceptional line `R[t/x] ⧸ (x)` of the right chart is the affine line over
`R ⧸ (t, x)`, with coordinate the slope `t/x`. -/
private theorem exceptional_line_equiv_chart_exceptional_swap (R : Type) [CommRing R] (t x : R) :
    ∃ e : (BlowupChart R x t ⧸ chartExceptional R x t) ≃+*
      Polynomial (R ⧸ Ideal.span ({t,x} : Set R)),
      (∀ r : R, e (Ideal.Quotient.mk (chartExceptional R x t) (chartBase R x t r)) =
        Polynomial.C (Ideal.Quotient.mk (Ideal.span ({t,x} : Set R)) r)) ∧
      e (Ideal.Quotient.mk (chartExceptional R x t) (chartSlope R x t)) = Polynomial.X := by
  have h := exceptional_line_equiv_chart_exceptional R x t
  rwa [Set.pair_comm x t] at h

/-- Level-one coefficients in the right chart: the generator `FB` of the level-one right kernel
is congruent mod the exceptional ideal to `∑ cB i · slope^i` with leading coefficient a unit and
`n` the weighted degree. -/
private theorem two_chart_level_one_coefficients_right (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsNoetherianRing (BlowupChart R x t)]
    (FB : BlowupChart R x t) (hFB : rightLevelKernel D 1 =
    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^1) FB}) :
    ∃ (n : ℕ) (cB : Fin (n+1) → R), FB - ∑ i : Fin (n+1), algebraMap R (BlowupChart R x t) (cB i) *
        (chartSlope R x t)^i.val ∈ chartExceptional R x t ∧ cB (Fin.last n) ∉ Ideal.span {t,x} ∧ n =
        ∑ᶠ s : D.ι ⊕ D.ιinf, rightResidueDegree D s * rightMultiplicity D s := by
  classical
  let _ : Field (R ⧸ Ideal.span ({t,x} : Set R)) := Ideal.Quotient.field _
  have : Fintype D.ι := @Fintype.ofFinite _ D.fin
  have : Fintype D.ιinf := @Fintype.ofFinite _ D.fininf
  obtain ⟨e, he', heW⟩ := exceptional_line_equiv_chart_exceptional_swap R t x
  obtain ⟨φ, hφ, -, -, -, hdeg, -, hker⟩ :=
    two_chart_right_level_one_kernel_polynomial R t x beta D e he' heW
  have gen : ∀ J : Ideal (BlowupChart R x t), J = chartExceptional R x t →
      (rightKernel D 1).map (Ideal.Quotient.mk J) = Ideal.span {Ideal.Quotient.mk J FB} →
      (rightKernel D 1).map (Ideal.Quotient.mk (chartExceptional R x t)) =
        Ideal.span {Ideal.Quotient.mk (chartExceptional R x t) FB} := by
    rintro J rfl h; exact h
  set Pol := ∏ᶠ s, φ s ^ rightMultiplicity D s with hPol
  rw [gen _ (pow_one _) hFB] at hker
  obtain ⟨cB, hgB, u, hu, hcB⟩ := exists_coeffs_of_map_span_eq e he' heW FB _ hker
  have hPm : Pol.Monic := by
    rw [hPol, finprod_eq_prod_of_fintype]
    exact Polynomial.monic_prod_of_monic _ _ fun s _ => (hφ s).1.pow _
  refine ⟨Pol.natDegree, cB, hgB, ?_, ?_⟩
  · rw [← Ideal.Quotient.eq_zero_iff_mem, hcB, Fin.val_last, show Pol.coeff _ = 1 from hPm, one_mul]
    exact hu
  · rw [hPol, finprod_eq_prod_of_fintype, finsum_eq_sum_of_fintype,
      Polynomial.natDegree_prod_of_monic _ _ fun s _ => (hφ s).1.pow _]
    refine Finset.sum_congr rfl fun s _ => ?_
    rw [(hφ s).1.natDegree_pow, hdeg, mul_comm]

/-- Level-one normalization: the two level-one generators agree on the overlap up to a unit
`u` of `R` and the factor `slope^deg D`, modulo the overlap exceptional ideal. -/
private theorem two_chart_level_one_normalization (R : Type) [CommRing R] (t x : R)
    (beta : BlowupRestriction R t x) (D : TwoChartCurveData R t x beta)
    [(Ideal.span ({t,x} : Set R)).IsMaximal] [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)]
    [IsNoetherianRing (BlowupChart R x t)] (hreg : RegularParameterPair R t x)
    (hregSwap : RegularParameterPair R x t) (FA : ℕ → BlowupChart R t x)
    (hFA : ∀ j : ℕ, leftLevelKernel D j =
    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R t x t})^j) (FA j)})
    (FB : ℕ → BlowupChart R x t) (hFB : ∀ j : ℕ, rightLevelKernel D j =
    Ideal.span {Ideal.Quotient.mk ((Ideal.span {chartBase R x t x})^j) (FB j)}) :
    ∃ u : Rˣ, (algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1) - algebraMap
        R (BlowupOverlap R t x) (u : R) * ((overlapSlope R t x)^(curveDataDegree D) *
        beta.right (FB 1)) ∈ (Ideal.span {overlapException R t x}) := by
  have hpow : (Ideal.span {overlapException R t x})^1 = Ideal.span {overlapException R t x} :=
    pow_one _
  have hoverlap :
      Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x})
        ((algebraMap (BlowupChart R t x) (BlowupOverlap R t x)) (FA 1))} =
      Ideal.span {Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right (FB 1))} := by
    have := congrArg (Ideal.map (Ideal.quotEquivOfEq hpow).toRingHom)
      (two_chart_level_generators_agree_on_overlap R t x beta D FA hFA FB hFB 1)
    rwa [Ideal.map_span, Ideal.map_span, Set.image_singleton, Set.image_singleton] at this
  obtain ⟨hmaxR, -, hPe⟩ := two_chart_right_points_maximal R t x beta D
  have : ∀ s, (rightPoint D s).IsMaximal := hmaxR
  choose L hL using (two_chart_right_data_transverse_finite R t x beta D 1).2
  have hreg1 := overlap_level_generator_regular R t x hreg hregSwap beta (D.ι ⊕ D.ιinf)
    (rightPoint D) hPe (rightData D) L hL FB hFB 1
  have hregB : Function.Injective
      (fun c : BlowupOverlap R t x ⧸ (Ideal.span {overlapException R t x}) =>
        Ideal.Quotient.mk (Ideal.span {overlapException R t x}) (beta.right (FB 1)) * c) := by
    intro a b hab
    apply (Ideal.quotEquivOfEq hpow).symm.injective
    apply hreg1
    have key : ∀ y : BlowupOverlap R t x,
        Ideal.Quotient.mk ((Ideal.span {overlapException R t x})^1) y =
          (Ideal.quotEquivOfEq hpow).symm (Ideal.Quotient.mk _ y) := fun _ ↦ rfl
    simp only [key, ← map_mul]
    exact congrArg _ hab
  obtain ⟨m, r, cA, hgA, hlow, hr, hrm, hrdef, hmdef⟩ :=
    two_chart_level_one_coefficients_left R t x beta D (FA 1) (hFA 1)
  obtain ⟨n, cB, hgB, htop, hndef⟩ :=
    two_chart_level_one_coefficients_right R t x beta D (FB 1) (hFB 1)
  have hdeg : r + n = curveDataDegree D := by
    obtain ⟨e, he, heZ⟩ := exceptional_line_equiv_chart_exceptional R t x
    obtain ⟨eB, heB, heW⟩ := exceptional_line_equiv_chart_exceptional_swap R t x
    obtain ⟨_, -, -, -, -, -, h0, -⟩ :=
      two_chart_left_level_one_kernel_polynomial R t x beta D e he heZ
    obtain ⟨_, -, -, -, -, -, hinf, -⟩ :=
      two_chart_right_level_one_kernel_polynomial R t x beta D eB heB heW
    have hδ : ∀ i, leftResidueDegree D (Sum.inl i) = rightResidueDegree D (Sum.inl i) := fun i ↦
      congrArg ENat.toNat (overlap_point_residue_field_equiv R t x beta (D.Q i) (D.onE i)).2.2
    have hμ : ∀ i, leftMultiplicity D (Sum.inl i) = rightMultiplicity D (Sum.inl i) := fun i ↦
      (two_chart_common_multiplicity_eq R t x beta D i).1.trans
        (two_chart_common_multiplicity_eq R t x beta D i).2.symm
    have := Fintype.ofFinite D.ι
    have := Fintype.ofFinite D.ι0
    have := Fintype.ofFinite D.ιinf
    unfold curveDataDegree
    rw [hrdef, hndef]
    simp only [finsum_eq_sum_of_fintype, Fintype.sum_sum_type, h0, hinf, hδ, hμ, one_mul]
    ring
  exact glued_level_one_normalization R t x hreg beta _ (FA 1) (FB 1) hoverlap hregB m n cA cB hgA
      hgB r hlow hr hrm htop hdeg

/-- A two-chart curve datum on a complete regular local surface comes
from a global function `f` whose glued level generators cut out the left and right level kernels. -/
theorem two_chart_global_function_exists (R : Type) [CommRing R] (t x : R) (beta : BlowupRestriction
    R t x) (D : TwoChartCurveData R t x beta) [(Ideal.span ({t,x} : Set R)).IsMaximal]
    [IsLocalRing R] [IsNoetherianRing (BlowupChart R t x)] [IsNoetherianRing (BlowupChart R x t)]
    [IsAdicComplete (Ideal.span {t,x}) R] (hreg : RegularParameterPair R t x)
    (hregSwap : RegularParameterPair R x t) :
    ∃ f : R, ∃ G : GluedGenerators R t x beta (curveDataDegree D),
        (∀ j : ℕ, surfaceToCechInput R t x j f = (cechInputLattice R t x j).mkQ (gluedFunctionPair R
        t x G j)) ∧ ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk ((chartExceptional R t x)^j) (G.left j)}
        = leftLevelKernel D j ∧
        Ideal.span {Ideal.Quotient.mk ((chartExceptional R x t)^j) (G.right j)} = rightLevelKernel D
        j := by
  obtain ⟨⟨FA, hFA⟩, ⟨FB, hFB⟩⟩ := two_chart_level_generators_exist R t x beta D
  exact global_function_of_two_chart_curve_data R t x beta D hreg hregSwap
    (curveDataDegree D) FA hFA FB hFB
    (two_chart_level_one_normalization R t x beta D hreg hregSwap FA hFA FB hFB)

/-- A two-chart curve datum on a concrete surface `ConcreteSurface O pi u a b` comes from a global
function `f` whose glued level generators cut out the left and right level kernels. -/
theorem concrete_two_chart_glued_generators_exist (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) (beta : BlowupRestriction (ConcreteSurface O pi u a b)
        (surfaceT O pi u a b) (surfaceX O pi u a b))
    (D : TwoChartCurveData (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
        beta) :
    ∃ f : ConcreteSurface O pi u a b, ∃ G : GluedGenerators (ConcreteSurface O pi u a b)
        (surfaceT O pi u a b) (surfaceX O pi u a b) beta (curveDataDegree D),
      (∀ j : ℕ, surfaceToCechInput (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
          (surfaceX O pi u a b) j f =
        (cechInputLattice (ConcreteSurface O pi u a b) (surfaceT O pi u a b) (surfaceX O pi u a b)
            j).mkQ (gluedFunctionPair (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
                (surfaceX O pi u a b) G j)) ∧
      ∀ j : ℕ, Ideal.span {Ideal.Quotient.mk (tExc O pi u a b^j) (G.left j)} = leftLevelKernel D j ∧
        Ideal.span {Ideal.Quotient.mk (xExc O pi u a b^j) (G.right j)} = rightLevelKernel D j := by
  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))).IsMaximal :=
    concrete_surface_parameterIdeal_isMaximal O pi hpi u a b ha
  have := concrete_surface_isLocalRing O pi u a b hpi.not_isUnit ha
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  have : IsAdicComplete (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))) (ConcreteSurface O pi u a b) :=
    concrete_surface_isAdicComplete_parameterIdeal O pi u a b
  exact two_chart_global_function_exists _ _ _ beta D
    (concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha)
    (concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha)

/-- On the fixed tangent cell, an ideal is determined by its
strict transforms at the points of the exceptional divisor `Dv`. -/
theorem strict_transform_injOn_fixed_tangent_cell (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]
        [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O
            (ConcreteSurface O pi u a b))
    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField
        (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ)
    (hdeg : exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) Dv = d) :
    Set.InjOn (fun J Q => divisorStrictTransform (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b) e Dv hinf d J Q)
      (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv) := by
  intro J₁ h₁ J₂ h₂ hJ
  obtain ⟨beta⟩ := actual_blowup_restriction_exists (ConcreteSurface O pi u a b)
      (surfaceT O pi u a b) (surfaceX O pi u a b)
  obtain ⟨f₁, c, D, hJ₁, -, -, -, hst₁, hst₁r, hm, hdegD⟩ :=
    fixed_tangent_cell_curve_datum O pi hpi u a b ha S ⟨hS.1, hS.2.1⟩ e he heZ Dv s d J₁ h₁ beta
  obtain ⟨hst₂, hst₂r⟩ := cell_strict_transforms_agree_at_datum_points O pi hpi u a b ha S hS e he
    heZ Dv hinf s d J₁ J₂ h₁ h₂ (congrFun hJ) beta D hm hst₁ hst₁r
  obtain ⟨f, G, hf, hG⟩ := concrete_two_chart_glued_generators_exist O pi hpi u a b ha beta D
  have hdD : curveDataDegree D = d := hdegD.trans hdeg
  have hmax : IsLocalRing.maximalIdeal (ConcreteSurface O pi u a b) = Ideal.span
      {surfaceT O pi u a b, surfaceX O pi u a b} := by
    rw [← S.parameters, hS.1, hS.2.1]
  have : (Ideal.span ({surfaceT O pi u a b, surfaceX O pi u a b} : Set
      (ConcreteSurface O pi u a b))).IsMaximal := hmax ▸ IsLocalRing.maximalIdeal.isMaximal _
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  have hreg := concrete_surface_regular_pair_tx O pi hpi.ne_zero u a b ha
  have hregSwap := concrete_surface_regular_pair_xt O pi hpi.ne_zero u a b ha
  obtain ⟨hinst1, hinst2, -⟩ := two_chart_datum_concrete_instances O pi hpi u a b ha beta D
  have hL := fun s ↦ (hinst1 s).2
  have hR := fun s ↦ (hinst2 s).2
  have hregS : RegularParameterPair (ConcreteSurface O pi u a b) S.t S.x := by
    rw [hS.1, hS.2.1]; exact hreg
  -- an ideal of the cell with the strict transforms of `D` is `(f)`
  have key : ∀ J ∈ fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv,
      (∀ s, strictTransformAt (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
          (surfaceX O pi u a b) (leftPoint D s) d J = Ideal.span {leftData D s}) →
      (∀ s, strictTransformAt (ConcreteSurface O pi u a b) (surfaceX O pi u a b)
          (surfaceT O pi u a b) (rightPoint D s) d J = Ideal.span {rightData D s}) →
      J = Ideal.span {f} := by
    rintro J ⟨⟨⟨g, rfl⟩, -⟩, hJc⟩ hl hr
    have hmul := has_tangent_divisor_multiplicity O (ConcreteSurface O pi u a b) S hregS _ d Dv hJc
    rw [HasMultiplicity, hmax] at hmul
    subst hdD
    exact parent_ideal_unique_of_level_lattice (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b) hreg hregSwap beta _ G
      (two_chart_left_generators_regular_on_overlap (ConcreteSurface O pi u a b)
          (surfaceT O pi u a b) (surfaceX O pi u a b) beta D _ G hG hreg hregSwap) f hf g
      (strict_transforms_give_level_lattice_membership (ConcreteSurface O pi u a b)
          (surfaceT O pi u a b) (surfaceX O pi u a b) beta D _ G hG g
        ((Ideal.span_singleton_le_iff_mem _).1 hmul.1) hl hr)
      fun h ↦ hmul.2 ((Ideal.span_singleton_le_iff_mem _).2 h)
  exact (key J₁ h₁ hst₁ hst₁r).trans (key J₂ h₂ hst₂ hst₂r).symm

/-- The strict transform map is a bijection from the fixed tangent cell onto the
product of the child ideal sets over the support of `Dv`. -/
theorem strict_transform_bijOn_child_ideals (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]
    [Finite (IsLocalRing.ResidueField O)] (pi : O) (hpi : Irreducible pi) (u : (TwoSeries O)ˣ)
    (a b : ℕ) (ha : 0 < a) [IsDomain (ConcreteSurface O pi u a b)]
        [IsRegularLocalRing (ConcreteSurface O pi u a b)] (S : SurfaceData O
            (ConcreteSurface O pi u a b))
    (hS : S.t = surfaceT O pi u a b ∧ S.x = surfaceX O pi u a b ∧ S.a = a ∧ S.b = b)
    (e : (tChart O pi u a b ⧸ tExc O pi u a b) ≃+* Polynomial (IsLocalRing.ResidueField
        (ConcreteSurface O pi u a b)))
    (he : ∀ r : ConcreteSurface O pi u a b, e (Ideal.Quotient.mk (tExc O pi u a b)
        (tBase O pi u a b r)) = Polynomial.C (IsLocalRing.residue (ConcreteSurface O pi u a b) r))
    (heZ : e (Ideal.Quotient.mk (tExc O pi u a b) (tSlope O pi u a b)) = Polynomial.X)
    (Dv : ExceptionalDivisor (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)))
    (hinf : (infinityPoint (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b)).IsPrime) (s : State) (d : ℕ) (hd : 0 < d)
    (hs : (∃ c : ℕ, s = State.single a c ∧ b = 0) ∨ (∃ c h : ℕ, s = State.crossing a b c h ∧ 0 < b))
    (hdc : d ≤ stateContactT s) (hdh : ∀ h : ℕ, stateContactX s = some h → d ≤ h)
    (hDinf : 0 < Dv none ↔ d < stateContactT s)
    (hDzero : ∀ h : ℕ, stateContactX s = some h →
      (0 < Dv (zeroDirection (IsLocalRing.ResidueField (ConcreteSurface O pi u a b))) ↔ d < h))
    (hdeg : exceptionalDegree (IsLocalRing.ResidueField (ConcreteSurface O pi u a b)) Dv = d) :
    Set.BijOn (fun J Q => divisorStrictTransform (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
        (surfaceX O pi u a b) e Dv hinf d J Q)
      (fixedTangentCell O (ConcreteSurface O pi u a b) S s d Dv)
      (Set.pi Set.univ (childIdealSet (ConcreteSurface O pi u a b) (surfaceT O pi u a b)
          (surfaceX O pi u a b) e Dv hinf s d)) := by
  refine ⟨strict_transform_mapsTo_child_ideals O pi hpi u a b ha S hS e he heZ Dv hinf s d,
    strict_transform_injOn_fixed_tangent_cell O pi hpi u a b ha S hS e he heZ Dv hinf s d hdeg,
    fun I hI ↦ ?_⟩
  rw [Set.mem_univ_pi] at hI
  obtain ⟨beta⟩ := actual_blowup_restriction_exists (ConcreteSurface O pi u a b)
      (surfaceT O pi u a b) (surfaceX O pi u a b)
  obtain ⟨D, hm, hcl⟩ := child_ideals_curve_datum O pi hpi u a b ha e he heZ Dv hinf s d beta I hI
  obtain ⟨ht, hx, ha', hb'⟩ := hS
  rcases S with ⟨p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15⟩
  dsimp only at ht hx ha' hb'
  subst ht hx
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceT O pi u a b)
      (surfaceX O pi u a b)
  have := blowupChart_concrete_isNoetherianRing O pi u a b (surfaceX O pi u a b)
      (surfaceT O pi u a b)
  have hdD : curveDataDegree D = d := hdeg ▸ (matches_divisor_degree O (ConcreteSurface O pi u a b)
    ⟨p1, p2, surfaceT O pi u a b, surfaceX O pi u a b, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14,
        p15⟩ beta D Dv e he heZ hm).symm
  obtain ⟨f, G, hf, hG⟩ := concrete_two_chart_glued_generators_exist O pi hpi u a b ha beta D
  obtain ⟨h1, h2⟩ := concrete_strict_transforms_are_prescribed O pi hpi u a b ha beta D f G hf hG
  rw [hdD] at h1 h2
  have hIf := hcl f h1 h2
  subst hdD
  exact ⟨_, global_function_mem_cell O pi hpi u a b ha _ ⟨rfl, rfl, ha', hb'⟩ e he heZ Dv hinf s _
    hd hs hdc hdh hDinf hDzero beta D hm rfl f G hf hG I hI hIf, funext hIf⟩

end SurfaceBlowup