The chaining of the closed-embedding commutation, III: the chaining lemma #
[Kol07, 108] reduces the commutation of the order-reduction functors with closed embeddings to
the hypersurface case along a flag Y = Y₀ ⊂ Y₁ ⊂ ⋯ ⊂ Y_c = X, the question being local. This
module proves the step of that reduction, (E1): if B₂ commutes with closed embeddings of
codimension s through B₁ and B₁ with hypersurfaces through B₀, then B₂ commutes with
closed embeddings of codimension s + 1 through B₀; and the induction it drives, (E3), for a
tower of functors at the standard models. The sources say only that the question is local; the
route through a flag cover is spelled out here:
- (E-a), (E-b)
IsClosedSubmanifold.diffeomorphRestrict,BlowUpSequence.pushforward_pullback_diffeomorph: an analytic isomorphism of the ambient manifolds carrying one closed submanifold onto another restricts to an isomorphism of the bundled submanifolds, and push-forward ([Kol07, Definition 30, 30.3]) commutes with the pull-back along it (pushforwardAux_pullbackat the trivial stages); - (E-c)
BlowUpSequence.pushforwardRestrict_pushforwardRestrict_of_flag: the per-open form ofpushforward_pushforward_of_flag(Hironaka.Resolution.Analytic.Restrict.FlagPushforward): pushing a list forward fromS ∩ UtoY ∩ Uand then toUis pushing it forward fromS ∩ UtoU, the list read on theS ⊂ Ystructure through the identificatione; - the flag case
AnalyticFamilyFunctor.commutesWithClosedEmbeddings_flag_case: on a manifold carrying a global flagS ⊂ Y ⊂ M, the codimension-sclause atY(C), the hypersurface clause of the middle functor atS ⊂ Y(D) and (E-c) give the per-open identity atS; the ideals are handled byHironaka.Resolution.Analytic.Submanifold.FlagIdeal; - (E1)
AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_chain: a relatively compact openUhas a flag cover (FlagCover,Hironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingCover); on its coproductΣthe preimage ofSsits in a global flag, pull-back along the surjective local isomorphismcoverMapis injective ([Kol07, Proposition 37]), both sides of the identity pull back to values of the functors on the pulled-back triples (CommutesWithLocalIsos;pushforwardRestrict_pullback_restrictMapfor the right side), and the flag case onΣidentifies them; - (E3)
AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_tower: induction on the codimension with (E1) at the bottom of the flag and the degenerate case ofHironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingDegeneratewhenn ≤ s.
(E-a) an ambient analytic isomorphism carrying one closed submanifold onto another induces #
an analytic isomorphism of the bundled submanifolds
theorem
Manifold.IsClosedSubmanifold.mapsTo_of_preimage_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(h : SA = ⇑G ⁻¹' SB)
(x : A.carrier)
:
G maps SA = G⁻¹(SB) into SB.
theorem
Manifold.IsClosedSubmanifold.symm_mapsTo_of_preimage_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(h : SA = ⇑G ⁻¹' SB)
(y : B.carrier)
:
G.symm maps SB into SA = G⁻¹(SB).
def
Manifold.IsClosedSubmanifold.restrictMapOfPreimage
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
{c : ℕ}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(hA : IsClosedSubmanifold ψ SA c)
(hB : IsClosedSubmanifold ψ SB c)
(h : SA = ⇑G ⁻¹' SB)
:
The restriction of G to the bundled submanifolds.
Equations
- Manifold.IsClosedSubmanifold.restrictMapOfPreimage G hA hB h = hA.restrictMap hB ⇑G ⋯ ⋯
Instances For
def
Manifold.IsClosedSubmanifold.restrictMapOfPreimageSymm
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
{c : ℕ}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(hA : IsClosedSubmanifold ψ SA c)
(hB : IsClosedSubmanifold ψ SB c)
(h : SA = ⇑G ⁻¹' SB)
:
The restriction of G.symm to the bundled submanifolds.
Equations
- Manifold.IsClosedSubmanifold.restrictMapOfPreimageSymm G hA hB h = hB.restrictMap hA ⇑G.symm ⋯ ⋯
Instances For
def
Manifold.IsClosedSubmanifold.diffeomorphRestrict
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
{c : ℕ}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(hA : IsClosedSubmanifold ψ SA c)
(hB : IsClosedSubmanifold ψ SB c)
(h : SA = ⇑G ⁻¹' SB)
:
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜))
hA.toAnalyticManifold.carrier hB.toAnalyticManifold.carrier ⊤
An analytic isomorphism G : A ≃ B with SA = G⁻¹(SB) restricts to an analytic isomorphism
of the bundled closed submanifolds (both directions IsClosedSubmanifold.restrictMaps, inverse to
each other on the carriers).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Manifold.IsClosedSubmanifold.diffeomorphRestrict_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
{c : ℕ}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(hA : IsClosedSubmanifold ψ SA c)
(hB : IsClosedSubmanifold ψ SB c)
(h : SA = ⇑G ⁻¹' SB)
(p : hA.toAnalyticManifold.carrier)
:
The restricted isomorphism is G on the points.
(E-b) the square: push-forward against pull-back along an ambient isomorphism #
theorem
AnalyticManifold.BlowUpSequence.pushforward_pullback_diffeomorph
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{A B : AnalyticManifold 𝕜 E}
{SA : Set A.carrier}
{SB : Set B.carrier}
{c : ℕ}
(G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤)
(hA : Manifold.IsClosedSubmanifold ψ SA c)
(hB : Manifold.IsClosedSubmanifold ψ SB c)
(h : SA = ⇑G ⁻¹' SB)
(L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - c) → 𝕜)) hB.toAnalyticManifold)
:
(pushforward hB L).pullback ⟨⇑G, ⋯⟩ ⋯ = pushforward hA (L.pullback ⟨⇑(Manifold.IsClosedSubmanifold.diffeomorphRestrict G hA hB h), ⋯⟩ ⋯)
[Kol07, Definition 30, 30.3] transported along an analytic isomorphism of the ambient
manifolds (the square lemma pushforwardAux_pullback at the trivial stages): pulling back the
push-forward along G is pushing forward the pull-back along the induced isomorphism of the
bundled submanifolds.
theorem
AnalyticManifold.BlowUpSequence.pullback_pullback_pullback_eq_pullback_pullback
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M N₁ N₂ N₃ P : AnalyticManifold 𝕜 E}
(L : BlowUpSequence ψ M)
(f₁ : AnalyticMap N₁ M)
(hf₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₁)
(f₂ : AnalyticMap N₂ N₁)
(hf₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₂)
(f₃ : AnalyticMap P N₂)
(hf₃ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₃)
(g₁ : AnalyticMap N₃ M)
(hg₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₁)
(g₂ : AnalyticMap P N₃)
(hg₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g₂)
(h : ∀ (q : P.carrier), (ContMDiffMap.comp f₁ (ContMDiffMap.comp f₂ f₃)) q = (ContMDiffMap.comp g₁ g₂) q)
:
Three pull-backs against two: two chains of local analytic isomorphisms with the same
composite pull a list back to the same list (pullback_comp twice each way, pullback_congr
in the middle).
(E-c) the composition of the per-open push-forwards along the flag #
theorem
Manifold.IsClosedSubmanifold.image_flagDiffeomorph_preimageOpens_subset
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(e :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜))
hSY.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤)
(he : ∀ (x : hSY.toAnalyticManifold.carrier), hS.inclusionMap (e x) = hY.inclusionMap (hSY.inclusionMap x))
(U : TopologicalSpace.Opens M.carrier)
:
⇑e '' ↑(hSY.preimageOpens (hY.preimageOpens U)) ⊆ ↑(hS.preimageOpens U)
The identification of the two bundled structures on S maps the trace of U on S ⊂ Y into
the trace of U on S.
theorem
Manifold.IsClosedSubmanifold.image_flagDiffeomorph_preimageOpens_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(e :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜))
hSY.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤)
(he : ∀ (x : hSY.toAnalyticManifold.carrier), hS.inclusionMap (e x) = hY.inclusionMap (hSY.inclusionMap x))
(U : TopologicalSpace.Opens M.carrier)
:
The identification of the two bundled structures on S maps the trace of U on S ⊂ Y ONTO
the trace of U on S.
theorem
Manifold.IsClosedSubmanifold.restrictOpen_flag
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hsub : S ⊆ Y)
(U : TopologicalSpace.Opens M.carrier)
:
IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑⋯.inclusionMap ⁻¹' ⇑(M.inclusion U) ⁻¹' S) 1
The trace of S on the open U is a hypersurface of the trace of Y (the flag restricted to
U; preimage_val_of_subset at codimension s + 1 - s = 1).
theorem
Manifold.IsClosedSubmanifold.flag_trace_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(U : TopologicalSpace.Opens M.carrier)
:
⇑⋯.inclusionMap ⁻¹' ⇑(M.inclusion U) ⁻¹' S = ⇑(hY.restrictBundleDiffeomorph U).symm ⁻¹' ⇑(hY.toAnalyticManifold.inclusion (hY.preimageOpens U)) ⁻¹' ⇑hY.inclusionMap ⁻¹' S
The trace of S ∩ U in the restricted flag is the preimage, under the bridge of Y, of the
trace of S in Y ∩ U_Y (a set-level identity of the two bundled hypersurfaces).
noncomputable def
Manifold.IsClosedSubmanifold.flagMapS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(e :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜))
hSY.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤)
(he : ∀ (x : hSY.toAnalyticManifold.carrier), hS.inclusionMap (e x) = hY.inclusionMap (hSY.inclusionMap x))
(U : TopologicalSpace.Opens M.carrier)
:
AnalyticMap (hSY.toAnalyticManifold.restrict (hSY.preimageOpens (hY.preimageOpens U)))
(hS.toAnalyticManifold.restrict (hS.preimageOpens U))
f₁: the identification e restricted to the traces of U.
Equations
- hY.flagMapS hS hSY e he U = Hironaka.Manifold.AnalyticMap.restrictMap ⟨⇑e, ⋯⟩ (hSY.preimageOpens (hY.preimageOpens U)) (hS.preimageOpens U) ⋯
Instances For
theorem
Manifold.IsClosedSubmanifold.isLocalDiffeomorph_flagMapS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(e :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜))
hSY.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤)
(he : ∀ (x : hSY.toAnalyticManifold.carrier), hS.inclusionMap (e x) = hY.inclusionMap (hSY.inclusionMap x))
(U : TopologicalSpace.Opens M.carrier)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) ⊤
⇑(hY.flagMapS hS hSY e he U)
f₁ is a local analytic isomorphism (e restricted to opens).
noncomputable def
Manifold.IsClosedSubmanifold.flagBridgeSY
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(U : TopologicalSpace.Opens M.carrier)
:
AnalyticMap ⋯.toAnalyticManifold (hSY.toAnalyticManifold.restrict (hSY.preimageOpens (hY.preimageOpens U)))
f₂: the bridge of S ⊂ Y at U_Y, inverted.
Equations
- hY.flagBridgeSY hSY U = ⟨⇑(hSY.restrictBundleDiffeomorph (hY.preimageOpens U)).symm, ⋯⟩
Instances For
noncomputable def
Manifold.IsClosedSubmanifold.flagBridgeHyp
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hsub : S ⊆ Y)
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(U : TopologicalSpace.Opens M.carrier)
:
f₃: the isomorphism of the two bundled hypersurfaces S ∩ U induced by the bridge of Y.
Equations
- hY.flagBridgeHyp hS hsub hSY U = ⟨⇑(Manifold.IsClosedSubmanifold.diffeomorphRestrict (hY.restrictBundleDiffeomorph U).symm ⋯ ⋯ ⋯), ⋯⟩
Instances For
noncomputable def
Manifold.IsClosedSubmanifold.flagBridgeS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{S : Set M.carrier}
{s : ℕ}
(hS : IsClosedSubmanifold ψ S (s + 1))
(U : TopologicalSpace.Opens M.carrier)
:
AnalyticMap ⋯.toAnalyticManifold (hS.toAnalyticManifold.restrict (hS.preimageOpens U))
g₁: the bridge of S at U, inverted.
Equations
- hS.flagBridgeS U = ⟨⇑(hS.restrictBundleDiffeomorph U).symm, ⋯⟩
Instances For
theorem
Manifold.IsClosedSubmanifold.isLocalDiffeomorph_flagBridgeSY
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(U : TopologicalSpace.Opens M.carrier)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) ⊤
⇑(hY.flagBridgeSY hSY U)
f₂ is a local analytic isomorphism (an inverted bridge).
theorem
Manifold.IsClosedSubmanifold.isLocalDiffeomorph_flagBridgeHyp
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : IsClosedSubmanifold ψ Y s)
(hS : IsClosedSubmanifold ψ S (s + 1))
(hsub : S ⊆ Y)
(hSY : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(U : TopologicalSpace.Opens M.carrier)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) ⊤
⇑(hY.flagBridgeHyp hS hsub hSY U)
f₃ is a local analytic isomorphism (diffeomorphRestrict).
theorem
Manifold.IsClosedSubmanifold.isLocalDiffeomorph_flagBridgeS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{S : Set M.carrier}
{s : ℕ}
(hS : IsClosedSubmanifold ψ S (s + 1))
(U : TopologicalSpace.Opens M.carrier)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) ⊤
⇑(hS.flagBridgeS U)
g₁ is a local analytic isomorphism (an inverted bridge).
theorem
AnalyticManifold.BlowUpSequence.pushforwardRestrict_pushforwardRestrict_of_flag
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
{s : ℕ}
(hY : Manifold.IsClosedSubmanifold ψ Y s)
(hS : Manifold.IsClosedSubmanifold ψ S (s + 1))
(hsub : S ⊆ Y)
(hSY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(e :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜))
hSY.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤)
(he : ∀ (x : hSY.toAnalyticManifold.carrier), hS.inclusionMap (e x) = hY.inclusionMap (hSY.inclusionMap x))
(U : TopologicalSpace.Opens M.carrier)
(L :
BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - (s + 1)) → 𝕜))
(hS.toAnalyticManifold.restrict (hS.preimageOpens U)))
:
pushforwardRestrict hY U (pushforwardRestrict hSY (hY.preimageOpens U) (L.pullback (hY.flagMapS hS hSY e he U) ⋯)) = pushforwardRestrict hS U L
(E), the restricted form of pushforward_pushforward_of_flag ([Kol07, Definition 30, 30.3]
twice): pushing a list forward from the hypersurface S ∩ U of Y ∩ U to Y ∩ U and then to U
is pushing it forward from S ∩ U to U — the list read on the S ⊂ Y structure through e.
From the unrestricted lemma on
M.restrict U, the three pushforwardRestricts unfolded by
pushforwardRestrictOf_eq, the middle push-forward transported along the bridge of Y by
pushforward_pullback_diffeomorph, and the pull-backs composed (pullback_comp, pullback_congr:
all the maps are the identity on the points of S ∩ U).
The pull-back of an empty-divisor triple #
theorem
Manifold.AnalyticTriple.pullback_emptyDivisor
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
[FiniteDimensional 𝕜 E]
{M N : AnalyticManifold 𝕜 E}
(I : M.IdealSheaf)
(hI : IdealSheaf.IsNonzeroEverywhere I)
(g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g)
:
{ I := I, isNonzeroEverywhere := hI, F := HypersurfaceFamily.empty M.carrier, isSnc := ⋯ }.pullback g hg = { I := IdealSheaf.pullback ⇑g ⋯ I, isNonzeroEverywhere := ⋯, F := HypersurfaceFamily.empty N.carrier, isSnc := ⋯ }
The pull-back of an empty-divisor triple along a local analytic isomorphism is the
empty-divisor triple of the pulled-back ideal (HypersurfaceFamily.empty_comap).
The flag cover: the descent map restricted to the bundled preimage of S #
noncomputable def
Hironaka.Manifold.FlagCover.descS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{S : Set M.carrier}
{s : ℕ}
{hS : Manifold.IsClosedSubmanifold ψ S (s + 1)}
{U : TopologicalSpace.Opens M.carrier}
(C : FlagCover hS U)
:
The descent map restricted to the bundled preimage of S
(IsClosedSubmanifold.restrictMap).
Equations
- C.descS = ⋯.restrictMap hS ⇑C.desc ⋯ ⋯
Instances For
theorem
Hironaka.Manifold.FlagCover.isLocalDiffeomorph_descS
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{S : Set M.carrier}
{s : ℕ}
{hS : Manifold.IsClosedSubmanifold ψ S (s + 1)}
{U : TopologicalSpace.Opens M.carrier}
(C : FlagCover hS U)
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - (s + 1)) → 𝕜)) ⊤
⇑C.descS
The restricted descent map is a local analytic isomorphism (isLocalDiffeomorph_restrictMap at
any codimension).
theorem
Hironaka.Manifold.FlagCover.image_descS_preimageOpens_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{S : Set M.carrier}
{s : ℕ}
{hS : Manifold.IsClosedSubmanifold ψ S (s + 1)}
{U : TopologicalSpace.Opens M.carrier}
(C : FlagCover hS U)
:
The restricted descent map carries the trace of the cover's opens on the preimage of S ONTO
the trace of U on S (the cover's opens map onto U).
The flag case of the chaining lemma: (C) + (D) + (E) #
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.commutesWithClosedEmbeddings_flag_case
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{s : ℕ}
{Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ M → Prop}
(B₂ : AnalyticFamilyFunctor ψ fun {M : AnalyticManifold 𝕜 E} => Dom₂)
{Dom₁ :
{M₁ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} →
Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M₁ → Prop}
(B₁ :
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜))
fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom₁)
{Dom₀ :
{M₀ : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)} →
Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜)) M₀ → Prop}
(B₀ :
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜))
fun {M : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)} => Dom₀)
(hDom₁ :
∀ {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y s) (I : M.IdealSheaf)
(hI : Manifold.IdealSheaf.IsNonzeroEverywhere I)
(hJ : (Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I).IsNonzeroEverywhere),
hY.idealSheaf ≤ I →
Dom₂ { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ } →
Dom₁
{ I := Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I, isNonzeroEverywhere := hJ,
F := Manifold.HypersurfaceFamily.empty hY.toAnalyticManifold.carrier, isSnc := ⋯ })
(hB₀ : B₀.CommutesWithLocalIsos)
(hDom₀ :
∀ {M N : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜)) M) (g : AnalyticMap N M)
(hg :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s - 1) → 𝕜)) ⊤
⇑g),
Dom₀ T → Dom₀ (T.pullback g hg))
(hs : B₂.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₁)
(h1 : B₁.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₀)
{M : AnalyticManifold 𝕜 E}
{Y S : Set M.carrier}
(hY : Manifold.IsClosedSubmanifold ψ Y s)
(hS : Manifold.IsClosedSubmanifold ψ S (s + 1))
(hsub : S ⊆ Y)
(hSY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑hY.inclusionMap ⁻¹' S) 1)
(I : M.IdealSheaf)
(hI : Manifold.IdealSheaf.IsNonzeroEverywhere I)
(J : hS.toAnalyticManifold.IdealSheaf)
(hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J)
(hle : hS.idealSheaf ≤ I)
(hJI : J = Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I)
(hT : Dom₂ { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ })
(hT' :
Dom₀
{ I := J, isNonzeroEverywhere := hJ, F := Manifold.HypersurfaceFamily.empty hS.toAnalyticManifold.carrier,
isSnc := ⋯ })
(U : TopologicalSpace.Opens M.carrier)
(hU : IsCompact (closure ↑U))
:
(B₂.fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ } hT).seqOn U
hU = AnalyticManifold.BlowUpSequence.pushforwardRestrict hS U
((B₀.fam
{ I := J, isNonzeroEverywhere := hJ, F := Manifold.HypersurfaceFamily.empty hS.toAnalyticManifold.carrier,
isSnc := ⋯ }
hT').seqOn
(hS.preimageOpens U) ⋯)
The flag case of (E1) ([Kol07, 108]): on a manifold
carrying a global flag S ⊂ Y ⊂ M (Y of codimension s, S a hypersurface of Y), the
per-open identity of the predicate at S follows from the codimension-s clause at Y (C), the
codimension-one clause of the middle functor at S ⊂ Y (D) and the composition of the two
push-forwards (E).
(E1) the chaining lemma and (E3) the tower #
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_chain
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{s : ℕ}
{Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ M → Prop}
(B₂ : AnalyticFamilyFunctor ψ fun {M : AnalyticManifold 𝕜 E} => Dom₂)
(hB₂ : B₂.CommutesWithLocalIsos)
(hDom₂ :
∀ {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ M) (g : AnalyticMap N M)
(hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g),
Dom₂ T → Dom₂ (T.pullback g hg))
{Dom₁ :
{M₁ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} →
Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M₁ → Prop}
(B₁ :
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜))
fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom₁)
(hDom₁ :
∀ {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y s) (I : M.IdealSheaf)
(hI : Manifold.IdealSheaf.IsNonzeroEverywhere I)
(hJ : (Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I).IsNonzeroEverywhere),
hY.idealSheaf ≤ I →
Dom₂ { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ } →
Dom₁
{ I := Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I, isNonzeroEverywhere := hJ,
F := Manifold.HypersurfaceFamily.empty hY.toAnalyticManifold.carrier, isSnc := ⋯ })
{Dom₀ :
{M₀ : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)} →
Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜)) M₀ → Prop}
(B₀ :
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜))
fun {M : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)} => Dom₀)
(hB₀ : B₀.CommutesWithLocalIsos)
(hDom₀ :
∀ {M N : AnalyticManifold 𝕜 (Fin (n - s - 1) → 𝕜)}
(T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s - 1) → 𝕜)) M) (g : AnalyticMap N M)
(hg :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s - 1) → 𝕜)) ⊤
⇑g),
Dom₀ T → Dom₀ (T.pullback g hg))
(hs : B₂.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₁)
(h1 : B₁.CommutesWithClosedEmbeddingsOfEmptyDivisorFam B₀)
:
(E1), the chaining lemma ([Kol07, 108]):
the codimension-s clause of B₂ through B₁ and the codimension-one clause of B₁ through B₀
give the codimension-(s + 1) clause of B₂ through B₀. (A) a flag cover of the relatively
compact open U and its coproduct Σ, on which desc⁻¹ S sits in the global flag
FlagCover.flag of codimension s; pull-back along the surjective local isomorphism coverMap
is injective ([Kol07, Proposition 37]), so it suffices to compare the two pull-backs: (A1) the left
side is the value of B₂ on the pulled-back triple (CommutesWithLocalIsos), (A2) the right side
is the push-forward from desc⁻¹ S of the value of B₀ on the pulled-back triple
(pushforwardRestrict_pullback_restrictMap, CommutesWithLocalIsos along the restricted descent
map), and the flag case (C)–(E) on Σ identifies the two.
theorem
Hironaka.Manifold.AnalyticFamilyFunctor.commutesWithClosedEmbeddingsOfEmptyDivisorFam_tower
{𝕜 : Type}
[RCLike 𝕜]
{Dom :
(n : ℕ) →
{M : AnalyticManifold 𝕜 (Fin n → 𝕜)} → Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M → Prop}
(F :
(n : ℕ) →
AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Dom n)
(hF : ∀ (n : ℕ), (F n).CommutesWithLocalIsos)
(hDomPull :
∀ (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),
Dom n T → Dom n (T.pullback g hg))
(hDomRes :
∀ (n s : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {Y : Set M.carrier}
(hY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y s) (I : M.IdealSheaf)
(hI : Manifold.IdealSheaf.IsNonzeroEverywhere I)
(hJ : (Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I).IsNonzeroEverywhere),
hY.idealSheaf ≤ I →
Dom n { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ } →
Dom (n - s)
{ I := Manifold.IdealSheaf.pullback ⇑hY.inclusionMap ⋯ I, isNonzeroEverywhere := hJ,
F := Manifold.HypersurfaceFamily.empty hY.toAnalyticManifold.carrier, isSnc := ⋯ })
(h0 : ∀ (n : ℕ), (F n).CommutesWithClosedEmbeddingsOfEmptyDivisorFam (F n))
(h1 : ∀ (m : ℕ), 0 < m → (F m).CommutesWithClosedEmbeddingsOfEmptyDivisorFam (F (m - 1)))
(n s : ℕ)
:
(F n).CommutesWithClosedEmbeddingsOfEmptyDivisorFam (F (n - s))
(E3): for a tower F of family functors at
the standard models with the domain hypotheses of (E1) at every level, the codimension-zero and
codimension-one clauses give the clause at every codimension, n - s literal — induction on s
with (E1) at the bottom of the flag when 0 < n - s and the degenerate case of
Hironaka.Resolution.Analytic.Functor.ChainClosedEmbeddingDegenerate when n ≤ s.