Naturality of the disjoined triple

The disjoined triple of a list (disjoinedTripleOf) is natural for the two operations the independence of the shrinking open compares (functoriality for smooth morphisms [Kol07, 34.1] and the empty blow-up convention [Kol07, 32]):

• pull-back along a local analytic isomorphism h: the disjoined triple of h^* L for the pulled-back triple is the pull-back of the disjoined triple of L along the last-stage lift h_r (the boundary families by totalTransformSeqFrom_last_pullbackLiftLast, the original members by originalIdx_last_pullback_heq, the ideal sheaves by stageMap_last_pullbackLiftLast; [Kol07, 30.1] for the pull-back of a blow-up sequence);
• padding by an empty blow-up: the disjoined triple of cons h∅ (π^* L) (the disjoining list with one more, empty, first round; π : Bl_∅ M → M the blow-down) is an empty extension of the pull-back of the disjoined triple of L along π_r — the extra exceptional divisor is empty (isEmptyExtension_totalTransform_of_eq_empty, propagated along the list by exists_isEmptyExtension_totalTransformSeqFrom_last).

Both are instances of disjoinedTripleOf_isEmptyExtensionOfPullback: a correspondence of the boundary families at the last stages (PullbackCorr, Corr.lean) with matched original members, plus the equation of the ideal sheaves, gives the relation IsEmptyExtensionOfPullback of the disjoined triples (the same ideal sheaf, the boundary an empty extension of the pulled-back boundary) — the hypothesis under which the input family's IndifferentToEmptyMembers and CommutesWithLocalIsos identify its values. Used by Canonicity.lean (through ValueNatural.lean) for the independence of the shrinking open.

Empty extensions of pull-backs of triples

def Manifold.AnalyticTriple.IsEmptyExtensionOfPullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T' : AnalyticTriple ψ₀ N) (T : AnalyticTriple ψ₀ M) (g : AnalyticMap N M) : Prop

T' on N is an empty extension of the pull-back of T along g: the same ideal sheaf, and the boundary of T' an empty extension of the pulled-back boundary (the same nonempty members plus extra empty members).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.disjoinedTripleOf_isEmptyExtensionOfPullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X X' : AnalyticManifold 𝕜 E} (T₁ : Manifold.AnalyticTriple ψ₀ X') (L : AnalyticManifold.BlowUpSequence ψ₀ X') (h₁ : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L.toSuccession.totalTransformSeqFrom T₁.F (Fin.last L.toSuccession.length))) (h₁' : ((L.toSuccession.totalTransformSeqFrom T₁.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T₁.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T₁.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) (T₂ : Manifold.AnalyticTriple ψ₀ X) (R : AnalyticManifold.BlowUpSequence ψ₀ X) (h₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ (R.toSuccession.totalTransformSeqFrom T₂.F (Fin.last R.toSuccession.length))) (h₂' : ((R.toSuccession.totalTransformSeqFrom T₂.F (Fin.last R.toSuccession.length)).subfamily fun (k : (R.toSuccession.totalTransformSeqFrom T₂.F (Fin.last R.toSuccession.length)).ι) => k ∈ Set.range (R.toSuccession.originalIdx T₂.F (Fin.last R.toSuccession.length))).meetLocus 2 = ∅) (g : AnalyticMap (R.stage (Fin.last R.length)) (L.stage (Fin.last L.length))) (hI : Manifold.IdealSheaf.pullback ⇑(R.toSuccession.stageMap (Fin.last R.toSuccession.length)) ⋯ T₂.I = Manifold.IdealSheaf.pullback ⇑g ⋯ (Manifold.IdealSheaf.pullback ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⋯ T₁.I)) (e₀ : T₁.F.ι ≃ T₂.F.ι) (hF : Manifold.HypersurfaceFamily.PullbackCorr (⇑g) (L.toSuccession.totalTransformSeqFrom T₁.F (Fin.last L.toSuccession.length)) (R.toSuccession.totalTransformSeqFrom T₂.F (Fin.last R.toSuccession.length)) (L.toSuccession.originalIdx T₁.F (Fin.last L.toSuccession.length)) (R.toSuccession.originalIdx T₂.F (Fin.last R.toSuccession.length) ∘ ⇑e₀)) : (disjoinedTripleOf T₂ R h₂ h₂').IsEmptyExtensionOfPullback (disjoinedTripleOf T₁ L h₁ h₁') g

A correspondence of the boundary families at the last stages with matched original members, together with the equation of the ideal sheaves, makes the disjoined triple of the one list an empty extension of the pull-back of the disjoined triple of the other.

Propagation of an empty extension along a list

theorem AnalyticManifold.BlowUpSequence.exists_isEmptyExtension_totalTransformSeqFrom_last {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (G G' : Manifold.HypersurfaceFamily M.carrier) (e₀ : G.ι ↪o G'.ι) : Manifold.HypersurfaceFamily.IsEmptyExtension e₀ → Manifold.HypersurfaceFamily.PullbackCorr id (L.toSuccession.totalTransformSeqFrom G (Fin.last L.toSuccession.length)) (L.toSuccession.totalTransformSeqFrom G' (Fin.last L.toSuccession.length)) (L.toSuccession.originalIdx G (Fin.last L.toSuccession.length)) fun (j : G.ι) => L.toSuccession.originalIdx G' (Fin.last L.toSuccession.length) (e₀ j)

An empty extension on the same space is a correspondence across the identity.

The stage map of cons at the last stage

theorem AnalyticManifold.BlowUpSequence.stageMap_last_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (q : ((cons hY rest).stage (Fin.last (cons hY rest).length)).carrier) : ((cons hY rest).toSuccession.stageMap (Fin.last (cons hY rest).toSuccession.length)) q = (Manifold.blowUpπ ψ₀ hY) ((rest.toSuccession.stageMap (Fin.last rest.toSuccession.length)) q)

The composite blow-down of cons hY rest at the last stage is the blow-down of the first round after the composite of rest (stageMapAux_cons_succ).

The blow-down of an empty centre is a local analytic isomorphism

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_blowUpπ_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(Manifold.blowUpπ ψ₀ hY)

The blow-down of an empty centre is a local analytic isomorphism (it is the analytic isomorphism emptyBlowUpDiffeomorph as a function).

Naturality of the disjoined triple

theorem AnalyticManifold.BlowUpSequence.isEmptyExtensionOfPullback_disjoinedTripleOf_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (h₁ : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length))) (h₁' : ((L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) (h₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((L.pullback h hh).toSuccession.totalTransformSeqFrom (T.pullback h hh).F (Fin.last (L.pullback h hh).toSuccession.length))) (h₂' : (((L.pullback h hh).toSuccession.totalTransformSeqFrom (T.pullback h hh).F (Fin.last (L.pullback h hh).toSuccession.length)).subfamily fun (k : ((L.pullback h hh).toSuccession.totalTransformSeqFrom (T.pullback h hh).F (Fin.last (L.pullback h hh).toSuccession.length)).ι) => k ∈ Set.range ((L.pullback h hh).toSuccession.originalIdx (T.pullback h hh).F (Fin.last (L.pullback h hh).toSuccession.length))).meetLocus 2 = ∅) : (Hironaka.Manifold.disjoinedTripleOf (T.pullback h hh) (L.pullback h hh) h₂ h₂').IsEmptyExtensionOfPullback (Hironaka.Manifold.disjoinedTripleOf T L h₁ h₁') (L.pullbackLiftLast h hh)

Functoriality of the disjoined triple for local analytic isomorphisms ([Kol07, 34.1]): the disjoined triple of h^* L for the pulled-back triple is (an empty extension of, with no extra member) the pull-back of the disjoined triple of L along the last-stage lift h_r.

theorem AnalyticManifold.BlowUpSequence.isEmptyExtensionOfPullback_disjoinedTripleOf_cons_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : BlowUpSequence ψ₀ M) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(Manifold.blowUpπ ψ₀ hY)) (h₁ : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length))) (h₁' : ((L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) (h₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.totalTransformSeqFrom T.F (Fin.last (cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.length))) (h₂' : (((cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.totalTransformSeqFrom T.F (Fin.last (cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.length)).subfamily fun (k : ((cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.totalTransformSeqFrom T.F (Fin.last (cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.length)).ι) => k ∈ Set.range ((cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.originalIdx T.F (Fin.last (cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)).toSuccession.length))).meetLocus 2 = ∅) : (Hironaka.Manifold.disjoinedTripleOf T (cons hY (L.pullback (Manifold.blowUpπ ψ₀ hY) hπ)) h₂ h₂').IsEmptyExtensionOfPullback (Hironaka.Manifold.disjoinedTripleOf T L h₁ h₁') (L.pullbackLiftLast (Manifold.blowUpπ ψ₀ hY) hπ)

The empty blow-up convention [Kol07, 32] for the disjoined triple: the disjoined triple of the list padded by an empty first round, cons h∅ (π^* L), is an empty extension of the pull-back of the disjoined triple of L along the last-stage lift of the blow-down π — the extra exceptional divisor is empty.