Compatible families of blow-up sequences and the family functors

Włodarczyk's resolution of an analytic space is a compatible family: a finite blow-up sequence over every relatively compact open subset, the sequences over U ⊆ V compatible under restriction up to empty blow-ups [Wlo09, Theorem 2.0.3, (1) and (4)], the notion of extension being [Wlo09, Definition 3.2.6]; the vocabulary of the main theorems has the corresponding AnalyticManifold.ExtensionCompatibleFamily. Accordingly the analytic order-reduction functors have, beside their finite form on triples, a family form: the value on a triple is a finite CenterList on every relatively compact open U ⊆ M, with no empty blow-ups ([Kol07, 32]), compatible under restriction up to empty blow-ups.

This file provides the general tool AnalyticMap.restrictMap (the restriction of an analytic map to a pair of opens, with restrictLE, the open inclusion U ⊆ V, as its instance at the identity) and its properties (image opens, compact closure of images, local isomorphism and surjectivity of restrictions); CompatibleFamily; the family functor AnalyticFamilyFunctor with its commutation ([Kol07, 34.1]) and indifference predicates; the records BOanFam and BMOanFam of the order-reduction functors in family form; and the per-open bridge AnalyticBlowUpSequenceAssignment.toFamily from a finite functor to a family functor.

The general restriction of an analytic map to a pair of opens

def Hironaka.Manifold.AnalyticMap.restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (U' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (h : ⇑g '' ↑U' ⊆ ↑V) : AnalyticMap (N.restrict U') (M.restrict V)

The restriction of an analytic map g : N → M to opens U' ⊆ N, V ⊆ M with g '' U' ⊆ V, as an analytic map N.restrict U' → M.restrict V. Its instance at g = id is the open inclusion restrictLE, and it is also the restriction g|_{U'} of a cover map and of a local isomorphism in the commutation predicates of the family functors: one constructor for all three.

Equations

• Hironaka.Manifold.AnalyticMap.restrictMap g U' V h = ⟨fun (p : (N.restrict U').carrier) => ⟨g ↑p, ⋯⟩, ⋯⟩

@[simp]

theorem Hironaka.Manifold.AnalyticMap.restrictMap_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (U' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (h : ⇑g '' ↑U' ⊆ ↑V) (p : (N.restrict U').carrier) : (M.inclusion V) ((restrictMap g U' V h) p) = g ((N.inclusion U') p)

def AnalyticManifold.restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : AnalyticMap (M.restrict U) (M.restrict V)

The open inclusion M.restrict U → M.restrict V for U ≤ V, the id-instance of restrictMap.

Equations

• M.restrictLE hUV = ⟨TopologicalSpace.Opens.inclusion hUV, ⋯⟩

theorem Hironaka.Manifold.isLocalDiffeomorph_restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(M.restrictLE hUV)

The compatible family of finite blow-up sequences

structure Hironaka.Manifold.CompatibleFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Type (max (u + 1) u_1)

The value of an order-reduction functor on a triple T — a finite CenterList on every relatively compact open U, with no empty blow-ups, compatible under restriction U ≤ V up to empty blow-ups: the value on U is the pull-back of the value on V along the inclusion with its empty centres deleted (one-sided, seqOn having no empty centres). The analogue of the vocabulary's AnalyticManifold.ExtensionCompatibleFamily.

• seqOn (U : TopologicalSpace.Opens M.carrier) : IsCompact (closure ↑U) → AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

  The finite blow-up sequence over each relatively compact open.

• noEmptyCenters (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (self.seqOn U hU).NoEmptyCenters

  No empty centres ([Kol07, 32], per open).

• compat (U V : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : self.seqOn U hU = ((self.seqOn V hV).pullback (M.restrictLE hUV) ⋯).eraseEmpty

  Compatibility under restriction, up to empty blow-ups ([Wlo09, Theorem 2.0.3, (4)]; Wlo09, Definition 3.2.6).

theorem Hironaka.Manifold.CompatibleFamily.ext_iff {𝕜 : Type} {inst✝ : RCLike 𝕜} {E : Type u_1} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {x y : CompatibleFamily T} : x = y ↔ x.seqOn = y.seqOn

theorem Hironaka.Manifold.CompatibleFamily.ext {𝕜 : Type} {inst✝ : RCLike 𝕜} {E : Type u_1} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {x y : CompatibleFamily T} (seqOn : x.seqOn = y.seqOn) : x = y

noncomputable def Hironaka.Manifold.CompatibleFamily.nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : CompatibleFamily T

The trivial family — the empty CenterList on every open — is a CompatibleFamily for every triple (compatibility by pullback_nil and eraseEmpty_nil). The value of the trivial family functor nilFamilyFunctor.

Equations

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

theorem Hironaka.Manifold.CompatibleFamily.eq_of_seqOn_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {F₁ F₂ : CompatibleFamily T} (hTop : IsCompact (closure ↑⊤)) (h : F₁.seqOn ⊤ hTop = F₂.seqOn ⊤ hTop) : F₁ = F₂

On a manifold whose whole space is relatively compact (in particular a compact M), a CompatibleFamily is determined by its value at ⊤ — every open lies below ⊤, so compat reads every seqOn U hU off seqOn ⊤. The finite and family layers agree there.

More tools for restrictMap: the image open, its compact closure, local

diffeomorphism, surjectivity and range

def Hironaka.Manifold.AnalyticMap.imageOpens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) : TopologicalSpace.Opens M.carrier

The image g '' U' of a relatively compact open under a local analytic isomorphism g, as an open subset of the codomain (g is an open map, IsLocalDiffeomorph.isOpenMap). The codomain open onto which g|_{U'} is surjective in CommutesWithLocalIsos.

Equations

• Hironaka.Manifold.AnalyticMap.imageOpens g hg U' = { carrier := ⇑g '' ↑U', is_open' := ⋯ }

theorem Hironaka.Manifold.AnalyticMap.isCompact_closure_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) {U' : TopologicalSpace.Opens N.carrier} (hU' : IsCompact (closure ↑U')) : IsCompact (closure (⇑g '' ↑U'))

The closure of the image of a relatively compact open under g is compact — closure (g '' U') ⊆ g '' closure U', a compact (hence closed, the codomain is Hausdorff) set, and a closed subset of a compact set is compact. Makes g.imageOpens hg U' a valid index of seqOn.

theorem Hironaka.Manifold.AnalyticMap.isLocalDiffeomorph_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (h : ⇑g '' ↑U' ⊆ ↑V) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(restrictMap g U' V h)

g|_{U'} : N.restrict U' → M.restrict V is a local analytic isomorphism when g is — it factors as (M.inclusion V)⁻¹ ∘ g ∘ N.inclusion U', a composite of local diffeomorphisms (IsLocalDiffeomorphAt.comp; inclusionInv is the local inverse of the open inclusion on V). Needed to pull a family back along g|_{U'}.

theorem Hironaka.Manifold.AnalyticMap.surjective_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} {U' : TopologicalSpace.Opens N.carrier} {V : TopologicalSpace.Opens M.carrier} (h' : ⇑g '' ↑U' = ↑V) : Function.Surjective ⇑(restrictMap g U' V ⋯)

g|_{U'} is surjective onto the image open (g '' U' = V). This is why the two bullets of [Kol07, 34.1] collapse to one clause per open: g|_{U'} is always onto its image.

theorem Hironaka.Manifold.AnalyticMap.range_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (U' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (h : ⇑g '' ↑U' ⊆ ↑V) : Set.range ⇑(restrictMap g U' V h) = Subtype.val ⁻¹' ⇑g '' ↑U'

The range of g|_{U'} in M.restrict V is the preimage of the image g '' U' under the inclusion of V.

theorem Hironaka.Manifold.range_restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : Set.range ⇑(M.restrictLE hUV) = Subtype.val ⁻¹' ↑U

The range of the open inclusion restrictLE in M.restrict V is the preimage of U under the inclusion of V.

theorem Hironaka.Manifold.isAnalyticOpenEmbedding_restrictLE {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) : Manifold.IsAnalyticOpenEmbedding (M.restrictLE hUV)

The open inclusion restrictLE is an analytic open embedding (a local analytic isomorphism that is injective) — the datum CommutesWithOpenEmbeddings reads in the bridge.

theorem Hironaka.Manifold.AnalyticMap.isCoprodOfOpenEmbeddings_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} {g : AnalyticMap N M} (hg : Manifold.IsCoprodOfOpenEmbeddings g) (U' : TopologicalSpace.Opens N.carrier) (V : TopologicalSpace.Opens M.carrier) (h : ⇑g '' ↑U' ⊆ ↑V) : Manifold.IsCoprodOfOpenEmbeddings (restrictMap g U' V h)

If g is a coproduct of open embeddings, so is g|_{U'} — the clopen decomposition of N pulls back to one of N.restrict U', g injective on each piece.

theorem Hironaka.Manifold.restrictLE_eq_restrictMap_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U V : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) (h : ⇑ContMDiffMap.id '' ↑U ⊆ ↑V) : M.restrictLE hUV = AnalyticMap.restrictMap ContMDiffMap.id U V h

The open inclusion restrictLE is the g = id instance of restrictMap (rfl), so that the two constructors are interchangeable.

The family functor on a class and its per-open commutation predicates

structure Hironaka.Manifold.AnalyticFamilyFunctor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop) : Type (max (u + 1) u_1)

A family order-reduction functor on a class Dom — a compatible family of finite blow-up sequences for every triple of the class. The single field is fam; commutation and indifference are predicates on it, consumed by the records BOanFam/BMOanFam as fields.

• fam {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Dom T → CompatibleFamily T

  The compatible family assigned to each triple of the class.

def Hironaka.Manifold.AnalyticFamilyFunctor.CommutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) : Prop

B commutes with local analytic isomorphisms — for a local analytic isomorphism g : N → M with T' carrying the pull-back data of T (both in Dom) and every relatively compact open U' ⊆ N, the value on U' is the pull-back along g|_{U'} : U' → g(U') (always onto its image, so the two bullets of 34.1 unite) of the value on the relatively compact open g(U'), with empty blow-ups erased.

Equations

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

def Hironaka.Manifold.AnalyticFamilyFunctor.IndifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) : Prop

Deleting empty boundary members changes no seqOn U hU.

Equations

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

The family records BOanFam / BMOanFam at the standard model

structure Hironaka.Manifold.BOanFam (𝕜 : Type) [RCLike 𝕜] (n m : ℕ) : Type (u + 1)

The family form of the order-reduction functor BO_{n,m} — a family functor on the class BOClass m at the standard model with four clauses read per relatively compact open on the restricted triple T.pullback (M.inclusion U) (isLocalDiffeomorph_inclusion M U). It lives in Type (u+1). The clauses of [Kol07, Theorem 103, (3)] and [Kol07, 108] are not fields.

• functor : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BOClass m

  The family functor BO_{n,m} on the order-reduction class at the standard model 𝕜ⁿ.

• isOfOrderGe {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((self.functor.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I m (T.pullback (M.inclusion U) ⋯).F.idealSheaf

  [Kol07, Definition 66] (2′)–(4′), per open: the value on U is a smooth blow-up sequence of order ≥ m starting with the restricted (M, 𝓘, m, E).

• ord_lt {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : (((self.functor.fam T hT).seqOn U hU).toSuccession.stage (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (((self.functor.fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I m (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)) x < ↑m

  Theorem 103 (1) ("max-ord I_r < m"), pointwise per open: the marked transform at the last stage over U has order < m at every point.

• commutesWithLocalIsos : self.functor.CommutesWithLocalIsos

  Theorem 103 (2): the functor commutes with local analytic isomorphisms.

• indifferentToEmptyMembers : self.functor.IndifferentToEmptyMembers

  The functor is indifferent to empty boundary members.

structure Hironaka.Manifold.BMOanFam (𝕜 : Type) [RCLike 𝕜] (n m : ℕ) : Type (u + 1)

The family form of the marked order-reduction functor BMO_{n,m} — a family functor on the class BMOClass m (no order bound) at the standard model with the four BMOanData clauses read per relatively compact open on the restricted triple. Type (u+1) as the finite record. The clauses of [Kol07, Theorem 107, (3)] and [Kol07, 108] are not fields.

• functor : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BMOClass m

  The family functor BMO_{n,m} on the marked class at the standard model 𝕜ⁿ.

• isOfOrderGe {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((self.functor.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I m (T.pullback (M.inclusion U) ⋯).F.idealSheaf

  [Kol07, Definition 66] (2′)–(4′), per open: the value on U is a smooth blow-up sequence of order ≥ m starting with the restricted (M, 𝓘, m, E).

• ord_lt {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : (((self.functor.fam T hT).seqOn U hU).toSuccession.stage (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (((self.functor.fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I m (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)) x < ↑m

  Theorem 107 (1) ("max-ord I_r < m"), pointwise per open: the marked transform at the last stage over U has order < m at every point.

• commutesWithLocalIsos : self.functor.CommutesWithLocalIsos

  Theorem 107 (2): the functor commutes with local analytic isomorphisms.

• indifferentToEmptyMembers : self.functor.IndifferentToEmptyMembers

  The functor is indifferent to empty boundary members.

The per-open bridge from the finite layer

noncomputable def Manifold.AnalyticBlowUpSequenceAssignment.toFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) (hres : ∀ {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier), Dom T → Dom (T.pullback (M.inclusion U) ⋯)) (hopen : B.CommutesWithOpenEmbeddings) : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom

A finite blow-up-sequence functor B on a class closed under restriction to opens (hres) that commutes with open embeddings (hopen) gives a family functor B.toFamily, its value on U the finite value on the restricted triple. compat is the open-embedding clause of [Kol07, 34.1] along the open inclusion restrictLE; noEmptyCenters is B.noEmptyCenters. The finite functor thereby yields a family functor with no further proof.

Equations

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

The intrinsic classes restrict to any open (the hypothesis hres of toFamily)

theorem Hironaka.Manifold.finite_nonempty_pullback_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hfin : Finite { j : T.F.ι // T.F.hyp j ≠ ∅ }) : Finite { j : (T.pullback (M.inclusion U) ⋯).F.ι // (T.pullback (M.inclusion U) ⋯).F.hyp j ≠ ∅ }

A member's preimage under the open inclusion is nonempty only if the member is, so the global finiteness of the nonempty members restricts to any open (no relative compactness needed — the weaker hypothesis beside boClass_pullback_inclusion).

theorem Hironaka.Manifold.boClass_pullback_inclusion_of_boClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {m : ℕ} (U : TopologicalSpace.Opens M.carrier) (hT : Manifold.AnalyticTriple.BOClass m T) : Manifold.AnalyticTriple.BOClass m (T.pullback (M.inclusion U) ⋯)

The intrinsic class BOClass m restricts to any open — the order bound restricts (IdealSheaf.ord_pullback_of_isLocalDiffeomorphAt) and the finiteness from finite_nonempty_pullback_inclusion (weaker hypotheses than boClass_pullback_inclusion: no relative compactness).

theorem Hironaka.Manifold.bmoClass_pullback_inclusion_of_bmoClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {m : ℕ} (U : TopologicalSpace.Opens M.carrier) (hT : Manifold.AnalyticTriple.BMOClass m T) : Manifold.AnalyticTriple.BMOClass m (T.pullback (M.inclusion U) ⋯)

The intrinsic class BMOClass m (no order bound) restricts to any open.

Universes: the family records live in Type (u+1),

exactly the universe of the finite record BMOanData (both quantify over AnalyticManifold.{u}).