The restriction of a piece's local resolution to a smaller open

The functoriality of the sequence functor under open embeddings ([Kol07, Definition 30.1]), at the inclusion W' ↪ W of two relatively compact opens of a piece's ambient: the restriction Ỹ(W') → Ỹ(W) of the piece's local resolution (localResolutionHomOn of LocalResolutionOn.lean at the identity of the ambient) — an open immersion onto the part over W', lying over Sp(W' ↪ W) on the closed subspaces, compatible with the piece maps to X (the identity of the two restriction-of-a-quotient maps). With the generic tools the lift of the glued space into the last transform (AmbientLift.lean) uses: the point lemmas of isomorphisms of K-spaces, open immersions as monomorphisms, Sp(f) ≫ Sp(g) = Sp(g ∘ f), and the characterisation of the points of the piece over W lying over an open W'. Not in the sources beyond the functoriality cited; bookkeeping.

theorem Hironaka.Manifold.KIso.surjective_toFun_hom {𝕜 : Type} [RCLike 𝕜] {A B : AnalyticSpace.KLocallyRingedSpace 𝕜} (e : A ≅ B) : Function.Surjective (AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.hom)

The underlying map of an isomorphism of K-spaces is surjective.

theorem Hironaka.Manifold.KIso.surjective_toFun_inv {𝕜 : Type} [RCLike 𝕜] {A B : AnalyticSpace.KLocallyRingedSpace 𝕜} (e : A ≅ B) : Function.Surjective (AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.inv)

The underlying map of the inverse of an isomorphism of K-spaces is surjective.

theorem Hironaka.Manifold.KIso.toFun_hom_toFun_inv {𝕜 : Type} [RCLike 𝕜] {A B : AnalyticSpace.KLocallyRingedSpace 𝕜} (e : A ≅ B) (y : ↑↑B.toPresheafedSpace) : AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.hom (AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.inv y) = y

e.hom ∘ e.inv = id on points.

theorem Hironaka.Manifold.KIso.toFun_inv_toFun_hom {𝕜 : Type} [RCLike 𝕜] {A B : AnalyticSpace.KLocallyRingedSpace 𝕜} (e : A ≅ B) (x : ↑↑A.toPresheafedSpace) : AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.inv (AnalyticSpace.KLocallyRingedSpace.Hom.toFun e.hom x) = x

e.inv ∘ e.hom = id on points.

theorem Hironaka.Manifold.Hom.ext_of_comp_of_isOpenImmersion {𝕜 : Type} [RCLike 𝕜] {A B C : AnalyticSpace.KLocallyRingedSpace 𝕜} (q : B ⟶ C) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑q] {f g : A ⟶ B} (h : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp g q) : f = g

Open immersions of K-spaces are monomorphisms: two morphisms agreeing after an open immersion agree (cancel_mono on the locally ringed spaces).

theorem Hironaka.Manifold.isAnalyticOpenEmbedding_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : Manifold.IsAnalyticOpenEmbedding ContMDiffMap.id

The identity of an analytic manifold is an analytic open embedding.

theorem Hironaka.Manifold.toSpaceHom_comp_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A B C : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f : AnalyticMap A B) (g : AnalyticMap B C) (k : AnalyticMap A C) (h : ∀ (x : A.carrier), g (f x) = k x) : CategoryTheory.CategoryStruct.comp (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) f) (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) g) = AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) k

Sp(f) ≫ Sp(g) = Sp(k) when g ∘ f = k pointwise (ofManifoldHom_comp).

theorem Hironaka.Manifold.PieceEmbedding.restrictedIdeal_eq_pullback_restrictLE {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hle : W' ≤ W) : E.restrictedIdeal W' = Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 E.G).restrictLE hle) ⋯ (E.restrictedIdeal W)

The restricted ideal over W' ≤ W is the pull-back of the one over W along the inclusion W' ↪ W of the restricted manifolds (pullback_inclusion_restrictLE).

theorem Hironaka.Manifold.PieceEmbedding.isPullbackOf_ambientTriple_id {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : E.ambientTriple.IsPullbackOf E.ambientTriple ContMDiffMap.id

The piece triple is its own pull-back along the identity (its divisor is empty).

noncomputable def Hironaka.Manifold.PieceEmbedding.localResolutionRestrictHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : E.localResolution bed W' hW' ⟶ E.localResolution bed W hW

The restriction of the local resolution to a smaller open W' ≤ W ([Kol07, Definition 30.1]): localResolutionHomOn at the identity of the ambient — an open immersion Ỹ(W') → Ỹ(W) onto the part over W'.

Equations

• E.localResolutionRestrictHom bed W hW W' hW' hle hbed = bed.localResolutionHomOn E.ambientTriple ⋯ W hW E.ambientTriple ⋯ ContMDiffMap.id ⋯ ⋯ W' hW' ⋯ hbed

theorem Hironaka.Manifold.PieceEmbedding.isOpenImmersion_localResolutionRestrictHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(E.localResolutionRestrictHom bed W hW W' hW' hle hbed)

theorem Hironaka.Manifold.PieceEmbedding.range_toFun_localResolutionRestrictHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : Set.range ↑(E.localResolutionRestrictHom bed W hW W' hW' hle hbed) = {y : ↑↑(bed.lastIdealOn E.ambientTriple ⋯ W hW).toAnalyticSpace.toPresheafedSpace | ↑(((bed.seqOn E.ambientTriple ⋯ W hW).toSuccession.stageMap (Fin.last (bed.seqOn E.ambientTriple ⋯ W hW).toSuccession.length)) (↑(bed.lastIdealOn E.ambientTriple ⋯ W hW).toAnalyticSpaceι y)) ∈ W'}

Its range: the points of Ỹ(W) whose ambient image lies in W'.

theorem Hironaka.Manifold.PieceEmbedding.localResolutionRestrictHom_comp_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : CategoryTheory.CategoryStruct.comp (E.localResolutionRestrictHom bed W hW W' hW' hle hbed) (E.localResolutionMap bed W hW) = CategoryTheory.CategoryStruct.comp (E.localResolutionMap bed W' hW') (Manifold.IdealSheaf.homOfPullbackEq ⇑((pieceAmbient 𝕜 E.G).restrictLE hle) ⋯ ⋯)

It lies over Sp(W' ↪ W) on the closed subspaces (localResolutionHomOn_comp_map).

theorem Hironaka.Manifold.PieceEmbedding.pieceOverIncl_mem_domOpens_iff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (z : ↑↑(E.restrictedIdeal W).toAnalyticSpace.toPresheafedSpace) : E.pieceOverIncl W z ∈ E.domOpens W' ↔ ↑(↑(E.restrictedIdeal W).toAnalyticSpaceι z) ∈ W'

The open immersion of the piece over W lands in domOpens W' exactly over W': pieceOverIncl W z ∈ domOpens W' iff the ambient point of z lies in W'.

theorem Hironaka.Manifold.PieceEmbedding.homOfPullbackEq_restrictLE_comp_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hle : W' ≤ W) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑((pieceAmbient 𝕜 E.G).restrictLE hle) ⋯ ⋯) (E.restrictedIdealHom W) = E.restrictedIdealHom W'

homOfPullbackEq along W' ↪ W followed by the restriction-of-a-quotient map over W is the one over W' (both lie over Sp(W' ↪ G)). Internal.

theorem Hironaka.Manifold.PieceEmbedding.localResolutionRestrictHom_comp_toSpaceMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : CategoryTheory.CategoryStruct.comp (E.localResolutionRestrictHom bed W hW W' hW' hle hbed) (E.toSpaceMap bed W hW) = E.toSpaceMap bed W' hW'

The restriction Ỹ(W') → Ỹ(W) followed by the piece map of Ỹ(W) is the piece map of Ỹ(W').