The transport of the functor's data along an analytic isomorphism

The functoriality of the blow-up sequence under local isomorphisms [Kol07, Definition 30.1]: for a triple T of the class of bed on M, a relatively compact open W and an analytic isomorphism Θ : A ≅ M|W, the functor's sequence on T|W (seqOn, LocalResolutionOn.lean), the ideal T.I|W, its strict-transform chain and the morphism Π_r|_{Ỹ} of closed subspaces are transported onto A (BlowUpSequence.pullback, strictTransformSubspaceSeq): the transported last transform is the pull-back of lastIdealOn along the lifted Θ, it is non-singular (clause (3) of hbed, transported along the diffeomorphism), and the two identifications homOfPullbackEq with localResolutionOn/Sp(W)/T.I|W make the transport square commute. These are the data (seq, ideal, transform, isNonsingular_last, map, map_comp) of an AmbientBlowUpFactorization on an ambient of the form that structure asks for, once A := sigmaOpens G' (AmbientLift.lean).

Not in the sources; bookkeeping.

theorem Manifold.IdealSheaf.isNonsingular_of_isNonsingular_toAnalyticSpace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) (h : J.toAnalyticSpace.IsNonsingular) : J.IsNonsingular

The sheaf-level non-singularity of J (every stalk 𝒪_x/J_x on the support regular) from the space-level one of Sp(A)/J (regularLocus = univ): the stalks of the closed subspace are the quotients (ClosedSubspace.isNonsingular_iff_forall). Internal.

noncomputable def Hironaka.Manifold.BEDanFamStar.ambSeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) A

The functor's sequence on T|W, transported onto A along the analytic isomorphism Θ : A ≅ M|W (BlowUpSequence.pullback at a diffeomorphism; [Kol07, Definition 30.1]).

Equations

• bed.ambSeqOn T hT W hW Θ = (bed.seqOn T hT W hW).pullback Θ.toAnalyticMap ⋯

noncomputable def Hironaka.Manifold.BEDanFamStar.ambIdealOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : A.IdealSheaf

The ideal T.I|W transported onto A.

Equations

• Hironaka.Manifold.BEDanFamStar.ambIdealOn T W Θ = Manifold.IdealSheaf.pullback ⇑Θ.toAnalyticMap ⋯ (Hironaka.Manifold.BEDanFamStar.restrictedIdealOn T W)

noncomputable def Hironaka.Manifold.BEDanFamStar.ambTransformOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) (k : Fin ((bed.ambSeqOn T hT W hW Θ).toSuccession.length + 1)) : ((bed.ambSeqOn T hT W hW Θ).toSuccession.stage k).IdealSheaf

The strict-transform chain of the transported ideal along the transported sequence (the field transform of AmbientBlowUpFactorization).

Equations

• bed.ambTransformOn T hT W hW Θ k = (bed.ambSeqOn T hT W hW Θ).toSuccession.strictTransformSubspaceSeq (Hironaka.Manifold.BEDanFamStar.ambIdealOn T W Θ) k

noncomputable def Hironaka.Manifold.BEDanFamStar.ambLastOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : ((bed.ambSeqOn T hT W hW Θ).toSuccession.stage (Fin.last (bed.ambSeqOn T hT W hW Θ).toSuccession.length)).IdealSheaf

Its last member.

Equations

• bed.ambLastOn T hT W hW Θ = bed.ambTransformOn T hT W hW Θ (Fin.last (bed.ambSeqOn T hT W hW Θ).toSuccession.length)

noncomputable def Hironaka.Manifold.BEDanFamStar.ambLiftLastOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ((bed.ambSeqOn T hT W hW Θ).toSuccession.stage (Fin.last (bed.ambSeqOn T hT W hW Θ).toSuccession.length)).carrier ((bed.seqOn T hT W hW).toSuccession.stage (Fin.last (bed.seqOn T hT W hW).toSuccession.length)).carrier ⊤

The last-stage lift of Θ, a diffeomorphism.

Equations

• bed.ambLiftLastOn T hT W hW Θ = (bed.seqOn T hT W hW).pullbackLiftLastDiffeomorph Θ

theorem Hironaka.Manifold.BEDanFamStar.ambLastOn_eq_comap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : bed.ambLastOn T hT W hW Θ = Manifold.IdealSheaf.pullback ⇑(bed.ambLiftLastOn T hT W hW Θ).toAnalyticMap ⋯ (bed.lastIdealOn T hT W hW)

The transported last transform is the pull-back of the functor's last transform along the lifted Θ.

theorem Hironaka.Manifold.BEDanFamStar.isNonsingular_ambLastOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) (hbed : IsEmbeddedDesing 𝕜 bed) : (bed.ambLastOn T hT W hW Θ).IsNonsingular

The transported last transform is non-singular (the field isNonsingular_last): clause (3) of hbed for T|W, transported along the lifted Θ (isNonsingular_pullbackDiffeomorph_iff).

noncomputable def Hironaka.Manifold.BEDanFamStar.ambMapOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : (bed.ambLastOn T hT W hW Θ).toAnalyticSpace ⟶ (ambIdealOn T W Θ).toAnalyticSpace

Π_r|_{Ỹ} on the transported data (the field map): the morphism of closed subspaces induced by the composite of the transported sequence (the counterpart of localResolutionMapOn).

Equations

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

theorem Hironaka.Manifold.BEDanFamStar.ambMapOn_comp {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : CategoryTheory.CategoryStruct.comp (bed.ambMapOn T hT W hW Θ) (ambIdealOn T W Θ).toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp (bed.ambLastOn T hT W hW Θ).toAnalyticSpaceι (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (bed.ambSeqOn T hT W hW Θ).toSuccession.composite)

It lies over the composite (the field map_comp).

noncomputable def Hironaka.Manifold.BEDanFamStar.ambLastIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : (bed.ambLastOn T hT W hW Θ).toAnalyticSpace ⟶ bed.localResolutionOn T hT W hW

The transported local resolution IS the functor's (homOfPullbackEq along the lifted Θ).

Equations

• bed.ambLastIso T hT W hW Θ = Manifold.IdealSheaf.homOfPullbackEq ⇑(bed.ambLiftLastOn T hT W hW Θ) ⋯ ⋯

theorem Hironaka.Manifold.BEDanFamStar.isIso_ambLastIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : CategoryTheory.IsIso (bed.ambLastIso T hT W hW Θ)

noncomputable def Hironaka.Manifold.BEDanFamStar.ambIdealIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : (ambIdealOn T W Θ).toAnalyticSpace ⟶ (restrictedIdealOn T W).toAnalyticSpace

The transported closed subspace IS Sp(W)/T.I|W (homOfPullbackEq along Θ).

Equations

• Hironaka.Manifold.BEDanFamStar.ambIdealIso T W Θ = Manifold.IdealSheaf.homOfPullbackEq ⇑Θ ⋯ ⋯

theorem Hironaka.Manifold.BEDanFamStar.isIso_ambIdealIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (W : TopologicalSpace.Opens M.carrier) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : CategoryTheory.IsIso (ambIdealIso T W Θ)

theorem Hironaka.Manifold.BEDanFamStar.ambMapOn_square {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bed : BEDanFamStar 𝕜) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (Θ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) A.carrier (M.restrict W).carrier ⊤) : CategoryTheory.CategoryStruct.comp (bed.ambLastIso T hT W hW Θ) (bed.localResolutionMapOn T hT W hW) = CategoryTheory.CategoryStruct.comp (bed.ambMapOn T hT W hW Θ) (ambIdealIso T W Θ)

The transport square: Π_r|_{Ỹ} on the transported data is localResolutionMapOn through the two identifications (Hom.ext_of_comp_quotientι, four quotientMap_comp_quotientι squares and the manifold square stageMap_last_pullbackLiftLast).