The marked transform does not depend on the chart witnesses; order ≥ 1 on cons

FiniteSuccession.markedTransformSeq (Hironaka/Manifold/FiniteSuccession/Basic.lean) is defined through MarkedIdealSheaf.birationalTransform at the witnesses chartAt/codim chosen from isMonoidal (Classical.choose), while the one-step descent lemma of Hironaka/Resolution/Analytic/MaximalContact/OneStepDescent.lean produces the marked transform at the list's model chart ψ and the given codimension. This module shows the two agree, because none of the data of birationalTransform hY h ⟨J, m⟩ depends on the witnesses:

• MarkedIdealSheaf.birationalTransform_congr: the ideal sheaf I_Y of a closed submanifold depends only on the set Y (IsClosedSubmanifold.idealSheaf_congr), hence the marked transform along one blow-down π is the same for any two witnesses (ψ, c), (ψ', c') of "Y is a closed submanifold and π is its blowing-up";
• FiniteSuccession.cons_markedTransformSeq_one: on cons ψ hZ C the first marked transform is birationalTransform hZ (isBlowUp_blowUpπ ψ hZ) ⟨J, m⟩, the form the one-step lemma yields;
• isMarkedOne_cons_zero / isMarkedOne_cons_tail: the two clauses of IsMarkedOne on cons ψ hZ C — the first centre lies in cosupp J, and the tail is IsMarkedOne for the first marked transform (the recursion cons_markedTransformSeq_succ_castSucc).

These are the bookkeeping steps of Kollár's induction "X_{i+1} = X'_{i+1}, the blow-up of the same centre" [Kol07, Theorem 97, proof], for sequences of order ≥ m in the sense of [Kol07, Definition 66].

theorem Manifold.MarkedIdealSheaf.birationalTransform_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y Y' : Set M} {c c' : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ' Y' c') (hYY' : Y = Y') (h : IsBlowUp ψ Y c π) (h' : IsBlowUp ψ' Y' c' π) (J : MarkedIdealSheaf (structureSheaf 𝕜 E M)) : birationalTransform hY h J = birationalTransform hY' h' J

The marked transform π_*^{-1}(J, m) along a blow-down π does not depend on the witnesses (ψ, c) of "Y is a closed submanifold and π its blowing-up": its inputs are the total transform π^*J and the exceptional ideal sheaf π^*I_Y, and I_Y depends only on the set Y (idealSheaf_congr).

theorem AnalyticManifold.FiniteSuccession.cons_markedTransformSeq_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (C : (Manifold.blowUp ψ hZ).FiniteSuccession) (J : M.IdealSheaf) (m : ℕ) : (cons ψ hZ C).markedTransformSeq J m (Fin.succ 0) = (Manifold.MarkedIdealSheaf.birationalTransform hZ ⋯ { I := J, m := m }).I

On cons ψ hZ C the marked transform at stage 1 is birationalTransform at the given witnesses (ψ, c) and the blow-down blowUpπ ψ hZ: the chosen witnesses of isMonoidal give the same value (birationalTransform_congr).

theorem AnalyticManifold.FiniteSuccession.isMarkedOne_cons_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (C : (Manifold.blowUp ψ hZ).FiniteSuccession) {J : M.IdealSheaf} (h : (cons ψ hZ C).IsMarkedOne J) : Z ⊆ Manifold.IdealSheaf.support J

Stage 0 of Kollár's "Z_i^U ⊆ W_i" [Kol07, Theorem 97, proof]: if cons ψ hZ C is of order ≥ 1 for (J, 1), its first centre Z lies in cosupp J.

theorem AnalyticManifold.FiniteSuccession.isMarkedOne_cons_tail {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (C : (Manifold.blowUp ψ hZ).FiniteSuccession) {J : M.IdealSheaf} (h : (cons ψ hZ C).IsMarkedOne J) : C.IsMarkedOne (Manifold.MarkedIdealSheaf.birationalTransform hZ ⋯ { I := J, m := 1 }).I

The later stages: if cons ψ hZ C is of order ≥ 1 for (J, 1), its tail C is of order ≥ 1 for the first marked transform (π_*^{-1}(J, 1), 1) (the recursion of the marked transforms on the constructor form).