The rounds on the nonmonomial part: commutation with local analytic isomorphisms #
Clause (2) of [Kol07, Theorem 103] and the second condition of [Kol07, 34.1] for the value of the
rounds on the nonmonomial part: along a local analytic isomorphism g : N → M and a relatively
compact open U' ⊆ N, the value for the pulled-back triple on U' is the value for T on g(U')
pulled back along g|_{U'} and cleaned of empty blow-ups (stepAFamOn_pullback), the shape of
AnalyticFamilyFunctor.CommutesWithLocalIsos. The family functor of the rounds on the marked class
BMOClass m is stepAFunctor, and its commutation is stepAFunctor_commutesWithLocalIsos.
The proof aligns the two canonical descents through a third, virtual descent over N (the device of
StepACompat.lean and StepAIndep.lean): its chain preJoin is the canonical chain of U' met
with the g-preimage of the canonical chain of V ⊇ g(U') (relatively compact, shrinking,
containing U'), its bound the larger of the two bounds, its triple the pulled-back triple pulled
back once more along the identity, so that the descent over M compares with it along g
(descent_restrictMap_eq, the form of descent_restrict_eq for a general g) and the canonical
descent over N compares with it along the identity (descent_restrict_eq itself). The two
comparisons read the same list on U' (imageValueAt_eq_preJoin,
stepAFamOn_pullback_eq_preJoin), with the deletion of empty blow-ups once at the end.
A descent pulled back along a local isomorphism, through the virtual descent #
theorem
Hironaka.Manifold.BMOmod.descent_restrictMap_eq
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑h)
{T₂ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N}
(e : T₂ = T.pullback h hh)
(hT₂ : Manifold.AnalyticTriple.BMOClass m T₂)
(W : ℕ → TopologicalSpace.Opens M.carrier)
(hW : ∀ (k : ℕ), IsCompact (closure ↑(W k)))
(r : ℕ)
(hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k))
(D : ℕ)
(hD : ∀ x ∈ ↑(W 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T).I x ≤ ↑D)
(X : ℕ → TopologicalSpace.Opens N.carrier)
(hX : ∀ (j : ℕ), IsCompact (closure ↑(X j)))
(rX : ℕ)
(hXsub : ∀ j < rX, closure ↑(X (j + 1)) ⊆ ↑(X j))
(DX : ℕ)
(hDX : ∀ x ∈ ↑(X 0), Manifold.IdealSheaf.ord (BMO.nonmonomialTriple T₂).I x ≤ ↑DX)
(hDD : D ≤ DX)
(hrr : rX ≤ DX - D + r)
(hXW : ∀ (j : ℕ), ⇑h '' ↑(X j) ⊆ ↑(W (j - (DX - D))))
(hrXt : rX ≤ DX + 1 - t)
{U' : TopologicalSpace.Opens N.carrier}
(hU'X : U' ≤ X rX)
:
((descentStateAux T m hT bo ⋯ ⋯ t hm hmt W hW r hWsub D hD (rX - (DX - D)) ⋯ ⋯).L.pullback
(AnalyticMap.restrictMap h U' (W (rX - (DX - D))) ⋯) ⋯).eraseEmpty = ((descentStateAux T₂ m hT₂ bo ⋯ ⋯ t hm hmt X hX rX hXsub DX hDX rX ⋯ hrXt).L.pullback (N.restrictLE hU'X)
⋯).eraseEmpty
A descent over M, pulled back along h to an open U' inside the last open of a chain over
N, equals the descent over N (for a triple equal to the pulled-back one) restricted to U',
up to empty blow-ups: the alignment descentStateAux_rel along h, then the restriction composed
with the inclusion (eraseEmpty_pullback_eraseEmpty, pullback_comp). The form of
descent_restrict_eq for a general h.
The virtual chain of a chain over N and the preimage of a chain over M #
@[reducible, inline]
noncomputable abbrev
Hironaka.Manifold.BMOmod.preJoin
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(j : ℕ)
:
The virtual chain: the canonical chain of U' met with the g-preimage of the canonical chain
of V.
Equations
- Hironaka.Manifold.BMOmod.preJoin g U' hU' V hV j = Hironaka.Manifold.BMOmod.stepAChainOpens U' hU' j ⊓ Manifold.preimageOpens ⇑g ⋯ (Hironaka.Manifold.BMOmod.stepAChainOpens V hV j)
Instances For
theorem
Hironaka.Manifold.BMOmod.isCompact_closure_preJoin
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(j : ℕ)
:
theorem
Hironaka.Manifold.BMOmod.closure_preJoin_succ_subset
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(j : ℕ)
:
theorem
Hironaka.Manifold.BMOmod.preJoin_le_left
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(j k : ℕ)
(hkj : k ≤ j)
:
theorem
Hironaka.Manifold.BMOmod.image_preJoin_subset
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(j k : ℕ)
(hkj : k ≤ j)
:
⇑g '' ↑(preJoin g U' hU' V hV j) ⊆ ↑(stepAChainOpens V hV k)
theorem
Hironaka.Manifold.BMOmod.le_preJoin
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(g : AnalyticMap N M)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hUV : ⇑g '' ↑U' ⊆ ↑V)
(j : ℕ)
:
U' lies in every open of the virtual chain (when g(U') ⊆ V).
@[reducible, inline]
noncomputable abbrev
Hironaka.Manifold.BMOmod.preJoinBound
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
:
The larger of the two bounds.
Equations
- Hironaka.Manifold.BMOmod.preJoinBound T g hg U' hU' V hV = max (Hironaka.Manifold.BMOmod.stepABound (T.pullback g hg) U' hU') (Hironaka.Manifold.BMOmod.stepABound T V hV)
Instances For
theorem
Hironaka.Manifold.BMOmod.preJoin_bound
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(x : N.carrier)
(hx : x ∈ ↑(preJoin g U' hU' V hV 0))
:
Manifold.IdealSheaf.ord (BMO.nonmonomialTriple ((T.pullback g hg).pullback ContMDiffMap.id ⋯)).I x ≤ ↑(preJoinBound T g hg U' hU' V hV)
The larger bound holds on the first open of the virtual chain, for the pulled-back triple pulled back once more along the identity (the triple of the virtual descent).
The value of V pulled back along g|_{U'}, with a re-indexed final state #
noncomputable def
Hironaka.Manifold.BMOmod.imageValueAt
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(k : ℕ)
(hk : k ≤ stepALinks T t V hV)
(hkt : k ≤ stepABound T V hV + 1 - t)
(hk' : ⇑g '' ↑U' ⊆ ↑(stepAChainOpens V hV k))
:
AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (N.restrict U')
The k-th state of the canonical descent of V over M, pulled back along g|_{U'} and
cleaned of empty blow-ups (its type does not depend on k).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hironaka.Manifold.BMOmod.imageValueAt_congr
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
{k k' : ℕ}
(e : k = k')
(hk : k ≤ stepALinks T t V hV)
(hkt : k ≤ stepABound T V hV + 1 - t)
(hk' : k' ≤ stepALinks T t V hV)
(hkt' : k' ≤ stepABound T V hV + 1 - t)
(hsub : ⇑g '' ↑U' ⊆ ↑(stepAChainOpens V hV k))
(hsub' : ⇑g '' ↑U' ⊆ ↑(stepAChainOpens V hV k'))
:
imageValueAt T m hT bo ⋯ ⋯ t hm hmt g hg U' V hV k hk hkt hsub = imageValueAt T m hT bo ⋯ ⋯ t hm hmt g hg U' V hV k' hk' hkt' hsub'
theorem
Hironaka.Manifold.BMOmod.stepAFamOn_pullback_restrictMap_eq
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hUV : ⇑g '' ↑U' ⊆ ↑V)
:
((stepAFamOn T m hT bo ⋯ ⋯ t hm hmt V hV).pullback (AnalyticMap.restrictMap g U' V hUV) ⋯).eraseEmpty = imageValueAt T m hT bo ⋯ ⋯ t hm hmt g hg U' V hV (stepALinks T t V hV) ⋯ ⋯ ⋯
The value on V pulled back along g|_{U'} and cleaned is the final state pulled back along
g|_{U'} (eraseEmpty_pullback_eraseEmpty, pullback_comp).
The two alignments with the virtual descent #
theorem
Hironaka.Manifold.BMOmod.imageValueAt_eq_preJoin
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg))
(hUV : ⇑g '' ↑U' ⊆ ↑V)
:
imageValueAt T m hT bo ⋯ ⋯ t hm hmt g hg U' V hV (stepALinks T t V hV) ⋯ ⋯ ⋯ = ((descentStateAux ((T.pullback g hg).pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (preJoin g U' hU' V hV) ⋯
(preJoinBound T g hg U' hU' V hV + 1 - t) ⋯ (preJoinBound T g hg U' hU' V hV) ⋯
(preJoinBound T g hg U' hU' V hV + 1 - t) ⋯ ⋯).L.pullback
(N.restrictLE ⋯) ⋯).eraseEmpty
The canonical descent of V over M, pulled back along g|_{U'}, aligned with the virtual
descent of the pair U', V over N and read on U'.
theorem
Hironaka.Manifold.BMOmod.stepAFamOn_pullback_eq_preJoin
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
(V : TopologicalSpace.Opens M.carrier)
(hV : IsCompact (closure ↑V))
(hT' : Manifold.AnalyticTriple.BMOClass m (T.pullback g hg))
(hUV : ⇑g '' ↑U' ⊆ ↑V)
:
stepAFamOn (T.pullback g hg) m hT' bo ⋯ ⋯ t hm hmt U' hU' = ((descentStateAux ((T.pullback g hg).pullback ContMDiffMap.id ⋯) m ⋯ bo ⋯ ⋯ t hm hmt (preJoin g U' hU' V hV) ⋯
(preJoinBound T g hg U' hU' V hV + 1 - t) ⋯ (preJoinBound T g hg U' hU' V hV) ⋯
(preJoinBound T g hg U' hU' V hV + 1 - t) ⋯ ⋯).L.pullback
(N.restrictLE ⋯) ⋯).eraseEmpty
The canonical descent of U' over N for the pulled-back triple, aligned with the virtual
descent of the pair U', V and read on U'.
Commutation with local isomorphisms #
theorem
Hironaka.Manifold.BMOmod.stepAFamOn_pullback
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
{M N : AnalyticManifold 𝕜 (Fin n → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M)
(m : ℕ)
(hT : Manifold.AnalyticTriple.BMOClass m T)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g)
{T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N}
(hpull : T'.IsPullbackOf T g)
(hT' : Manifold.AnalyticTriple.BMOClass m T')
(U' : TopologicalSpace.Opens N.carrier)
(hU' : IsCompact (closure ↑U'))
:
stepAFamOn T' m hT' bo ⋯ ⋯ t hm hmt U' hU' = ((stepAFamOn T m hT bo ⋯ ⋯ t hm hmt (AnalyticMap.imageOpens g hg U') ⋯).pullback
(AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty
The value of the rounds commutes with local analytic isomorphisms (the analogue of
[Kol07, Theorem 103 (2)]; [Kol07, 34.1]): for T' a pull-back of T along g, the value on U'
is the value on g(U')
pulled back along g|_{U'} and cleaned of empty blow-ups. Both sides are the virtual descent of the
pair U', g(U') read on U' (stepAFamOn_pullback_eq_preJoin, imageValueAt_eq_preJoin).
The family functor of the rounds #
noncomputable def
Hironaka.Manifold.BMOmod.stepAFunctor
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
(m : ℕ)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
:
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} =>
Manifold.AnalyticTriple.BMOClass m
The family functor of the rounds on the nonmonomial part on the marked class BMOClass m:
the compatible family stepAFam for every triple of the class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Hironaka.Manifold.BMOmod.stepAFunctor_fam_seqOn
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
(m : ℕ)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
{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))
:
theorem
Hironaka.Manifold.BMOmod.stepAFunctor_commutesWithLocalIsos
{𝕜 : Type}
[RCLike 𝕜]
{n : ℕ}
(m : ℕ)
(bo : (d : ℕ) → BOanFam 𝕜 n d)
(hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)))
(t : ℕ)
(hm : 1 ≤ m)
(hmt : m ≤ t)
:
(stepAFunctor m bo ⋯ ⋯ t hm hmt).CommutesWithLocalIsos
The family functor of the rounds commutes with local analytic isomorphisms (the analogue of [Kol07, Theorem 103 (2)]).