Independence of the shrinking open; the principalization family functor

The value of the principalization family on a relatively compact open U was defined with a shrinking open W ⊇ closure U (principalizationValueOn, Hironaka/Resolution/Analytic/Principalization/Assembly.lean). This module proves it does not depend on W and assembles the compatible family and the family functor:

• principalizationValueOn_eq_of_le: for W ≤ W', the disjoining list over W' pulled back to W is the disjoining list over W at the (larger) bound of W' (disjoinList_pullback, AnalyticTriple.pullback_inclusion_restrictLE), so the value at W' is the value at W computed with that bound (valueOf_pullback, the disjoined triple being natural under pull-back), which is the value at W's own bound by padding with empty blow-ups (valueOf_disjoinList_eq);
• principalizationValueOn_eq: two arbitrary shrinking opens compare through their union;
• principalizationValue_compat: the values on U ≤ V compare at the common shrinking open of V (principalizationValueOn_restrict) — the compatibility of the family under restriction (Kollár's functoriality for open embeddings [Kol07, 34.1]; Włodarczyk's compatibility of the factorizations over nested opens [Wlo09, Theorem 2.0.3 (4)]);
• principalizationFam: the family functor on all triples (Dom := fun _ => True).

Transports along equalities of the base triple and the list

theorem Hironaka.Manifold.isSnc_totalTransformSeqFrom_last_congr₂ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (eL : L₁ = L₂) {F₁ F₂ : Manifold.HypersurfaceFamily M.carrier} (eF : F₁ = F₂) (h : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L₁.toSuccession.totalTransformSeqFrom F₁ (Fin.last L₁.toSuccession.length))) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L₂.toSuccession.totalTransformSeqFrom F₂ (Fin.last L₂.toSuccession.length))

Transport of the snc hypothesis on the boundary along equalities of the list and the family.

theorem Hironaka.Manifold.meetLocus_two_subfamily_original_congr₂ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (eL : L₁ = L₂) {F₁ F₂ : Manifold.HypersurfaceFamily M.carrier} (eF : F₁ = F₂) (h : ((L₁.toSuccession.totalTransformSeqFrom F₁ (Fin.last L₁.toSuccession.length)).subfamily fun (k : (L₁.toSuccession.totalTransformSeqFrom F₁ (Fin.last L₁.toSuccession.length)).ι) => k ∈ Set.range (L₁.toSuccession.originalIdx F₁ (Fin.last L₁.toSuccession.length))).meetLocus 2 = ∅) : ((L₂.toSuccession.totalTransformSeqFrom F₂ (Fin.last L₂.toSuccession.length)).subfamily fun (k : (L₂.toSuccession.totalTransformSeqFrom F₂ (Fin.last L₂.toSuccession.length)).ι) => k ∈ Set.range (L₂.toSuccession.originalIdx F₂ (Fin.last L₂.toSuccession.length))).meetLocus 2 = ∅

Transport of the disjointness hypothesis on the original members along equalities of the list and the family.

theorem Hironaka.Manifold.valueOf_disjoinedTripleOf_congr₂ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T₁ T₂ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (eT : T₁ = T₂) {L₁ L₂ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (eL : 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 equalities of the base triple and of the list.

Canonicity of the shrinking open

theorem Hironaka.Manifold.principalizationValueOn_eq_of_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) {U W W' : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hW : IsCompact (closure ↑W)) (hW' : IsCompact (closure ↑W')) (hUW : closure ↑U ⊆ ↑W) (hUW' : closure ↑U ⊆ ↑W') (hWW' : W ≤ W') : principalizationValueOn bmo T U hU W hW hUW = principalizationValueOn bmo T U hU W' hW' hUW'

The value does not depend on the shrinking open, for W ≤ W': the disjoining list over W' pulled back to W is the disjoining list over W at W''s bound; the value at W' is the value at W with that bound (valueOf_pullback), which is the value at W's own bound (valueOf_disjoinList_eq).

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

The value does not depend on the shrinking open: two admissible shrinking opens compare through their union.

The compatible family and the functor

theorem Hironaka.Manifold.principalizationValue_compat {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U V : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : principalizationValue bmo T U hU = ((principalizationValue bmo T V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The compatibility clause of the principalization family ([Kol07, 34.1]; [Wlo09, Theorem 2.0.3 (4)], per open): the value on U ≤ V is the value on V pulled back along the open inclusion with the empty rounds deleted. Both values are computed at the shrinking open of V (principalizationValueOn_eq), where they restrict (principalizationValueOn_restrict).

noncomputable def Hironaka.Manifold.principalizationFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (x : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) => True

The principalization family functor on all triples ([Kol07, Theorem 35] built as in [Kol07, 72], in the compatible-family form): the value on each relatively compact open is principalizationValue (no empty centres; compatible under restriction).

Equations

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

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