The Jacobian ledger of a blow-up sequence

Every blow-up sequence whose centres have simple normal crossings with the accumulated total transform carries a Jacobian ledger (Kollár's condition that "the centers Z_i have simple normal crossings with E", under which the total transform Π⁻¹_tot(E) is a simple normal crossings divisor [Kol07, Definition 25]): for a list of centres L : CenterList ψ₀ M and a start family F, if at every stage the centre has simple normal crossings with the current total transform (HasSncWith), the composite σ^r : M_r → M has a ledger (JacobianLedger, Hironaka/Resolution/Analytic/BM97/Ledger.lean) relative to the final total transform totalTransformSeqFrom F (Fin.last _), the exceptional members being those off the range of originalIdx — the strict transforms of the original members are the non-exceptional ones (jacobianLedger_composite_of_forall_hasSncWith). The proof is the induction along the list with the step of Hironaka/Resolution/Analytic/BM97/LedgerStep.lean (JacobianLedger.step) at every blow-up, r = 0 being the identity (jacobianStalk = ⊤, s = ∅; jacobianLedger_id): the joint statement isSnc_and_jacobianLedger_stageMap_totalTransformSeqFrom carries the simple normal crossings property of the boundary family along (isSnc_totalTransform), reads each blowing-up of the succession in the fixed chart ψ₀ through IsBlowUp.congr_chart and IsClosedSubmanifold.congr_chart, and keeps the exceptional index set in the form (range originalIdx)ᶜ by compl_range_toLex_inl. The instance used for the Jacobian clause of the principalization theorem (jacobianLedger_composite_of_forall_hasSncWith_empty, Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean) is the empty start, exc = univ.

theorem Hironaka.Manifold.jacobianLedger_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) : JacobianLedger ψ₀ (⇑ContMDiffMap.id) F ∅

The start of the induction, r = 0: the identity carries the empty ledger relative to any simple normal crossings family — jacobianStalk id x = ⊤ (the identity being a local analytic isomorphism) is the empty product.

theorem Hironaka.Manifold.compl_range_toLex_inl {α : Type u_2} {β : Type u_3} (g : α → β) : (Set.range fun (a : α) => toLex (Sum.inl (g a)))ᶜ = (fun (b : β) => toLex (Sum.inl b)) '' (Set.range g)ᶜ ∪ {toLex (Sum.inr PUnit.unit)}

The bookkeeping of the exceptional indices: the members of the total transform off the range of inl ∘ g are the strict transforms of the members off the range of g together with the new exceptional divisor inr.

theorem Hironaka.Manifold.isSnc_and_jacobianLedger_stageMap_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (h3 : ∀ (i : Fin S.length), Manifold.HypersurfaceFamily.HasSncWith ψ₀ (S.totalTransformSeqFrom F i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (i : Fin (S.length + 1)) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (S.totalTransformSeqFrom F i) ∧ JacobianLedger ψ₀ (⇑(S.stageMap i)) (S.totalTransformSeqFrom F i) (Set.range (S.originalIdx F i))ᶜ

The joint induction along a blow-up sequence (the hypothesis "the centres have simple normal crossings with the boundary" of [Kol07, Definition 25]): at every stage i the boundary family F_i = totalTransformSeqFrom F i is a simple normal crossings family and the partial composite σ^i = stageMap i carries a Jacobian ledger relative to F_i, the exceptional members being those off the range of originalIdx (the strict transforms of the original members are the non-exceptional ones). Fin.induction: the start is the identity's empty ledger; the step is JacobianLedger.step at the i-th blowing-up, read in the fixed chart ψ₀ through IsBlowUp.congr_chart and IsClosedSubmanifold.congr_chart (the codimension stays S.codim i), with isSnc_totalTransform for the simple normal crossings clause and the index bookkeeping compl_range_toLex_inl at the successor.

theorem Hironaka.Manifold.jacobianLedger_composite_of_forall_hasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (h3 : ∀ (i : Fin L.toSuccession.length), Manifold.HypersurfaceFamily.HasSncWith ψ₀ (L.toSuccession.totalTransformSeqFrom F i.castSucc) (Manifold.IdealSheaf.support (L.toSuccession.center i)) (L.toSuccession.codim i)) : JacobianLedger ψ₀ (⇑L.toSuccession.composite) (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length)) (Set.range (L.toSuccession.originalIdx F (Fin.last L.toSuccession.length)))ᶜ

The Jacobian ledger of a blow-up sequence ([Kol07, Definition 25]): every blow-up sequence whose centres have simple normal crossings with the accumulated total transform carries a Jacobian ledger relative to the final total transform, the exceptional members being those off the range of originalIdx. The last stage of the joint induction.

theorem Hironaka.Manifold.jacobianLedger_composite_of_forall_hasSncWith_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) (h3 : ∀ (i : Fin L.toSuccession.length), Manifold.HypersurfaceFamily.HasSncWith ψ₀ (L.toSuccession.totalTransformSeq i.castSucc) (Manifold.IdealSheaf.support (L.toSuccession.center i)) (L.toSuccession.codim i)) : JacobianLedger ψ₀ (⇑L.toSuccession.composite) (L.toSuccession.totalTransformSeq (Fin.last L.toSuccession.length)) Set.univ

The instance used for the Jacobian clause of the principalization theorem: for a list of centres whose centres have simple normal crossings with the accumulated exceptional divisor totalTransformSeq (the empty start), the composite carries a ledger relative to the final family of exceptional divisors with every member exceptional (exc = univ) — the general form at the empty family (isSnc_empty), whose originalIdx has empty range.