The local resolution of a triple over an open, and its transport along an open embedding

The value of the embedded desingularization functor bed on a triple T of the class over a relatively compact open W is a finite blow-up sequence on M|W (the canonical embedded desingularization of a local embedding, [Wlo09, §4, (3)⇒(4)]); the local resolution of T over W is the closed subspace of the last stage cut out by the final strict transform of T.I|W, with its map to Sp(W)/T.I|W (localResolutionOn, localResolutionMapOn, defined in PieceResolution.lean, where the localResolution of a piece is their instance at the piece's ambient triple).

For an analytic open embedding g : N → M with T' the pull-back of T and relatively compact W' ⊆ N, W ⊆ M with g(W') ⊆ W, the value over W' is the pull-back of the value over W along g|W', empty blow-ups erased (the commutation with smooth morphisms, [Kol07, 34.1] — hbed's CommutesWithLocalIsos — and the family's restriction compatibility, [Wlo09, Theorem 2.0.2(5)]), so the final strict transforms correspond under the last-stage lift (the lift of [Kol07, Definition 30.1]; the transports of LocalResolutionRestrict.lean) and the local resolution of T' over W' is the part of the local resolution of T over W lying over g(W') (localResolutionHomOn, an open immersion over the restricted closed subspaces) — the transport exists_localResolution_restrictPiece_iso of PieceRestrictResolution.lean made generic in the open embedding, for the disjoint-union presentation of the local model ([Kol07, Proposition 37, proof]).

Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.BEDanFamStar.restrictedIdealOn_eq_pullback_restrictMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (g : AnalyticMap N M) (W' : TopologicalSpace.Opens N.carrier) (hle : ⇑g '' ↑W' ⊆ ↑W) (hpb : T'.IsPullbackOf T g) : restrictedIdealOn T' W' = Manifold.IdealSheaf.pullback ⇑(AnalyticMap.restrictMap g W' W hle) ⋯ (restrictedIdealOn T W)

The restricted ideal of the pulled-back triple over W' is the pull-back, along the restricted embedding g|W' : W' → W, of the restricted ideal of T over W — both are T.I pulled back along W' → M (pullback_pullback).

theorem Hironaka.Manifold.BEDanFamStar.seqOn_eq_of_isAnalyticOpenEmbedding {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : bed.seqOn T' hT' W' hW' = ((bed.seqOn T hT W hW).pullback (AnalyticMap.restrictMap g W' W hle) ⋯).eraseEmpty

The sequence identity along an open embedding of triples ([Kol07, 34.1]; [Wlo09, Theorem 2.0.2(5)]): the value over W' is the pull-back along g|W' : W' → W of the value over W, empty blow-ups erased — hbed's CommutesWithLocalIsos at g and U' := W' (onto the image open g(W')), the family's restriction compatibility from g(W') up to W, eraseEmpty_pullback_eraseEmpty and pullback_comp.

noncomputable def Hironaka.Manifold.BEDanFamStar.liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : AnalyticMap ((bed.seqOn T' hT' W' hW').stage (Fin.last (bed.seqOn T' hT' W' hW').length)) ((bed.seqOn T hT W hW).stage (Fin.last (bed.seqOn T hT W hW).length))

The last-stage lift along the open embedding (the lift of [Kol07, Definition 30.1]): stageOfEq of the sequence identity, eraseEmptyLast⁻¹, pullbackLiftLast (the pattern of liftOfLe, LocalResolutionRestrict.lean).

Equations

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

theorem Hironaka.Manifold.BEDanFamStar.isLocalDiffeomorph_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)

The lift is a local analytic isomorphism.

theorem Hironaka.Manifold.BEDanFamStar.injective_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : Function.Injective ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)

The lift is injective (g|W' is).

theorem Hironaka.Manifold.BEDanFamStar.stageMap_last_liftOn' {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) (p : ((bed.seqOn T' hT' W' hW').stage (Fin.last (bed.seqOn T' hT' W' hW').length)).carrier) : ((bed.seqOn T hT W hW).toSuccession.stageMap (Fin.last (bed.seqOn T hT W hW).toSuccession.length)) ((bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) p) = (AnalyticMap.restrictMap g W' W hle) (((bed.seqOn T' hT' W' hW').toSuccession.stageMap (Fin.last (bed.seqOn T' hT' W' hW').toSuccession.length)) p)

The lift lies over g|W' (stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast_symm, stageMap_last_stageOfEq). Internal.

theorem Hironaka.Manifold.BEDanFamStar.stageMap_last_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) (p : ((bed.seqOn T' hT' W' hW').stage (Fin.last (bed.seqOn T' hT' W' hW').length)).carrier) : ↑(((bed.seqOn T hT W hW).toSuccession.stageMap (Fin.last (bed.seqOn T hT W hW).toSuccession.length)) ((bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) p)) = g ↑(((bed.seqOn T' hT' W' hW').toSuccession.stageMap (Fin.last (bed.seqOn T' hT' W' hW').toSuccession.length)) p)

The lift lies over g: the ambient point of the image is g of the ambient point.

theorem Hironaka.Manifold.BEDanFamStar.range_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : Set.range ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) = ⇑((bed.seqOn T hT W hW).toSuccession.stageMap (Fin.last (bed.seqOn T hT W hW).toSuccession.length)) ⁻¹' Set.range ⇑(AnalyticMap.restrictMap g W' W hle)

The range of the lift is the part of the last stage over g(W') (range_pullbackLiftLast). Internal.

theorem Hironaka.Manifold.BEDanFamStar.lastIdealOn_eq_pullback_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : bed.lastIdealOn T' hT' W' hW' = Manifold.IdealSheaf.pullback ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) ⋯ (bed.lastIdealOn T hT W hW)

The final strict transforms correspond under the lift (strictTransformSubspaceSeq_last_of_eq_pullback_eraseEmpty).

noncomputable def Hironaka.Manifold.BEDanFamStar.localResolutionHomOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : bed.localResolutionOn T' hT' W' hW' ⟶ bed.localResolutionOn T hT W hW

The morphism of local resolutions along an open embedding of triples (Kol07, Theorem 36, proof): homOfPullbackEq along the lift.

Equations

• bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed = Manifold.IdealSheaf.homOfPullbackEq ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) ⋯ ⋯

theorem Hironaka.Manifold.BEDanFamStar.isOpenImmersion_localResolutionHomOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)

It is an open immersion (isOpenImmersion_homOfPullbackEq_of_injective at the injective local isomorphism liftOn).

theorem Hironaka.Manifold.BEDanFamStar.range_toFun_localResolutionHomOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : Set.range ↑(bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) = {y : ↑↑(bed.lastIdealOn T hT W hW).toAnalyticSpace.toPresheafedSpace | ↑(((bed.seqOn T hT W hW).toSuccession.stageMap (Fin.last (bed.seqOn T hT W hW).toSuccession.length)) (↑(bed.lastIdealOn T hT W hW).toAnalyticSpaceι y)) ∈ ⇑g '' ↑W'}

Its range is the part of the local resolution of T over g(W') (range_toFun_homOfPullbackEq, range_liftOn, range_restrictMap).

theorem Hironaka.Manifold.BEDanFamStar.localResolutionHomOn_comp_map {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : IsEmbeddedDesing 𝕜 bed) : CategoryTheory.CategoryStruct.comp (bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) (bed.localResolutionMapOn T hT W hW) = CategoryTheory.CategoryStruct.comp (bed.localResolutionMapOn T' hT' W' hW') (Manifold.IdealSheaf.homOfPullbackEq ⇑(AnalyticMap.restrictMap g W' W hle) ⋯ ⋯)

It lies over the restricted closed subspaces: the square of the local resolution maps with Sp(g|W') on the closed subspaces, closed by Hom.ext_of_comp_quotientι (quotientMap_comp_quotientι four times, the composite of the ambient maps by stageMap_last_liftOn, ofManifoldHom_comp).