The value of the principalization family on a relatively compact open

Kollár's construction of the principalization functor [Kol07, 72] read over a relatively compact open U ⋐ M of the triple (M, 𝓘, E): choose a relatively compact open W with closure U ⊆ W (the shrinking chain U ⋐ W ⋐ M), restrict the triple to W — finitely many members of E meet closure W (IsSnc.finite_of_isCompact) — blow up the disjoining centres of [Kol07, 72] (disjoinList), form the disjoined triple on the last stage (disjoinedTriple, in the marked class at mark 1), apply the marked order-reduction family BMO_{n,1} to it and read its value on the reading open over U (liftRange, relatively compact since the composite blow-down is proper), append it to the disjoining list restricted to U (shrinkAppend), and delete the empty rounds (Kollár's convention [Kol07, 32]). This module defines that value, principalizationValue, and proves it has no empty centres; that it does not depend on W, and the compatibility clause of the family, are proved in Canonicity.lean; the clauses of [Kol07, Theorem 35] in the Clause*.lean modules of this directory. The value is what the resolution of an analytic space is assembled from (Hironaka/Manifold/Sequence/Resolve/).

The shrinking open W of the chain U ⋐ W ⋐ M

noncomputable def Hironaka.Manifold.shrinkOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : TopologicalSpace.Opens M.carrier

The shrinking open of the chain: a relatively compact open containing closure U (chosen; Mathlib's exists_isOpen_superset_and_isCompact_closure on the locally compact manifold).

Equations

• Hironaka.Manifold.shrinkOpen U hU = { carrier := Classical.choose ⋯, is_open' := ⋯ }

theorem Hironaka.Manifold.closure_subset_shrinkOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : closure ↑U ⊆ ↑(shrinkOpen U hU)

theorem Hironaka.Manifold.isCompact_closure_shrinkOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : IsCompact (closure ↑(shrinkOpen U hU))

theorem Hironaka.Manifold.le_shrinkOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : U ≤ shrinkOpen U hU

The restricted triple over W and its disjoining list

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.restrictTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict W)

The triple restricted to the open W (Kollár's "over a relatively compact open").

Equations

• Hironaka.Manifold.restrictTriple T W = T.pullback (M.inclusion W) ⋯

theorem Hironaka.Manifold.finite_nonempty_restrictTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : Finite { j : (restrictTriple T W).F.ι // (restrictTriple T W).F.hyp j ≠ ∅ }

Finitely many members of E meet a relatively compact open (Kollár's E_1, …, E_k, [Kol07, 72]; IsSnc.finite_of_isCompact), so the restricted family has finitely many nonempty members.

noncomputable def Hironaka.Manifold.disjoinBound {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) : ℕ

Kollár's k: the number of members of E meeting W.

Equations

• Hironaka.Manifold.disjoinBound T W = Nat.card { j : (Hironaka.Manifold.restrictTriple T W).F.ι // (Hironaka.Manifold.restrictTriple T W).F.hyp j ≠ ∅ }

theorem Hironaka.Manifold.meetLocus_disjoinBound_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : (restrictTriple T W).F.meetLocus (disjoinBound T W + 1) = ∅

No point of W lies on k + 1 members.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.disjoinListOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict W)

The disjoining blow-ups of [Kol07, 72] for the triple restricted to W.

Equations

• Hironaka.Manifold.disjoinListOn T W hW = Hironaka.Manifold.disjoinList (Hironaka.Manifold.disjoinBound T W) (Hironaka.Manifold.restrictTriple T W).F ⋯ ⋯

The value built from a list and a triple on its last stage

noncomputable def Hironaka.Manifold.valueOf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (L.stage (Fin.last L.length))) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N

The value built from a list L on X and a triple T' of the marked class on its last stage, read along a local analytic isomorphism ι : N → X with relatively compact range: the shrink-and-append of L along ι with the order-reduction value of T' on the reading open, the empty rounds deleted. The value on U is its instance at the disjoining list and the disjoined triple; the general form is what the independence of the shrinking open compares.

Equations

• Hironaka.Manifold.valueOf bmo L T' hT' ι hι hc = (L.shrinkAppend ι hι ((bmo.functor.fam T' hT').seqOn (L.liftRange ι hι) ⋯)).eraseEmpty

theorem Hironaka.Manifold.valueOf_congr_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (L.stage (Fin.last L.length))) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') {ι ι' : AnalyticMap N X} (e : ι = ι') (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hι' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι') (hc : IsCompact (closure (Set.range ⇑ι))) (hc' : IsCompact (closure (Set.range ⇑ι'))) : valueOf bmo L T' hT' ι hι hc = valueOf bmo L T' hT' ι' hι' hc'

The value is compatible with an equality of the reading maps.

theorem Hironaka.Manifold.valueOf_disjoinedTripleOf_congr {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) {L₁ L₂ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (e : L₁ = L₂) (h₁ : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (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 (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (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 = ∅) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) : valueOf bmo L₁ (disjoinedTripleOf T L₁ h₁ h₁') ⋯ ι hι hc = valueOf bmo L₂ (disjoinedTripleOf T L₂ h₂ h₂') ⋯ ι hι hc

The value built from the disjoined triple is compatible with an equality of lists.

The value on U

noncomputable def Hironaka.Manifold.principalizationValueOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hUW : closure ↑U ⊆ ↑W) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U)

The value on U computed with a shrinking open W ([Kol07, 72], per relatively compact open): for any relatively compact open W with closure U ⊆ W, disjoin over W, apply BMO_{n,1} to the disjoined triple, read it on the reading open over U, append to the disjoining list restricted to U, and delete the empty rounds ([Kol07, 32]). The independence of W is proved with the compatibility clause (Canonicity.lean).

Equations

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

noncomputable def Hironaka.Manifold.principalizationValue {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U)

The value of the principalization family on U: the value computed with the chosen shrinking open shrinkOpen U hU.

Equations

• Hironaka.Manifold.principalizationValue bmo T U hU = Hironaka.Manifold.principalizationValueOn bmo T U hU (Hironaka.Manifold.shrinkOpen U hU) ⋯ ⋯

theorem Hironaka.Manifold.noEmptyCenters_principalizationValue {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (principalizationValue bmo T U hU).NoEmptyCenters

The value has no empty centres (Kollár's convention on empty blow-ups, [Kol07, 32]).