/-
Copyright (c) 2026 Resolution. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Elliott (Resolution): formalization performed by Claude Fable 5.1
-/
module

public import Hironaka.Resolution.Algebraic.Hir64.ComponentwiseMainTheorems
import Hironaka.Resolution.Algebraic.Hir64.Corollary1
import Hironaka.Resolution.Algebraic.Hir64.Corollary3
import Hironaka.Resolution.Algebraic.Hir64.ExtendOpen
import Hironaka.Resolution.Algebraic.Hir64.OpenPieceTransport
import Hironaka.Resolution.Algebraic.Kol07.Prop37.Prop37Local
import Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification
import Hironaka.Resolution.Algebraic.Kol07.Thm36.RelativeDimensionConstancy
import Hironaka.Scheme.BlowUpSequence.ConcatCenters
import Hironaka.Scheme.BlowUpSequence.ConcatClauses
import Hironaka.Scheme.BlowUpSequence.OpenTransport
import Hironaka.Scheme.BlowUpSequence.PullbackInduced
import Hironaka.Scheme.BlowUpSequence.PullbackSnc
import Hironaka.Scheme.IdealSheaf.Invertible
import Hironaka.Scheme.IdealSheaf.Order.Basic
import Hironaka.Scheme.IdealSheaf.Order.Invariance
import Hironaka.Scheme.IdealSheaf.StalkIdeal
public import Hironaka.Scheme.Resolution.Defs
import Hironaka.Scheme.Resolution.Basic

/-!
# Hironaka's Corollaries 1 and 3 for every smooth scheme

Hironaka's Corollary 1 [Hir64, Corollary 1, pp. 143–144], the simultaneous trivialization of a
finite system of ideal sheaves, and Corollary 3 [Hir64, Corollary 3, p. 146], the simplification
of an algebraic boundary, are proved in the library for a scheme smooth of a single relative
dimension over the field (`hironaka_corollary1`, `hironaka_corollary3`). This module derives them
for every scheme smooth and of finite type over the field, by the componentwise assembly of
`Hironaka/Resolution/Algebraic/Hir64/ComponentwiseMainTheorems.lean`: the irreducible components
of a smooth Noetherian scheme are disjoint closed opens, each smooth of one relative dimension; the
corollary is applied to a component, its succession is extended by the unit ideal across the
complement (`exists_extend_of_isOpenImmersion`), the untouched remainder embeds into the last stage
(`exists_untouched_embedding`), and the successions concatenate. The clauses of both corollaries
are pointwise, on the centres and on the points of the last stage, which is what the assembly
reads: `IsTrivializingRound` and `IsBoundaryRound` record them relative to the set over which the
centres lie, with `concat` lemmas in the manner of `IsOrderRound.concat`.

The corollaries themselves are stated and proved at the end of the file:

* `AlgebraicGeometry.exists_blowUpSequence_forall_exists_stalkIdeal_weakTransformSeq_eq_top`:
  Corollary 1 for every smooth `X`, in the clauses of `hironaka_corollary1`.
* `AlgebraicGeometry.exists_blowUpSequence_isInvertible_isSncBoundary_radical_comap`:
  Corollary 3 for every smooth `X`, in the clauses of
  `hironaka_corollary3`. Its final clauses are read on the stalks: the radical of the inverse
  image is invertible when every stalk is generated by a nonzerodivisor
  (`isInvertible_of_forall_stalkIdeal_eq_span`), and Definition 2 holds when it holds at every
  point (`isSncBoundary_iff_forall_isSncBoundaryAt`); both transport along open
  immersions through the stalk isomorphisms (`exists_stalkIdeal_comap_eq_span_iff`,
  `IsSncBoundaryAt.comap`), and the radical of an inverse image along an open immersion
  is the inverse image of the radical (`radical_comap_of_isOpenImmersion`).
-/

public section

universe u

open CategoryTheory TopologicalSpace AlgebraicGeometry Scheme Scheme.IdealSheafData
  BlowUpSequence

namespace Hironaka.Sequence

open AlgebraicGeometry Hironaka.Resolution

variable {X Y : Scheme.{u}}

/-! ### Stalks generated by a nonzerodivisor, along an open immersion -/

/-- The stalk of `I` at `u y` is generated by a nonzerodivisor iff the stalk of `I.comap u` at `y`
is, for an open immersion `u`: the stalk map is a ring isomorphism carrying the one ideal to the
other (`stalkIdeal_comap`) and nonzerodivisors to nonzerodivisors
(`MulEquivClass.map_nonZeroDivisors`). -/
theorem exists_stalkIdeal_comap_eq_span_iff (u : Y ⟶ X) [IsOpenImmersion u]
    (I : X.IdealSheafData) (y : Y) :
    (∃ b ∈ nonZeroDivisors (Y.presheaf.stalk y), (I.comap u).stalkIdeal y = Ideal.span {b}) ↔
      ∃ a ∈ nonZeroDivisors (X.presheaf.stalk (u y)), I.stalkIdeal (u y) = Ideal.span {a} := by
  set e : X.presheaf.stalk (u y) ≃+* Y.presheaf.stalk y := stalkEquivOfIsOpenImmersion u y
    with he_def
  set e' : X.presheaf.stalk (u y) →+* Y.presheaf.stalk y :=
    (e : X.presheaf.stalk (u y) →+* Y.presheaf.stalk y) with he'_def
  have he : (I.comap u).stalkIdeal y = (I.stalkIdeal (u y)).map e' := by
    rw [stalkIdeal_comap, he'_def, he_def, stalkEquivOfIsOpenImmersion_toRingHom]
  have he_symm : I.stalkIdeal (u y) = ((I.comap u).stalkIdeal y).map e.symm :=
    stalkIdeal_eq_map_symm_stalkIdeal_comap u I y
  constructor
  · rintro ⟨b, hb, hIb⟩
    refine ⟨e.symm b, ?_, ?_⟩
    · rw [← MulEquivClass.map_nonZeroDivisors e.symm]
      exact Submonoid.mem_map.mpr ⟨b, hb, rfl⟩
    · rw [he_symm, hIb, Ideal.map_span, Set.image_singleton]
  · rintro ⟨a, ha, hIa⟩
    refine ⟨e a, ?_, ?_⟩
    · rw [← MulEquivClass.map_nonZeroDivisors e]
      exact Submonoid.mem_map.mpr ⟨a, ha, rfl⟩
    · rw [he, hIa, Ideal.map_span, Set.image_singleton]
      rfl

/-- The support of the inverse image of `W` along an open immersion is nowhere dense when the
support of `W` is: the preimage of a nowhere dense set under an open continuous map is nowhere
dense. -/
theorem isNowhereDense_support_comap_of_isOpenImmersion (u : Y ⟶ X) [IsOpenImmersion u]
    (W : X.IdealSheafData) (hW : IsNowhereDense (W.support : Set X)) :
    IsNowhereDense ((W.comap u).support : Set Y) := by
  have hpre : ((W.comap u).support : Set Y) = u ⁻¹' (W.support : Set X) :=
    Set.ext fun y => mem_support_comap_iff_apply W u y
  rw [hpre]
  unfold IsNowhereDense at hW ⊢
  refine Set.eq_empty_of_subset_empty ?_
  calc interior (closure (u ⁻¹' (W.support : Set X)))
      ⊆ interior (u ⁻¹' closure (W.support : Set X)) :=
        interior_mono (u.continuous.closure_preimage_subset _)
    _ = u ⁻¹' interior (closure (W.support : Set X)) :=
        (u.isOpenEmbedding.isOpenMap.preimage_interior_eq_interior_preimage u.continuous _).symm
    _ = ∅ := by rw [hW, Set.preimage_empty]

/-! ### Corollary 1: the clauses of a trivializing succession, relative to a set -/

/-- The clauses of Hironaka's Corollary 1 for the system `J` on `Z`, read on the centres and, for
the final clause, on the points of the last stage lying over the set `R ⊆ Z` over which the
centres lie: the centres are regular and irreducible, every weak transform has constant positive
order along them (clause (1)), and at every point of the last stage over `R` some weak transform
has order `0`, that is, is the unit ideal there (clause (2)). -/
structure IsTrivializingRound {Z : Scheme.{u}} (S : BlowUpSequence Z) {e : ℕ}
    (J : Fin e → Z.IdealSheafData) (R : Set Z) : Prop where
  center : ∀ i : Fin S.length,
    IsRegular (S.center i).subscheme ∧ IrreducibleSpace (S.center i).subscheme
  ord_center : ∀ (i : Fin S.length) (j : Fin e), ∃ c : ℕ, 0 < c ∧
    ∀ y ∈ (S.center i).support, (S.weakTransformSeq (J j) i.castSucc).ord y = c
  mem : ∀ (i : Fin S.length) (x : S.stage i.castSucc), x ∈ (S.center i).support →
    S.stageMap i.castSucc x ∈ R
  ord_last : ∀ z : S.last, S.composite z ∈ R →
    ∃ j : Fin e, (S.weakTransformSeq (J j) (Fin.last S.length)).ord z = 0

/-- The empty succession is a trivializing round over the empty set. -/
theorem isTrivializingRound_nil {Z : Scheme.{u}} {e : ℕ} (J : Fin e → Z.IdealSheafData) :
    IsTrivializingRound (nil Z) J ∅ where
  center i := i.elim0
  ord_center i := i.elim0
  mem i := i.elim0
  ord_last _ h := h.elim

/-- Two trivializing rounds concatenate, as in `IsOrderRound.concat`: a round `S₁` over `R₁`
followed by a round `S₂` on its last stage for the last weak transforms, over `R₂`, is a round
over any `R ⊇ R₁` such that `R₂` lies over `R` and every point of the last stage of `S₁` over `R`
is in `R₂` or over `R₁`. At a point of the last stage not over `R₂` the last weak transforms of
`S₂` have the orders of those of `S₁` at the image (`ord_weakTransformSeq_of_stageMap_notMem`). -/
theorem IsTrivializingRound.concat {Z : Scheme.{u}} (S₁ : BlowUpSequence Z)
    (S₂ : BlowUpSequence S₁.last) {e : ℕ} {J : Fin e → Z.IdealSheafData}
    {R₁ : Set Z} {R₂ : Set S₁.last} {R : Set Z}
    (h₁ : IsTrivializingRound S₁ J R₁)
    (h₂ : IsTrivializingRound S₂ (fun j => S₁.weakTransformSeq (J j) (Fin.last _)) R₂)
    (hR₁ : R₁ ⊆ R) (hR₂ : ∀ z₁ ∈ R₂, S₁.composite z₁ ∈ R)
    (hcover : ∀ z₁ : S₁.last, S₁.composite z₁ ∈ R → z₁ ∈ R₂ ∨ S₁.composite z₁ ∈ R₁) :
    IsTrivializingRound (S₁.concat S₂) J R := by
  have hlast := last_concat S₁ S₂
  have hcomp : ∀ z : (S₁.concat S₂).last, (S₁.concat S₂).composite z =
      S₁.composite (S₂.composite (eqToHom hlast z)) := fun z => by
    rw [composite_concat, Scheme.Hom.comp_apply, Scheme.Hom.comp_apply]
  refine ⟨forall_center_concat (fun D => IsRegular D.subscheme ∧ IrreducibleSpace D.subscheme)
      S₁ S₂ h₁.center h₂.center, fun i j => ?_,
    forall_center_concat_mem S₁ S₂ R (fun i x hx => hR₁ (h₁.mem i x hx))
      (fun i x hx => hR₂ _ (h₂.mem i x hx)), ?_⟩
  · exact forall_stage_concat (fun D J' _ => ∃ c : ℕ, 0 < c ∧ ∀ y ∈ D.support, J'.ord y = c)
      S₁ S₂ (J j) ⊥ (fun i => h₁.ord_center i j) (fun i => h₂.ord_center i j) i
  · intro z hz
    rw [hcomp] at hz
    by_cases hz₂ : S₂.composite (eqToHom hlast z) ∈ R₂
    · obtain ⟨j, hj⟩ := h₂.ord_last _ hz₂
      refine ⟨j, ?_⟩
      rw [weakTransformSeq_concat_last]
      exact (ord_comap_of_isIso _ (eqToHom hlast) z).trans hj
    · have h := (hcover _ hz).resolve_left hz₂
      obtain ⟨j, hj⟩ := h₁.ord_last _ h
      refine ⟨j, ?_⟩
      rw [weakTransformSeq_concat_last]
      exact (ord_comap_of_isIso _ (eqToHom hlast) z).trans
        ((ord_weakTransformSeq_of_stageMap_notMem S₂ _ R₂ h₂.mem (Fin.last _) _ hz₂).trans hj)

variable {k : Type u} [Field k] [CharZero k]

/-- Corollary 1 on an irreducible open subscheme `U` of `X`, closed in `X` and contained in the
open `O`, carried out inside an ambient scheme `Z` containing `O` as an open subscheme with closed
range along `w`, for a system `J_Z` on `Z` restricting to `J` on `O`: `hironaka_corollary1` on `U`
(smooth of one relative dimension, since irreducible), extended across the complement
(`exists_extend_of_isOpenImmersion`), with the clauses transported along the stage lifts
(`weakTransformSeq_pullback_of_centersInRange`). -/
theorem exists_trivializingRound_extend (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [FiniteType (X ↘ Spec (.of k))] [IsSeparated (X ↘ Spec (.of k))] [Smooth (X ↘ Spec (.of k))]
    {e : ℕ} (he : 0 < e) (J : Fin e → X.IdealSheafData) (hJ : ∀ j, IsNonzeroEverywhere (J j))
    (U O : X.Opens) (hUO : U ≤ O) (hUc : IsClosed (U : Set X)) [IrreducibleSpace U]
    {Z : Scheme.{u}} [IsNoetherian Z] (w : (O : Scheme.{u}) ⟶ Z) [IsOpenImmersion w]
    (hw : IsClosed (Set.range w)) (J_Z : Fin e → Z.IdealSheafData)
    (hJZ : ∀ j, (J_Z j).comap w = (J j).comap O.ι) :
    ∃ S : BlowUpSequence Z, IsTrivializingRound S J_Z (Set.range (X.homOfLE hUO ≫ w)) := by
  set f := X ↘ Spec (.of k) with hf
  have hnoeth : IsNoetherian X := f.isNoetherian_of_field
  set v : (U : Scheme.{u}) ⟶ Z := X.homOfLE hUO ≫ w with hv
  have hvι : X.homOfLE hUO ≫ O.ι = U.ι := Scheme.homOfLE_ι X hUO
  have hJv : ∀ j, (J_Z j).comap v = (J j).comap U.ι := fun j => by
    rw [hv, comap_comp, hJZ, ← comap_comp, hvι]
  -- Corollary 1 on the irreducible open `U`
  let _ : (U : Scheme.{u}).Over (Spec (.of k)) := ⟨U.ι ≫ f⟩
  have hft : FiniteType ((U : Scheme.{u}) ↘ Spec (.of k)) :=
    inferInstanceAs (FiniteType (U.ι ≫ f))
  have hsep : IsSeparated ((U : Scheme.{u}) ↘ Spec (.of k)) :=
    inferInstanceAs (IsSeparated (U.ι ≫ f))
  obtain ⟨N, hN⟩ := exists_smoothOfRelativeDimension_of_irreducibleSpace (U.ι ≫ f)
  have hN' : ∃ N, SmoothOfRelativeDimension N ((U : Scheme.{u}) ↘ Spec (.of k)) := ⟨N, hN⟩
  obtain ⟨S', hirr', hcen', hlast'⟩ := hironaka_corollary1 (k := k) (U : Scheme.{u}) hN' he
    (fun j => (J j).comap U.ι) (fun j => isNonzeroEverywhere_comap_of_flat U.ι (hJ j))
  -- the extension across the complement of `U`
  set C : Set Z := Set.range v with hC
  have hCclosed : IsClosed C := isClosed_range_homOfLE_comp hUO hUc w hw
  have hcent : ∀ (i : Fin S'.length) (y : S'.stage i.castSucc), y ∈ (S'.center i).support →
      v (S'.stageMap i.castSucc y) ∈ C := fun _ _ _ => ⟨_, rfl⟩
  obtain ⟨S, hpull, hcentC⟩ := exists_extend_of_isOpenImmersion v S' C hCclosed subset_rfl hcent
  subst hpull
  have hCR : S.CentersInRange v := fun i y hy => by
    rw [range_pullbackStageHom]
    exact hcentC i y hy
  have hreg := forall_isRegular_center_of_pullback v S hCR fun i => (hirr' i).1
  have hirrS := forall_irreducibleSpace_center_of_pullback v S hCR fun i => (hirr' i).2
  have hwt : ∀ (j : Fin e) (i : Fin (S.length + 1)),
      (S.pullback v).weakTransformSeq ((J j).comap U.ι) (S.pullbackStageIdx v i) =
        (S.weakTransformSeq (J_Z j) i).comap (S.pullbackStageHom v i) := fun j i => by
    rw [← hJv]
    exact weakTransformSeq_pullback_of_centersInRange S v hCR (J_Z j) i
  -- clause (1) on the centres
  have hb : ∀ (i : Fin S.length) (j : Fin e), ∃ c : ℕ, 0 < c ∧
      ∀ y ∈ (S.center i).support, (S.weakTransformSeq (J_Z j) i.castSucc).ord y = c := by
    rintro ⟨i, hi⟩ j
    obtain ⟨c, hc, hcen⟩ := hcen' (S.pullbackCenterIdx v ⟨i, hi⟩) j
    refine ⟨c, hc, fun x hx => ?_⟩
    obtain ⟨y, rfl⟩ := hCR ⟨i, hi⟩ hx
    have hy : y ∈ ((S.pullback v).center (S.pullbackCenterIdx v ⟨i, hi⟩)).support := by
      rw [center_pullback_mk S v i hi]
      exact (mem_support_comap_iff_apply _ _ _).mpr hx
    have := isOpenImmersion_pullbackStageHom S v (Fin.castSucc ⟨i, hi⟩)
    rw [← ord_comap_of_isOpenImmersion, ← hwt]
    exact hcen y hy
  -- clause (2) at the last stage over `U`
  have hidx : S.pullbackStageIdx v (Fin.last S.length) = Fin.last _ := pullbackStageIdx_last S v
  have hf1 : ∀ z : S.last, S.composite z ∈ C →
      ∃ j : Fin e, (S.weakTransformSeq (J_Z j) (Fin.last S.length)).ord z = 0 := fun z hz => by
    have hz' : z ∈ Set.range (S.pullbackStageHom v (Fin.last _)) := by
      rw [range_pullbackStageHom]
      exact hz
    obtain ⟨y, rfl⟩ := hz'
    have := isOpenImmersion_pullbackStageHom S v (Fin.last _)
    have hlast'' : ∀ y' : (S.pullback v).stage (S.pullbackStageIdx v (Fin.last _)), ∃ j : Fin e,
        ((S.pullback v).weakTransformSeq ((J j).comap U.ι)
          (S.pullbackStageIdx v (Fin.last _))).ord y' = 0 := by
      rw [hidx]
      intro y'
      obtain ⟨j, hj⟩ := hlast' y'
      refine ⟨j, ?_⟩
      rw [ord_eq_ord_stalkIdeal, IsLocalRing.ord_eq_zero_iff]
      exact hj
    obtain ⟨j, hj⟩ := hlast'' y
    refine ⟨j, ?_⟩
    rw [← ord_comap_of_isOpenImmersion, ← hwt]
    exact hj
  exact ⟨S, ⟨fun i => ⟨hreg i, hirrS i⟩, hb, hcentC, hf1⟩⟩

/-- The induction of `exists_orderReductionRound_extend_aux` for Corollary 1: over the closed
opens `O` of `X`, on the number of irreducible components of `X` meeting `O`, the succession
produced on any scheme `Z` containing `O` as an open and closed subscheme along `w`, for a system
`J_Z` on `Z` restricting to `J` on `O`. -/
theorem exists_trivializingRound_extend_aux (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [FiniteType (X ↘ Spec (.of k))] [IsSeparated (X ↘ Spec (.of k))] [Smooth (X ↘ Spec (.of k))]
    {e : ℕ} (he : 0 < e) (J : Fin e → X.IdealSheafData) (hJ : ∀ j, IsNonzeroEverywhere (J j))
    (n : ℕ) :
    ∀ (O : X.Opens), IsClosed (O : Set X) →
      {C ∈ irreducibleComponents X | (C ∩ (O : Set X)).Nonempty}.ncard ≤ n →
      ∀ {Z : Scheme.{u}} [IsNoetherian Z] (w : (O : Scheme.{u}) ⟶ Z) [IsOpenImmersion w],
        IsClosed (Set.range w) →
      ∀ (J_Z : Fin e → Z.IdealSheafData), (∀ j, (J_Z j).comap w = (J j).comap O.ι) →
      ∃ S : BlowUpSequence Z, IsTrivializingRound S J_Z (Set.range w) := by
  induction n with
  | zero =>
    intro O hOc hn Z _ w _ hw J_Z hJZ
    have hO : IsEmpty (O : Scheme.{u}) := ⟨fun o => by
      obtain ⟨_, _, _, _, _, _, _, _, _, hnV'⟩ := exists_disjoint_pieces (k := k) X O hOc o
      omega⟩
    refine ⟨nil Z, ?_⟩
    rw [Set.range_eq_empty w]
    exact isTrivializingRound_nil J_Z
  | succ n ih =>
    intro O hOc hn Z _ w _ hw J_Z hJZ
    by_cases hO : IsEmpty (O : Scheme.{u})
    · refine ⟨nil Z, ?_⟩
      rw [Set.range_eq_empty w]
      exact isTrivializingRound_nil J_Z
    obtain ⟨o⟩ := not_isEmpty_iff.mp hO
    obtain ⟨U, V, hUO, hVO, hUV, hUc, hVc, hUint, hcov, hnV'⟩ :=
      exists_disjoint_pieces (k := k) X O hOc o
    have hnV : {C ∈ irreducibleComponents X | (C ∩ (V : Set X)).Nonempty}.ncard ≤ n := by omega
    -- the round on `U`, extended to `Z`
    obtain ⟨S₁, h₁⟩ :=
      exists_trivializingRound_extend (k := k) X he J hJ U O hUO hUc w hw J_Z hJZ
    -- the untouched piece `V` inside the last stage
    obtain ⟨w', hw'oi, hw'comp, hw'range, hw'c, hJw', -⟩ :=
      exists_untouched_embedding hUO hVO hUV hUc hVc w hw S₁ h₁.mem
    have hnoeth₁ : IsNoetherian (S₁.stage (Fin.last S₁.length)) :=
      isNoetherian_stage S₁ (Fin.last S₁.length)
    have hVO' : X.homOfLE hVO ≫ O.ι = V.ι := Scheme.homOfLE_ι X hVO
    have hJ' : ∀ j, (S₁.weakTransformSeq (J_Z j) (Fin.last S₁.length)).comap w' =
        (J j).comap V.ι := fun j => by
      rw [hJw', hJZ, ← comap_comp, hVO']
    obtain ⟨S₂, h₂⟩ := ih V hVc hnV w' hw'c
      (fun j => S₁.weakTransformSeq (J_Z j) (Fin.last S₁.length)) hJ'
    refine ⟨S₁.concat S₂, IsTrivializingRound.concat S₁ S₂ h₁ h₂ ?_ ?_ ?_⟩
    · rintro _ ⟨y, rfl⟩
      exact ⟨X.homOfLE hUO y, (Scheme.Hom.comp_apply _ _ _).symm⟩
    · rintro _ ⟨x, rfl⟩
      refine ⟨X.homOfLE hVO x, ?_⟩
      change (X.homOfLE hVO ≫ w) x = S₁.stageMap (Fin.last S₁.length) (w' x)
      rw [← Scheme.Hom.comp_apply, hw'comp]
    · intro z₁ hz₁
      obtain ⟨o', ho'⟩ := hz₁
      rcases hcov o' with ⟨y, rfl⟩ | ⟨x, rfl⟩
      · exact Or.inr ⟨y, by rw [Scheme.Hom.comp_apply, ho']⟩
      · left
        rw [hw'range]
        change S₁.composite z₁ ∈ Set.range (X.homOfLE hVO ≫ w)
        exact ⟨x, by rw [Scheme.Hom.comp_apply, ho']⟩

/-! ### Corollary 3: the clauses of a boundary simplification, relative to a set -/

omit [CharZero k] in
/-- The clauses of Hironaka's Corollary 3 for the ideal sheaf `W` on `Z`, read on the centres and,
for the final clauses, on the points of the last stage lying over the set `R ⊆ Z` over which the
centres lie: the centres are regular and lie over `W` (clause (ii)) and over `R`; at the points of
the last stage over `R` the scheme is regular (clause (i)) and the radical of the inverse image of
`W` has its stalk generated by a nonzerodivisor and has only normal crossings (clause (iii)). -/
structure IsBoundaryRound {Z : Scheme.{u}} (S : BlowUpSequence Z) (W : Z.IdealSheafData)
    (R : Set Z) : Prop where
  center : ∀ i : Fin S.length, IsRegular (S.center i).subscheme
  mem_support : ∀ (i : Fin S.length) (x : S.stage i.castSucc), x ∈ (S.center i).support →
    S.stageMap i.castSucc x ∈ W.support
  mem : ∀ (i : Fin S.length) (x : S.stage i.castSucc), x ∈ (S.center i).support →
    S.stageMap i.castSucc x ∈ R
  isRegularAt_last : ∀ z : S.last, S.composite z ∈ R → S.last.IsRegularAt z
  stalkIdeal_last : ∀ z : S.last, S.composite z ∈ R →
    ∃ a ∈ nonZeroDivisors (S.last.presheaf.stalk z),
      (W.comap S.composite).radical.stalkIdeal z = Ideal.span {a}
  nc_last : ∀ z : S.last, S.composite z ∈ R →
    IsSncBoundaryAt (W.comap S.composite).radical z

omit [CharZero k] in
/-- The empty succession is a boundary round over the empty set. -/
theorem isBoundaryRound_nil {Z : Scheme.{u}} (W : Z.IdealSheafData) :
    IsBoundaryRound (nil Z) W ∅ where
  center i := i.elim0
  mem_support i := i.elim0
  mem i := i.elim0
  isRegularAt_last _ h := h.elim
  stalkIdeal_last _ h := h.elim
  nc_last _ h := h.elim

omit [CharZero k] in
/-- Two boundary rounds concatenate, as in `IsOrderRound.concat`: a round `S₁` on `Z` for `W` over
`R₁` followed by a round `S₂` on its last stage for the inverse image `W.comap S₁.composite`, over
`R₂`, is a round for `W` over any `R ⊇ R₁` such that `R₂` lies over `R` and every point of the
last stage of `S₁` over `R` is in `R₂` or over `R₁`. The inverse image of `W` along the
concatenation is the inverse image along `S₂` of the inverse image along `S₁`; at a point of the
last stage not over `R₂`, the composite of `S₂` is an open immersion near the point
(`isOpenImmersion_ι_preimage_comp_stageMap`), so the radical of the inverse image is the inverse
image of the radical (`radical_comap_of_isOpenImmersion`) and the final clauses of `S₁` at the
image transport. -/
theorem IsBoundaryRound.concat {Z : Scheme.{u}} [IsNoetherian Z] (S₁ : BlowUpSequence Z)
    (S₂ : BlowUpSequence S₁.last) {W : Z.IdealSheafData} {R₁ : Set Z} {R₂ : Set S₁.last}
    {R : Set Z} (h₁ : IsBoundaryRound S₁ W R₁) (h₂ : IsBoundaryRound S₂ (W.comap S₁.composite) R₂)
    (hR₂c : IsClosed R₂) (hR₁ : R₁ ⊆ R) (hR₂ : ∀ z₁ ∈ R₂, S₁.composite z₁ ∈ R)
    (hcover : ∀ z₁ : S₁.last, S₁.composite z₁ ∈ R → z₁ ∈ R₂ ∨ S₁.composite z₁ ∈ R₁) :
    IsBoundaryRound (S₁.concat S₂) W R := by
  have hnoeth₁ : IsNoetherian S₁.last := isNoetherian_stage S₁ (Fin.last _)
  have hlast : (S₁.concat S₂).last = S₂.stage (Fin.last S₂.length) := last_concat S₁ S₂
  have hcomp' : (S₁.concat S₂).composite =
      eqToHom hlast ≫ S₂.stageMap (Fin.last S₂.length) ≫ S₁.composite := composite_concat S₁ S₂
  have hcomp : ∀ z : (S₁.concat S₂).last, (S₁.concat S₂).composite z =
      S₁.composite (S₂.stageMap (Fin.last S₂.length) (eqToHom hlast z)) := fun z => by
    rw [hcomp', Scheme.Hom.comp_apply, Scheme.Hom.comp_apply]
  have hW : W.comap (S₁.concat S₂).composite =
      ((W.comap S₁.composite).comap (S₂.stageMap (Fin.last S₂.length))).comap (eqToHom hlast) := by
    rw [hcomp', comap_comp, comap_comp]
  -- over the complement of `R₂` the round `S₂` changes nothing
  set V : S₁.last.Opens := ⟨R₂ᶜ, hR₂c.isOpen_compl⟩ with hV
  have hmemV : ∀ (i : Fin S₂.length) (y : S₂.stage i.castSucc), y ∈ (S₂.center i).support →
      S₂.stageMap i.castSucc y ∉ V := fun i y hy hmem => hmem (h₂.mem i y hy)
  set ι := (S₂.stageMap (Fin.last S₂.length) ⁻¹ᵁ V).ι with hι
  have hoi : IsOpenImmersion (ι ≫ S₂.stageMap (Fin.last S₂.length)) :=
    isOpenImmersion_ι_preimage_comp_stageMap S₂ V hmemV (Fin.last _)
  have hoff : ∀ z : S₂.stage (Fin.last S₂.length), S₂.stageMap (Fin.last S₂.length) z ∉ R₂ →
      ∃ q : ((S₂.stageMap (Fin.last S₂.length) ⁻¹ᵁ V) : Scheme.{u}), ι q = z := fun z hz => by
    have hz' : z ∈ Set.range ι := by
      rw [hι, Scheme.Opens.range_ι]
      exact hz
    exact hz'
  refine ⟨forall_center_concat (fun D => IsRegular D.subscheme) S₁ S₂ h₁.center h₂.center,
    forall_center_concat_mem S₁ S₂ (W.support : Set Z) h₁.mem_support (fun i x hx =>
      (mem_support_comap_iff_apply W S₁.composite _).mp (h₂.mem_support i x hx)),
    forall_center_concat_mem S₁ S₂ R (fun i x hx => hR₁ (h₁.mem i x hx))
      (fun i x hx => hR₂ _ (h₂.mem i x hx)), ?_, ?_, ?_⟩
  · -- clause (i) at the last stage
    intro z hz
    rw [hcomp] at hz
    refine (isRegularAt_apply_iff_of_isOpenImmersion (eqToHom hlast) z).mp ?_
    by_cases hz₂ : S₂.stageMap (Fin.last S₂.length) (eqToHom hlast z) ∈ R₂
    · exact h₂.isRegularAt_last _ hz₂
    · have h := (hcover _ hz).resolve_left hz₂
      obtain ⟨q, hq⟩ := hoff (eqToHom hlast z) hz₂
      have h1 : S₁.last.IsRegularAt ((ι ≫ S₂.stageMap (Fin.last S₂.length)) q) := by
        rw [Scheme.Hom.comp_apply, hq]
        exact h₁.isRegularAt_last _ h
      rw [← hq]
      exact (isRegularAt_apply_iff_of_isOpenImmersion ι q).mpr
        ((@isRegularAt_apply_iff_of_isOpenImmersion _ _ _ hoi q).mp h1)
  · -- clause (iii), the stalks
    intro z hz
    rw [hcomp] at hz
    rw [hW, ← radical_comap_of_isOpenImmersion]
    refine (exists_stalkIdeal_comap_eq_span_iff (eqToHom hlast) _ z).mpr ?_
    by_cases hz₂ : S₂.stageMap (Fin.last S₂.length) (eqToHom hlast z) ∈ R₂
    · exact h₂.stalkIdeal_last _ hz₂
    · have h := (hcover _ hz).resolve_left hz₂
      obtain ⟨q, hq⟩ := hoff (eqToHom hlast z) hz₂
      rw [← hq]
      refine (exists_stalkIdeal_comap_eq_span_iff ι _ q).mp ?_
      rw [radical_comap_of_isOpenImmersion, ← comap_comp,
        ← radical_comap_of_isOpenImmersion (ι ≫ S₂.stageMap (Fin.last S₂.length))]
      refine (@exists_stalkIdeal_comap_eq_span_iff _ _ _ hoi _ q).mpr ?_
      rw [Scheme.Hom.comp_apply, hq]
      exact h₁.stalkIdeal_last _ h
  · -- clause (iii), Definition 2
    intro z hz
    rw [hcomp] at hz
    rw [hW, ← radical_comap_of_isOpenImmersion]
    refine IsSncBoundaryAt.comap (eqToHom hlast) z ?_
    by_cases hz₂ : S₂.stageMap (Fin.last S₂.length) (eqToHom hlast z) ∈ R₂
    · exact h₂.nc_last _ hz₂
    · have h := (hcover _ hz).resolve_left hz₂
      obtain ⟨q, hq⟩ := hoff (eqToHom hlast z) hz₂
      rw [← hq]
      refine IsSncBoundaryAt.of_comap ι ?_
      rw [radical_comap_of_isOpenImmersion, ← comap_comp,
        ← radical_comap_of_isOpenImmersion (ι ≫ S₂.stageMap (Fin.last S₂.length))]
      refine @IsSncBoundaryAt.comap _ _ _ hoi _ q ?_
      rw [Scheme.Hom.comp_apply, hq]
      exact h₁.nc_last _ h

/-- Corollary 3 on an irreducible open subscheme `U` of `X`, closed in `X` and contained in the
open `O`, carried out inside an ambient scheme `Z` containing `O` as an open subscheme with closed
range along `w`, for an ideal sheaf `W_Z` on `Z` restricting to `W` on `O`: `hironaka_corollary3`
on `U` (smooth of one relative dimension, since irreducible; the support of `W` restricted to `U`
is nowhere dense), extended across the complement (`exists_extend_of_isOpenImmersion`), with the
clauses transported along the stage lifts: the inverse image of `W_Z` along the composite
restricts along the last stage lift to the inverse image of `W` along the composite on `U`
(`pullbackStageHom_stageMap`). -/
theorem exists_boundaryRound_extend (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [FiniteType (X ↘ Spec (.of k))] [IsSeparated (X ↘ Spec (.of k))] [Smooth (X ↘ Spec (.of k))]
    (W : X.IdealSheafData) (hW : IsNowhereDense (W.support : Set X))
    (U O : X.Opens) (hUO : U ≤ O) (hUc : IsClosed (U : Set X)) [IrreducibleSpace U]
    {Z : Scheme.{u}} [IsNoetherian Z] (w : (O : Scheme.{u}) ⟶ Z) [IsOpenImmersion w]
    (hw : IsClosed (Set.range w)) (W_Z : Z.IdealSheafData) (hWZ : W_Z.comap w = W.comap O.ι) :
    ∃ S : BlowUpSequence Z, IsBoundaryRound S W_Z (Set.range (X.homOfLE hUO ≫ w)) := by
  set f := X ↘ Spec (.of k) with hf
  have hnoeth : IsNoetherian X := f.isNoetherian_of_field
  set v : (U : Scheme.{u}) ⟶ Z := X.homOfLE hUO ≫ w with hv
  have hvι : X.homOfLE hUO ≫ O.ι = U.ι := Scheme.homOfLE_ι X hUO
  have hWv : W_Z.comap v = W.comap U.ι := by rw [hv, comap_comp, hWZ, ← comap_comp, hvι]
  -- Corollary 3 on the irreducible open `U`
  let _ : (U : Scheme.{u}).Over (Spec (.of k)) := ⟨U.ι ≫ f⟩
  have hft : FiniteType ((U : Scheme.{u}) ↘ Spec (.of k)) :=
    inferInstanceAs (FiniteType (U.ι ≫ f))
  have hsep : IsSeparated ((U : Scheme.{u}) ↘ Spec (.of k)) :=
    inferInstanceAs (IsSeparated (U.ι ≫ f))
  obtain ⟨N, hN⟩ := exists_smoothOfRelativeDimension_of_irreducibleSpace (U.ι ≫ f)
  have hN' : ∃ N, SmoothOfRelativeDimension N ((U : Scheme.{u}) ↘ Spec (.of k)) := ⟨N, hN⟩
  have hWU : IsNowhereDense ((W.comap U.ι).support : Set U) :=
    isNowhereDense_support_comap_of_isOpenImmersion U.ι W hW
  obtain ⟨S', hreg', hlastreg', hsupp', hinv', hnc'⟩ :=
    hironaka_corollary3 (k := k) (U : Scheme.{u}) hN' (W.comap U.ι) hWU
  -- the extension across the complement of `U`
  set C : Set Z := Set.range v with hC
  have hCclosed : IsClosed C := isClosed_range_homOfLE_comp hUO hUc w hw
  have hcent : ∀ (i : Fin S'.length) (y : S'.stage i.castSucc), y ∈ (S'.center i).support →
      v (S'.stageMap i.castSucc y) ∈ C := fun _ _ _ => ⟨_, rfl⟩
  obtain ⟨S, hpull, hcentC⟩ := exists_extend_of_isOpenImmersion v S' C hCclosed subset_rfl hcent
  subst hpull
  have hCR : S.CentersInRange v := fun i y hy => by
    rw [range_pullbackStageHom]
    exact hcentC i y hy
  have hreg := forall_isRegular_center_of_pullback v S hCR hreg'
  -- clause (ii): the centres lie over the support of `W_Z`
  have hsupp : ∀ (i : Fin S.length) (x : S.stage i.castSucc), x ∈ (S.center i).support →
      S.stageMap i.castSucc x ∈ W_Z.support := by
    rintro ⟨i, hi⟩ x hx
    obtain ⟨y, rfl⟩ := hCR ⟨i, hi⟩ hx
    have hy : y ∈ ((S.pullback v).center (S.pullbackCenterIdx v ⟨i, hi⟩)).support := by
      rw [center_pullback_mk S v i hi]
      exact (mem_support_comap_iff_apply _ _ _).mpr hx
    have h1 := hsupp' (S.pullbackCenterIdx v ⟨i, hi⟩) y hy
    rw [← hWv, mem_support_comap_iff_apply] at h1
    rw [← Scheme.Hom.comp_apply, pullbackStageHom_stageMap, Scheme.Hom.comp_apply]
    exact h1
  -- the last stage over `U`
  have hidx : S.pullbackStageIdx v (Fin.last S.length) = Fin.last _ := pullbackStageIdx_last S v
  have hWcomp : (W_Z.comap (S.stageMap (Fin.last S.length))).comap
        (S.pullbackStageHom v (Fin.last _)) =
      (W.comap U.ι).comap ((S.pullback v).stageMap (S.pullbackStageIdx v (Fin.last _))) := by
    have h := congrArg (fun g => W_Z.comap g) (pullbackStageHom_stageMap S v (Fin.last _))
    rw [comap_comp, comap_comp, hWv] at h
    exact h
  have hUlast : ∀ y : (S.pullback v).stage (S.pullbackStageIdx v (Fin.last _)),
      ((S.pullback v).stage (S.pullbackStageIdx v (Fin.last _))).IsRegularAt y ∧
      (∃ a ∈ nonZeroDivisors _, ((W.comap U.ι).comap
        ((S.pullback v).stageMap (S.pullbackStageIdx v (Fin.last _)))).radical.stalkIdeal y =
          Ideal.span {a}) ∧
      IsSncBoundaryAt ((W.comap U.ι).comap
        ((S.pullback v).stageMap (S.pullbackStageIdx v (Fin.last _)))).radical y := by
    rw [hidx]
    intro y
    exact ⟨hlastreg'.isRegularAt y, hinv'.exists_mem_nonZeroDivisors_stalkIdeal_eq_span y,
      (isSncBoundary_iff_forall_isSncBoundaryAt _).mp hnc' y⟩
  have hrange : ∀ z : S.stage (Fin.last S.length), S.stageMap (Fin.last S.length) z ∈ C →
      z ∈ Set.range (S.pullbackStageHom v (Fin.last _)) := fun z hz => by
    rw [range_pullbackStageHom]
    exact hz
  have hf1 : ∀ z : S.stage (Fin.last S.length), S.stageMap (Fin.last S.length) z ∈ C →
      (S.stage (Fin.last S.length)).IsRegularAt z := fun z hz => by
    obtain ⟨y, rfl⟩ := hrange z hz
    have := isOpenImmersion_pullbackStageHom S v (Fin.last _)
    exact (isRegularAt_apply_iff_of_isOpenImmersion _ y).mpr (hUlast y).1
  have hf2 : ∀ z : S.stage (Fin.last S.length), S.stageMap (Fin.last S.length) z ∈ C →
      ∃ a ∈ nonZeroDivisors ((S.stage (Fin.last S.length)).presheaf.stalk z),
        (W_Z.comap (S.stageMap (Fin.last S.length))).radical.stalkIdeal z = Ideal.span {a} :=
    fun z hz => by
    obtain ⟨y, rfl⟩ := hrange z hz
    have := isOpenImmersion_pullbackStageHom S v (Fin.last _)
    refine (exists_stalkIdeal_comap_eq_span_iff _ _ y).mp ?_
    rw [radical_comap_of_isOpenImmersion, hWcomp]
    exact (hUlast y).2.1
  have hf3 : ∀ z : S.stage (Fin.last S.length), S.stageMap (Fin.last S.length) z ∈ C →
      IsSncBoundaryAt (W_Z.comap (S.stageMap (Fin.last S.length))).radical z :=
    fun z hz => by
    obtain ⟨y, rfl⟩ := hrange z hz
    have := isOpenImmersion_pullbackStageHom S v (Fin.last _)
    refine IsSncBoundaryAt.of_comap _ ?_
    rw [radical_comap_of_isOpenImmersion, hWcomp]
    exact (hUlast y).2.2
  exact ⟨S, ⟨hreg, hsupp, hcentC, hf1, hf2, hf3⟩⟩

/-- The induction of `exists_orderReductionRound_extend_aux` for Corollary 3: over the closed
opens `O` of `X`, on the number of irreducible components of `X` meeting `O`, the succession
produced on any scheme `Z` containing `O` as an open and closed subscheme along `w`, for an ideal
sheaf `W_Z` on `Z` restricting to `W` on `O`. -/
theorem exists_boundaryRound_extend_aux (X : Scheme.{u}) [X.Over (Spec (.of k))]
    [FiniteType (X ↘ Spec (.of k))] [IsSeparated (X ↘ Spec (.of k))] [Smooth (X ↘ Spec (.of k))]
    (W : X.IdealSheafData) (hW : IsNowhereDense (W.support : Set X)) (n : ℕ) :
    ∀ (O : X.Opens), IsClosed (O : Set X) →
      {C ∈ irreducibleComponents X | (C ∩ (O : Set X)).Nonempty}.ncard ≤ n →
      ∀ {Z : Scheme.{u}} [IsNoetherian Z] (w : (O : Scheme.{u}) ⟶ Z) [IsOpenImmersion w],
        IsClosed (Set.range w) →
      ∀ (W_Z : Z.IdealSheafData), W_Z.comap w = W.comap O.ι →
      ∃ S : BlowUpSequence Z, IsBoundaryRound S W_Z (Set.range w) := by
  induction n with
  | zero =>
    intro O hOc hn Z _ w _ hw W_Z hWZ
    have hO : IsEmpty (O : Scheme.{u}) := ⟨fun o => by
      obtain ⟨_, _, _, _, _, _, _, _, _, hnV'⟩ := exists_disjoint_pieces (k := k) X O hOc o
      omega⟩
    refine ⟨nil Z, ?_⟩
    rw [Set.range_eq_empty w]
    exact isBoundaryRound_nil W_Z
  | succ n ih =>
    intro O hOc hn Z _ w _ hw W_Z hWZ
    by_cases hO : IsEmpty (O : Scheme.{u})
    · refine ⟨nil Z, ?_⟩
      rw [Set.range_eq_empty w]
      exact isBoundaryRound_nil W_Z
    obtain ⟨o⟩ := not_isEmpty_iff.mp hO
    obtain ⟨U, V, hUO, hVO, hUV, hUc, hVc, hUint, hcov, hnV'⟩ :=
      exists_disjoint_pieces (k := k) X O hOc o
    have hnV : {C ∈ irreducibleComponents X | (C ∩ (V : Set X)).Nonempty}.ncard ≤ n := by omega
    -- the round on `U`, extended to `Z`
    obtain ⟨S₁, h₁⟩ := exists_boundaryRound_extend (k := k) X W hW U O hUO hUc w hw W_Z hWZ
    -- the untouched piece `V` inside the last stage
    obtain ⟨w', hw'oi, hw'comp, hw'range, hw'c, -, -⟩ :=
      exists_untouched_embedding hUO hVO hUV hUc hVc w hw S₁ h₁.mem
    have hnoeth₁ : IsNoetherian (S₁.stage (Fin.last S₁.length)) :=
      isNoetherian_stage S₁ (Fin.last S₁.length)
    have hVO' : X.homOfLE hVO ≫ O.ι = V.ι := Scheme.homOfLE_ι X hVO
    have hW' : (W_Z.comap (S₁.stageMap (Fin.last S₁.length))).comap w' = W.comap V.ι := by
      rw [← comap_comp, hw'comp, comap_comp, hWZ, ← comap_comp, hVO']
    obtain ⟨S₂, h₂⟩ := ih V hVc hnV w' hw'c (W_Z.comap (S₁.stageMap (Fin.last S₁.length))) hW'
    refine ⟨S₁.concat S₂, IsBoundaryRound.concat S₁ S₂ h₁ h₂ hw'c ?_ ?_ ?_⟩
    · rintro _ ⟨y, rfl⟩
      exact ⟨X.homOfLE hUO y, (Scheme.Hom.comp_apply _ _ _).symm⟩
    · rintro _ ⟨x, rfl⟩
      refine ⟨X.homOfLE hVO x, ?_⟩
      change (X.homOfLE hVO ≫ w) x = S₁.stageMap (Fin.last S₁.length) (w' x)
      rw [← Scheme.Hom.comp_apply, hw'comp]
    · intro z₁ hz₁
      obtain ⟨o', ho'⟩ := hz₁
      rcases hcov o' with ⟨y, rfl⟩ | ⟨x, rfl⟩
      · exact Or.inr ⟨y, by rw [Scheme.Hom.comp_apply, ho']⟩
      · left
        rw [hw'range]
        change S₁.composite z₁ ∈ Set.range (X.homOfLE hVO ≫ w)
        exact ⟨x, by rw [Scheme.Hom.comp_apply, ho']⟩

end Hironaka.Sequence

end

@[expose] public section

universe u

open CategoryTheory AlgebraicGeometry Scheme.IdealSheafData Scheme

namespace AlgebraicGeometry

/-- **Hironaka's Corollary 1** [Hir64, Corollary 1, pp. 143–144], the trivialization of a system of
coherent sheaves of ideals. Let `X` be a smooth algebraic `k`-scheme (`AlgScheme k`), `k` of
characteristic zero, and `J_1, …, J_e` (`e ≥ 1`) ideal sheaves on `X` with nonzero stalks. Then
there is a finite succession of monoidal transformations `f_i : X_{i+1} → X_i` with non-singular
irreducible centres `D_i ⊆ X_i` (`BlowUpSequence.HasRegularIrreducibleCenters`) such that
* (1) every weak transform `J_j(i)` of every `J_j` has a constant positive order along `D_i`
  (`BlowUpSequence.HasConstantPositiveOrderAlongCenters`);
* (2) at every point of the end result `X_r` at least one of the weak transforms `J_j(r)` is the
  unit ideal.

Relation to the source.
* **Translation.** The weak transforms are those of Main Theorem II
  (`exists_blowUpSequence_ord_weakTransformSeq_lt`): `S.weakTransformSeq (J j) i` is Hironaka's
  $J_j(i)$. "$\nu(J_j(i)_y)$ is a positive constant for the points $y$ of $D(i)$" is `ord` equal to
  a natural number `c` with `0 < c` at every point of the support of the centre ($\nu$ is
  integer-valued on non-zero ideals), and his $J_j(r)_x = \mathcal{O}_{X(r),x}$ is
  `(S.weakTransformSeq (J j) (Fin.last S.length)).stalkIdeal x = ⊤`, read on the stalk. His
  $e \ge 1$ is `0 < e`.
* **Translation.** `[Smooth (X.left ↘ Spec (.of k))]` is Hironaka's "non-singular": for a scheme of
  finite type over the perfect field `k` the two agree (smoothness gives the regularity of every
  local ring, and a non-singular such scheme is smooth).
* **Interpretation.** Hironaka's "coherent sheaves of non-zero ideals" are read as ideal sheaves
  with nonzero stalks (`hJ`), as in Main Theorem II.
* **Restatement.** The regularity of the local rings of `X` is not a separate hypothesis: it follows
  from smoothness over the perfect field `k`.

Source statement: [Hir64, Corollary 1, pp. 143–144] -/
theorem exists_blowUpSequence_forall_exists_stalkIdeal_weakTransformSeq_eq_top
    {k : Type u} [Field k] [CharZero k] (X : AlgScheme k) [Smooth (X.left ↘ Spec (.of k))]
    {e : ℕ} (he : 0 < e) (J : Fin e → X.left.IdealSheafData)
    (hJ : ∀ j, IsNonzeroEverywhere (J j)) :
    ∃ S : BlowUpSequence X.left,
      -- non-singular irreducible centres
      S.HasRegularIrreducibleCenters ∧
      -- (1)
      (∀ j, S.HasConstantPositiveOrderAlongCenters (J j)) ∧
      -- (2)
      ∀ x : S.last, ∃ j, (S.weakTransformSeq (J j) (Fin.last S.length)).stalkIdeal x = ⊤ := by
  have hnoeth : IsNoetherian X.left := (X.left ↘ Spec (.of k)).isNoetherian_of_field
  have hrange : Set.range (⊤ : X.left.Opens).ι = Set.univ := by
    rw [Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_top]
  obtain ⟨S, hS⟩ := Hironaka.Sequence.exists_trivializingRound_extend_aux (k := k) X.left he J hJ
    _ ⊤ (by rw [TopologicalSpace.Opens.coe_top]; exact isClosed_univ) le_rfl
    (⊤ : X.left.Opens).ι (by rw [hrange]; exact isClosed_univ) J (fun _ => rfl)
  have hx : ∀ x : S.stage (Fin.last S.length), S.stageMap (Fin.last S.length) x ∈ Set.univ →
      ∃ j : Fin e, (S.weakTransformSeq (J j) (Fin.last S.length)).stalkIdeal x = ⊤ :=
    fun x hx => by
    obtain ⟨j, hj⟩ := hS.ord_last x (by rw [hrange]; exact hx)
    refine ⟨j, ?_⟩
    rwa [ord_eq_ord_stalkIdeal, IsLocalRing.ord_eq_zero_iff] at hj
  exact ⟨S, hS.center, fun j i => hS.ord_center i j, fun x => hx x (Set.mem_univ _)⟩

/-- **Hironaka's Corollary 3** [Hir64, Corollary 3, p. 146], the simplification of an algebraic
boundary. Let `X` be a smooth algebraic `k`-scheme (`AlgScheme k`), `k` of characteristic zero, and
`W` a nowhere dense closed subscheme of `X`, given by its ideal sheaf. Then there is a finite
succession of monoidal transformations `f_i : X_{i+1} → X_i` with non-singular centres `D_i ⊆ X_i`
such that
* (i) the end result `X_r` is non-singular;
* (ii) every centre lies over `W`: `D_i ⊆ f̄_i⁻¹(W)`, where `f̄_i = f_0 ∘ ⋯ ∘ f_{i-1} : X_i → X`;
* (iii) the associated reduced scheme `red(f̄_r⁻¹(W))` of `f̄_r⁻¹(W)` is defined by an invertible
  sheaf of ideals on `X_r` and has only normal crossings.

Hironaka asks nothing of `W` beyond nowhere density; `W` may be empty (the unit ideal sheaf, of
nowhere dense support), for which the empty succession satisfies every clause.

Relation to the source.
* **Translation.** $\bar f_i$ is `S.stageMap i.castSucc` and $\bar f_r$ is `S.composite`. The
  associated reduced scheme $\mathrm{red}(\bar f_r^{-1}(W))$ is the radical
  `(W.comap S.composite).radical` of the inverse image ideal sheaf; "invertible" is `IsInvertible`
  (generated on an affine neighbourhood of every point by a nonzerodivisor, an effective Cartier
  divisor; on the locally Noetherian `X_r` this is the stalkwise condition that every stalk is
  generated by a nonzerodivisor of the local ring, `isInvertible_iff_forall_stalkIdeal_eq_span`),
  and "has only normal crossings" is Hironaka's Definition 2 (`IsSncBoundary`).
* **Translation.** Clause (ii) is read on points: every point of a centre maps into the support of
  `W`; since $D_i$ is non-singular, hence reduced, this is the inclusion
  $D_i \subseteq \bar f_i^{-1}(W)$ of subschemes.
* **Interpretation.** Hironaka's "nowhere dense" for the closed subscheme $W$ of $X$ is read
  topologically, of its support (`IsNowhereDense (W.support : Set X.left)`).
* **Translation.** `[Smooth (X.left ↘ Spec (.of k))]` is Hironaka's "non-singular" for `X`: for a
  scheme of finite type over the perfect field `k` the two agree (smoothness gives the regularity of
  every local ring, and a non-singular such scheme is smooth).
* **Restatement.** The regularity of the local rings of `X` is not a separate hypothesis: it follows
  from smoothness over the perfect field `k`.

Source statement: [Hir64, Corollary 3, p. 146] -/
theorem exists_blowUpSequence_isInvertible_isSncBoundary_radical_comap
    {k : Type u} [Field k] [CharZero k] (X : AlgScheme k) [Smooth (X.left ↘ Spec (.of k))]
    (W : X.left.IdealSheafData) (hW : IsNowhereDense (W.support : Set X.left)) :
    ∃ S : BlowUpSequence X.left,
      -- non-singular centres
      (∀ i : Fin S.length, IsRegular (S.center i).subscheme) ∧
      -- (i)
      IsRegular S.last ∧
      -- (ii)
      (∀ i : Fin S.length, ∀ x ∈ (S.center i).support, S.stageMap i.castSucc x ∈ W.support) ∧
      -- (iii)
      (W.comap S.composite).radical.IsInvertible ∧
      (W.comap S.composite).radical.IsSncBoundary := by
  have hnoeth : IsNoetherian X.left := (X.left ↘ Spec (.of k)).isNoetherian_of_field
  have hrange : Set.range (⊤ : X.left.Opens).ι = Set.univ := by
    rw [Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_top]
  obtain ⟨S, hS⟩ := Hironaka.Sequence.exists_boundaryRound_extend_aux (k := k) X.left W hW _ ⊤
    (by rw [TopologicalSpace.Opens.coe_top]; exact isClosed_univ) le_rfl (⊤ : X.left.Opens).ι
    (by rw [hrange]; exact isClosed_univ) W rfl
  have hmem : ∀ z : S.last, S.composite z ∈ Set.range (⊤ : X.left.Opens).ι := fun z => by
    rw [hrange]
    exact Set.mem_univ _
  have hnoethS : IsNoetherian S.last := Hironaka.Resolution.isNoetherian_stage S (Fin.last _)
  exact ⟨S, hS.center, ⟨fun z => hS.isRegularAt_last z (hmem z)⟩, hS.mem_support,
    isInvertible_of_forall_stalkIdeal_eq_span _ fun z => hS.stalkIdeal_last z (hmem z),
    (Hironaka.Sequence.isSncBoundary_iff_forall_isSncBoundaryAt _).mpr fun z =>
      hS.nc_last z (hmem z)⟩

end AlgebraicGeometry