Step 3 of Theorem 103 in the compatible-family form: the existence statement and the descent

of the clauses

Two consequences of the descended family functor of GlobalizeFam.lean:

• AnalyticFamilyFunctor.BO_globalizeFam — Step 3 of the proof of [Kol07, Theorem 103] as an existence statement: a family functor on the class LocalMCClass m commuting with local analytic isomorphisms extends to one on BOClass m agreeing with it on LocalMCClass m and commuting with local analytic isomorphisms (witnessed by globalizeFam).
• isOfOrderGe_of_agreeFam, ord_lt_of_agreeFam, indifferentToEmptyMembers_of_agreeFam — the descent of the clauses of Theorem 103 along the cover of Step 3, per relatively compact open ("the functoriality package is local", [Kol07, 104, Step 2.3]). For a relatively compact open U of a triple T of the class, a finite cover C of the closure of U by pieces with maximal contact (GlobalizeFamCover.lean) gives the surjective local analytic isomorphism k : ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U; for any extension B' agreeing with B on the local class and commuting with local analytic isomorphisms, the pull-back along k of the value of B' on U is the value of B on the cover (ShrunkMCCover.seqOn_coverList_eq), and the two restricted triples agree (triple_pullback_inclusion_eq). The order clause ([Kol07, Definition 66]) and the conclusion max-ord I_r < m ([Kol07, Theorem 103 (1)]) then descend along the surjective k pointwise, and the indifference to empty boundary members descends because the triple with the smaller boundary has the same cover (maximal contact depends only on the ideal sheaf), B is indifferent on the cover, and pull-back along k is injective.

They give the order-reduction family assembled in BOanFamOfInput.lean its clauses.

theorem Manifold.AnalyticTriple.ShrunkMCCover.triple_pullback_inclusion_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) : C.triple.pullback (C.sigma.inclusion C.opens) ⋯ = (T.pullback (M.inclusion U) ⋯).pullback C.coverMap ⋯

The two restrictions agree: the restriction of the coproduct triple to the open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) is the pull-back of the restriction T|_U along the cover map (both carry the pull-back data of T along the same map ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → M).

theorem Manifold.AnalyticTriple.ShrunkMCCover.seqOn_coverList_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (B' : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => BOClass m) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ N) (hL : LocalMCClass m T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hG : BOClass m T) (hU : IsCompact (closure ↑U)) : (B.fam C.triple ⋯).seqOn C.opens ⋯ = ((B'.fam T hG).seqOn U hU).pullback C.coverMap ⋯

For an extension B' of B (agreeing on the local class, commuting with local analytic isomorphisms), the value of B on the open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) of the coproduct is the pull-back of the value of B' on U along the cover map; no empty blow-up is deleted, the cover map being onto U.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.BO_globalizeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m) (hB : B.CommutesWithLocalIsos) : ∃ (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m), (∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T), B'.fam T ⋯ = B.fam T hL) ∧ B'.CommutesWithLocalIsos

Step 3 of the proof of [Kol07, Theorem 103] in the compatible-family form, as an existence statement: a family functor B on the class LocalMCClass m of triples with a global hypersurface of maximal contact, commuting with local analytic isomorphisms, extends to a family functor on BOClass m which agrees with B on LocalMCClass m and commutes with local analytic isomorphisms. The witness is globalizeFam B hB (GlobalizeFam.lean).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.isOfOrderGe_of_agreeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m) (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hord : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)), ((B.fam T hL).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I m (T.pullback (N.inclusion U) ⋯).F.idealSheaf) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hG : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : ((B'.fam T hG).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I m (T.pullback (N.inclusion U) ⋯).F.idealSheaf

The order clause ([Kol07, Definition 66]) descends along the cover of Step 3 of the proof of [Kol07, Theorem 103], per relatively compact open: on the cover k : ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U of the closure of U by pieces with maximal contact, the pull-back along k of the value of B' on U is the value of B on the cover, which is of order ≥ m for the pulled-back data, and being a smooth blow-up sequence of order ≥ m descends along a surjective local analytic isomorphism (BlowUpSequence.isOfOrderGe_of_pullback).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.ord_lt_of_agreeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m) (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hlt : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) (x : (((B.fam T hL).seqOn U hU).toSuccession.stage (Fin.last ((B.fam T hL).seqOn U hU).toSuccession.length)).carrier), Manifold.IdealSheaf.ord (((B.fam T hL).seqOn U hU).toSuccession.weakTransformSeq (T.pullback (N.inclusion U) ⋯).I (Fin.last ((B.fam T hL).seqOn U hU).toSuccession.length)) x < ↑m) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hG : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) (x : (((B'.fam T hG).seqOn U hU).toSuccession.stage (Fin.last ((B'.fam T hG).seqOn U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (((B'.fam T hG).seqOn U hU).toSuccession.weakTransformSeq (T.pullback (N.inclusion U) ⋯).I (Fin.last ((B'.fam T hG).seqOn U hU).toSuccession.length)) x < ↑m

The conclusion max-ord I_r < m of [Kol07, Theorem 103 (1)] descends along the cover of Step 3, per relatively compact open: a point of the last stage over U is the image of a point of the last stage of the pull-back along the surjective cover map k, where the value of B on the cover has order < m, and the order of a pull-back along a local analytic isomorphism at a point is the order at its image.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.indifferentToEmptyMembers_of_agreeFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.LocalMCClass m) (B' : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BOClass m) (hagree : ∀ {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T), B'.fam T ⋯ = B.fam T hL) (hB' : B'.CommutesWithLocalIsos) (hind : B.IndifferentToEmptyMembers) : B'.IndifferentToEmptyMembers

The indifference to empty boundary members descends along the cover of Step 3: the triple with the smaller boundary has the same finite cover by pieces with maximal contact (maximal contact depends only on the ideal sheaf), B is indifferent on the cover, and pull-back along the surjective cover map is injective.