The induced triple of a concatenation

The induced triple of a list of centres (AnalyticTriple.induced: the marked transform and the total transform of the boundary at the last stage) decomposes along the constructors of the list: the empty list induces the triple itself (induced_nil), and cons hY R induces what R induces from the triple after the head blow-up (induced_cons). The head triple is read as the induced triple of the one-element list cons hY nil; its ideal is the marked transform of the first step, birationalTransform hY (isBlowUp_blowUpπ ψ₀ hY) ⟨𝓘, m⟩ (cons_markedTransformSeq_one, cons_markedTransformSeq_last: the chart witnesses of the succession are chosen, so the identification across successions is a theorem, birationalTransform_congr, not a rfl), and its boundary the total transform of the first step; the order clauses of the head and of the tail come from isOfOrderGe_cons_iff.

The consequence used by the rounds on the nonmonomial part: a pointwise bound on the order of the nonmonomial part of the induced ideal at the last stage passes through a concatenation L.concat L' from the bound for L' at the triple induced by L (nonmonomialOrdLe_induced_concat), by induction on L with the cons case definitional, so no transport across the type equality stage_last_concat is needed. The triple (X_j, I_j, E_j) carried along a composite sequence is Kollár's [Kol07, 104, Step 2.1].

theorem Manifold.AnalyticTriple.induced_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T₁ T₂ : AnalyticTriple ψ₀ M} (e : T₁ = T₂) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (h₁ : L.toSuccession.IsOfOrderGe T₁.I s T₁.F.idealSheaf) (h₂ : L.toSuccession.IsOfOrderGe T₂.I s T₂.F.idealSheaf) : T₁.induced s L h₁ = T₂.induced s L h₂

The induced triple of equal triples (on the same manifold) is the same triple.

theorem Manifold.AnalyticTriple.induced_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (h : (AnalyticManifold.BlowUpSequence.nil M).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : T.induced m (AnalyticManifold.BlowUpSequence.nil M) h = T

The empty list induces the triple itself (the marked and total transforms at index 0).

theorem Manifold.AnalyticTriple.isOfOrderGe_head_of_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) {R : AnalyticManifold.BlowUpSequence ψ₀ (blowUp ψ₀ hY)} (h : (AnalyticManifold.BlowUpSequence.cons hY R).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf

The head of a list of order ≥ m, as the one-element list, is of order ≥ m (isOfOrderGe_cons_iff: the head clauses do not mention the tail).

@[reducible, inline]

noncomputable abbrev Manifold.AnalyticTriple.headTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) (h₁ : (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : AnalyticTriple ψ₀ (blowUp ψ₀ hY)

The triple after the head blow-up: the induced triple of the one-element list.

Equations

• T.headTriple m hY h₁ = T.induced m (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (Manifold.blowUp ψ₀ hY))) h₁

theorem Manifold.AnalyticTriple.headTriple_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) (h₁ : (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (T.headTriple m hY h₁).I = (MarkedIdealSheaf.birationalTransform hY ⋯ { I := T.I, m := m }).I

The ideal of the head triple is the marked transform of the first step (cons_markedTransformSeq_last at the one-element list).

theorem Manifold.AnalyticTriple.headTriple_F {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) (h₁ : (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (T.headTriple m hY h₁).F = HypersurfaceFamily.totalTransform (⇑(blowUpπ ψ₀ hY)) hY.idealSheaf.support T.F

The head triple's divisor is the total transform of the first step (cons_totalTransformSeqFromAux_succ at the one-element list).

theorem Manifold.AnalyticTriple.headTriple_F_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) (h₁ : (AnalyticManifold.BlowUpSequence.cons hY (AnalyticManifold.BlowUpSequence.nil (blowUp ψ₀ hY))).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (T.headTriple m hY h₁).F.idealSheaf = AnalyticManifold.IdealSheaf.reducedTransform (blowUpπ ψ₀ hY) T.F.idealSheaf hY.idealSheaf

The boundary ideal of the head triple is the reduced transform of the boundary ideal (the total transform of [Kol07, Definition 25] along one blow-up).

theorem Manifold.AnalyticTriple.isOfOrderGe_tail_of_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) {R : AnalyticManifold.BlowUpSequence ψ₀ (blowUp ψ₀ hY)} (h : (AnalyticManifold.BlowUpSequence.cons hY R).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : R.toSuccession.IsOfOrderGe (T.headTriple m hY ⋯).I m (T.headTriple m hY ⋯).F.idealSheaf

The tail of a list of order ≥ m is of order ≥ m for the head triple.

theorem Manifold.AnalyticTriple.induced_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) {R : AnalyticManifold.BlowUpSequence ψ₀ (blowUp ψ₀ hY)} (h : (AnalyticManifold.BlowUpSequence.cons hY R).toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : T.induced m (AnalyticManifold.BlowUpSequence.cons hY R) h = (T.headTriple m hY ⋯).induced m R ⋯

The induced triple of a cons: what cons hY R induces from T is what R induces from the head triple (the marked transform at the last stage through the transform of the first step, cons_markedTransformSeq_last; the total transform, cons_totalTransformSeqFromAux_succ).

def Hironaka.Manifold.BMOmod.NonmonomialOrdLe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (S : Manifold.AnalyticTriple ψ₀ N) (d : ℕ) : Prop

The nonmonomial part of the ideal of a triple has order ≤ d at every point: the invariant carried along the descent of the rounds on the nonmonomial part.

Equations

• Hironaka.Manifold.BMOmod.NonmonomialOrdLe S d = ∀ (x : ↑↧N.carrier), Manifold.IdealSheaf.ord (Hironaka.Manifold.BMO.nonmonomialTriple S).I x ≤ ↑d

theorem Hironaka.Manifold.BMOmod.NonmonomialOrdLe.weaken {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {S : Manifold.AnalyticTriple ψ₀ N} {d d' : ℕ} (h : NonmonomialOrdLe S d) (hdd : d ≤ d') : NonmonomialOrdLe S d'

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_induced_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (L' : AnalyticManifold.BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) (m d : ℕ) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (hL' : L'.toSuccession.IsOfOrderGe (T.induced m L hL).I m (T.induced m L hL).F.idealSheaf) (hC : (L.concat L').toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : NonmonomialOrdLe ((T.induced m L hL).induced m L' hL') d → NonmonomialOrdLe (T.induced m (L.concat L') hC) d

The pointwise bound transports through a concatenation: if the nonmonomial part of the ideal induced by L' from the triple induced by L is of order ≤ d everywhere, so is the one induced by L.concat L' — by induction on L, the cons case through induced_cons (definitional at the constructors; no cast across stage_last_concat).