The restriction of a piece embedding to an open sub-piece

Włodarczyk: if Y_Z ⊂ Y_{Z'} is an open embedding of germs then it extends to an open embedding U_Z ⊂ U_{Z'} of the ambient manifolds [Wlo09, §4, (3)⇒(4)]; Kollár builds the resolution of a variety from local embeddings into affine spaces, the local resolutions being compared through the uniqueness up to automorphisms [Kol07, Theorem 36, proof]. For a piece embedding E : PieceEmbedding 𝕜 n X V (an ambient G ⊆ 𝕜ⁿ, a reduced nowhere-zero ideal sheaf 𝓘 on Sp(G) and the model isomorphism emb : X|V ≅ Sp(G)/𝓘) and an open V' ⊆ V of X, this module builds the restricted piece embedding E|V' : PieceEmbedding 𝕜 n X V' — the embedding to which the independence of the local resolution from the embedding (LocalResolutionIndependentOn, PieceGlueProof.lean) is applied over the overlaps of the pieces in the gluing of the local resolutions:

• PieceEmbedding.restrictAmbient E hV' — the shrunk ambient G' := G ∖ amb(V ∖ V'): the ambient image of the (closed) part of the piece outside V' is closed in G (isClosedEmbedding_ambientPoint: the closed-subspace inclusion is a closed embedding, emb a homeomorphism), so G' is open, with Y ∩ G' = amb(V') (pieceCoord_ambientPoint_mem_restrictAmbient_iff);
• PieceEmbedding.restrictPiece E hV' hsub — the embedding of X|V' with ambient G', the SAME ideal pulled back along the inclusion Sp(G') → Sp(G) (pieceAmbientIncl, a local analytic isomorphism onto the open coordPreimage G' G), its stalk conditions transported along the open embedding (germMap, bijective at a local isomorphism), and the model isomorphism X|V' ≅ Sp(G')/𝓘|G' assembled as X|V' ≅ (X|V)|_W ≅ (Sp(G)/𝓘)|_W ≅ (Sp(G)|_{G'})/(𝓘|_{G'}) ≅ Sp(G')/𝓘' (restrictOpenIso, restrictOpen_quotient_iso, quotient_kIso along ofManifold_restrictOpen_iso and the diffeomorphism pieceAmbientInclDiffeo — the pattern of modelPieceEmbIso, PieceModel.lean), the ideal identity by comap_ofManifoldHom_eq_pullback;
• the point bookkeeping: pieceAmbientIncl_ambientPoint_restrictPiece (the ambient point of a point of the sub-piece, read in Sp(G), is its ambient point in the piece), pieceCoord_ambientPoint_restrictPiece (the same in 𝕜ⁿ), embPreimage_restrictPiece (the points of the sub-piece over W' are the points of the piece over the image of W').

Not in the sources beyond the remarks cited; bookkeeping. The support of a closed subspace is Hironaka's [Hir64, Ch. 0, §1, p. 119].

theorem AnalyticSpace.mem_openOf_of_subset {K : Type} [RCLike K] {X : AnalyticSpace K} {U U' : Set ↑↑X.toPresheafedSpace} (hsub : U' ⊆ U) {x : ↑↑X.toPresheafedSpace} (hx : x ∈ U') : x ∈ X.openOf U

A subset of U lies in the open openOf X U of the restriction — U itself when U is open, everything otherwise (the convention of openOf).

theorem AnalyticSpace.mem_of_mem_openOf {K : Type} [RCLike K] {X : AnalyticSpace K} {U : Set ↑↑X.toPresheafedSpace} (hU : IsOpen U) {x : ↑↑X.toPresheafedSpace} (hx : x ∈ X.openOf U) : x ∈ U

A point of the open openOf X U of an OPEN U lies in U.

theorem AnalyticSpace.KLocallyRingedSpace.compat_id_of_eq {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {J₁ J₂ : Manifold.IdealSheaf X.𝒪} (h : J₁ = J₂) : QuotientSpace.Compat (↑(CategoryTheory.CategoryStruct.id X)) J₁ J₂

The identity is compatible (Compat) with two EQUAL ideal sheaves.

noncomputable def AnalyticSpace.KLocallyRingedSpace.quotientIsoOfEq {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {J₁ J₂ : Manifold.IdealSheaf X.𝒪} (h : J₁ = J₂) : X.quotient J₁ ≅ X.quotient J₂

Transport of a quotient along an equality of its ideal sheaves, the K-isomorphism induced by the identity of the ambient space (quotientMap) — deliberately NOT eqToIso: Lean's kernel would try to normalise the equality's proof when comparing eqToHom terms.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.quotientIsoOfEq_hom_comp_quotientι {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {J₁ J₂ : Manifold.IdealSheaf X.𝒪} (h : J₁ = J₂) : CategoryTheory.CategoryStruct.comp (quotientIsoOfEq h).hom (X.quotientι J₂) = X.quotientι J₁

The transport isomorphism lies over the identity — its hom followed by the canonical morphism is the canonical morphism.

theorem AnalyticSpace.KLocallyRingedSpace.quotient_kIso_inv_comp_quotientMap {K : Type} [RCLike K] {X' X : KLocallyRingedSpace K} (e : X'.KIso X) (J : Manifold.IdealSheaf X.𝒪) : CategoryTheory.CategoryStruct.comp (quotient_kIso e J).inv (quotientMap e.hom (transportIdeal e J) J ⋯) = CategoryTheory.CategoryStruct.id (X.quotient J)

The inverse of the transport isomorphism quotient_kIso, followed by the quotient map of the K-isomorphism, is the identity.

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpen_quotient_iso_inv_comp_quotientMap {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (J : Manifold.IdealSheaf X.𝒪) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (X.restrictOpen_quotient_iso J U).inv (quotientMap (X.ofRestrict U) (X.restrictIdeal J U) J ⋯) = (X.quotient J).ofRestrict (X.quotientOpens J U)

The inverse of the restriction-quotient isomorphism restrictOpen_quotient_iso, followed by the quotient map of the open immersion, is the open immersion of the quotient.

theorem AnalyticSpace.KLocallyRingedSpace.restrictOpenIso_hom_comp_ofRestrict {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (e : X ≅ Y) (V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (restrictOpenIso e V).hom (Y.ofRestrict V) = CategoryTheory.CategoryStruct.comp (X.ofRestrict ((TopologicalSpace.Opens.map (↑e.hom).base).obj V)) e.hom

The restricted K-isomorphism restrictOpenIso e V lies over e — composed with the open immersion of Y | V it is the open immersion of the source followed by e.

theorem AnalyticSpace.KLocallyRingedSpace.val_toFun_restrictOpen_restrictOpen_iso_inv {K : Type} [RCLike K] {X : KLocallyRingedSpace K} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑(X.restrictOpen U).toPresheafedSpace) (z : ↑↑(X.restrictOpen (imageOpens U V)).toPresheafedSpace) : ↑(Hom.toFun ((X.restrictOpen U).ofRestrict V) (Hom.toFun (restrictOpen_restrictOpen_iso U V).inv z)) = ↑z

The restriction-of-a-restriction isomorphism (restrictOpen_restrictOpen_iso) is over X on points — its inverse followed by the two open immersions is the open immersion of the image open.

theorem AnalyticSpace.KLocallyRingedSpace.val_toFun_eqToHom_restrictOpen {K : Type} [RCLike K] {X : KLocallyRingedSpace K} {U U' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (h : U = U') (y : ↑↑(X.restrictOpen U).toPresheafedSpace) : ↑(Hom.toFun (CategoryTheory.eqToHom ⋯) y) = ↑y

Transporting an open subspace along an equality of the opens is the identity on points.

theorem Hironaka.Manifold.isOpenMap_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : IsOpenMap (pieceCoord G)

The coordinate map pieceCoord of a one-piece ambient is an open map (it is the chart at every point, map_nhds_pieceCoord).

theorem Hironaka.Manifold.range_pieceCoord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Set.range (pieceCoord G) = ↑G

The coordinate map of a one-piece ambient has range G.

theorem Hironaka.Manifold.isNonzeroEverywhere_comap_pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (J : (pieceAmbient 𝕜 G).IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) : (Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl h) ⋯ J).IsNonzeroEverywhere

The inverse image of a nowhere-zero ideal sheaf along the inclusion Sp(G') → Sp(G) of a smaller one-piece ambient is nowhere zero — the germ map at a local analytic isomorphism is injective (germMap_bijective_of_isLocalDiffeomorphAt).

theorem Hironaka.Manifold.isReduced_comap_pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (J : (pieceAmbient 𝕜 G).IdealSheaf) (hJ : J.IsReduced) : AnalyticManifold.IdealSheaf.IsReduced (Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl h) ⋯ J)

The inverse image of a reduced ideal sheaf along the inclusion Sp(G') → Sp(G) of a smaller one-piece ambient is reduced — the germ map at a local analytic isomorphism is a ring isomorphism, and a radical ideal maps to a radical ideal (Ideal.map_radical_of_surjective; the argument of IdealSheaf.isReduced_pullback_diffeomorph).

theorem Hironaka.Manifold.isClosedEmbedding_toFun_toAnalyticSpaceι {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) : Topology.IsClosedEmbedding fun (z : ↑↑J.toAnalyticSpace.toPresheafedSpace) => ↑J.toAnalyticSpaceι z

The canonical morphism Sp(A)/J → Sp(A) of a closed subspace is a closed embedding of the underlying spaces — the inclusion of the closed cosupport (range_toFun_closedSubspaceι; the support of a closed subspace, [Hir64, Ch. 0, §1, p. 119]), read into the manifold A.

The embedding as a homeomorphism and as a K-isomorphism; the ambient point is a closed

embedding

noncomputable def Hironaka.Manifold.PieceEmbedding.embKIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : (X.restrictOpen (X.openOf V)).KIso E.ideal.toAnalyticSpace.toKLocallyRingedSpace

The model isomorphism emb : X|V ≅ Sp(G)/𝓘 as a K-isomorphism of the underlying K-local-ringed spaces, with the source in its restrictOpen spelling.

Equations

• E.embKIso = { hom := (CategoryTheory.asIso E.emb).hom, inv := (CategoryTheory.asIso E.emb).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem Hironaka.Manifold.PieceEmbedding.embKIso_hom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : E.embKIso.hom = E.emb

The hom of embKIso is the embedding emb.

noncomputable def Hironaka.Manifold.PieceEmbedding.embHomeomorph {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : ↑↑(X.restrictSet V).toPresheafedSpace ≃ₜ ↑↑E.ideal.toAnalyticSpace.toPresheafedSpace

The model isomorphism as a homeomorphism of the underlying spaces.

Equations

• E.embHomeomorph = { toFun := ↑E.emb, invFun := ↑(CategoryTheory.asIso E.emb).inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Hironaka.Manifold.PieceEmbedding.embHomeomorph_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : E.embHomeomorph y = ↑E.emb y

embHomeomorph evaluates as emb on points.

theorem Hironaka.Manifold.PieceEmbedding.isClosedEmbedding_ambientPoint {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : Topology.IsClosedEmbedding E.ambientPoint

The ambient point map of a piece is a closed embedding X|V → Sp(G) — the closed-subspace inclusion after the homeomorphism emb.

theorem Hironaka.Manifold.PieceEmbedding.isClosed_image_ambientPoint_of_isClosed {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {S : Set ↑↑(X.restrictSet V).toPresheafedSpace} (hS : IsClosed S) : IsClosed (E.ambientPoint '' S)

The ambient image of a closed subset of the piece is closed in Sp(G).

The shrunk ambient G' = G ∖ amb(V ∖ V')

theorem Hironaka.Manifold.PieceEmbedding.isOpen_restrictAmbient {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : IsOpen (↑E.G \ (fun (y : ↑↑(X.restrictSet V).toPresheafedSpace) => pieceCoord E.G (E.ambientPoint y)) '' {y : ↑↑(X.restrictSet V).toPresheafedSpace | ↑y ∉ V'})

The shrunk ambient is open — G minus the coordinate image of the ambient points of the piece outside the open V', a closed set (V ∖ V' is closed in the piece, ambientPoint a closed embedding, pieceCoord an injective open map with range G).

def Hironaka.Manifold.PieceEmbedding.restrictAmbient {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : TopologicalSpace.Opens (Fin n → 𝕜)

The ambient open of the restricted embedding (Włodarczyk's extension of an open embedding of germs to an open embedding U_Z ⊂ U_{Z'} of the ambient manifolds, [Wlo09, §4, (3)⇒(4)]) — G minus the ambient image of the part of the piece outside V', so that Y ∩ G' = amb(V') (pieceCoord_ambientPoint_mem_restrictAmbient_iff).

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.restrictAmbient_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : E.restrictAmbient hV' ≤ E.G

The shrunk ambient lies in the ambient.

theorem Hironaka.Manifold.PieceEmbedding.mem_restrictAmbient {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') {v : Fin n → 𝕜} : v ∈ E.restrictAmbient hV' ↔ v ∈ E.G ∧ ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), pieceCoord E.G (E.ambientPoint y) = v → ↑y ∈ V'

Membership in the shrunk ambient — a point of G whose only preimages in the piece (under the ambient point map) lie in V'.

theorem Hironaka.Manifold.PieceEmbedding.pieceCoord_ambientPoint_mem_restrictAmbient_iff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (y : ↑↑(X.restrictSet V).toPresheafedSpace) : pieceCoord E.G (E.ambientPoint y) ∈ E.restrictAmbient hV' ↔ ↑y ∈ V'

The ambient point of a point of the piece lies in the shrunk ambient iff the point lies in V' (Włodarczyk's Y ∩ U_Z = Y_Z, [Wlo09, §4, (3)⇒(4)]) — the ambient point map is injective.

The restricted embedding: its model isomorphism, assembled

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.PieceEmbedding.ambientSpace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : AnalyticSpace.KLocallyRingedSpace 𝕜

The ambient K-space Sp(G) of the piece.

Equations

• E.ambientSpace = (AnalyticSpace.toSpace (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Hironaka.Manifold.pieceAmbient 𝕜 E.G)).toKLocallyRingedSpace

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.PieceEmbedding.restrictAmbientSpace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : AnalyticSpace.KLocallyRingedSpace 𝕜

The shrunk ambient K-space Sp(G').

Equations

• E.restrictAmbientSpace hV' = (AnalyticSpace.toSpace (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Hironaka.Manifold.pieceAmbient 𝕜 (E.restrictAmbient hV'))).toKLocallyRingedSpace

noncomputable def Hironaka.Manifold.PieceEmbedding.subPieceOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : TopologicalSpace.Opens ↑↑E.ideal.toAnalyticSpace.toPresheafedSpace

The open of the closed subspace Sp(G)/𝓘 lying over the shrunk ambient G' (quotientOpens at coordPreimage G' G).

Equations

• E.subPieceOpens hV' = E.ambientSpace.quotientOpens E.ideal (Hironaka.Manifold.coordPreimage (E.restrictAmbient hV') E.G)

noncomputable def Hironaka.Manifold.PieceEmbedding.subPieceOpens₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : TopologicalSpace.Opens ↑↑(X.restrictOpen (X.openOf V)).toPresheafedSpace

The open of the piece X|V over the shrunk ambient — the preimage of subPieceOpens under emb; its points are those of embPreimage at coordPreimage G' G.

Equations

• E.subPieceOpens₁ hV' = (TopologicalSpace.Opens.map (↑E.emb).base).obj (E.subPieceOpens hV')

theorem Hironaka.Manifold.PieceEmbedding.mem_subPieceOpens₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (y : ↑↑(X.restrictOpen (X.openOf V)).toPresheafedSpace) : y ∈ E.subPieceOpens₁ hV' ↔ pieceCoord E.G (E.ambientPoint y) ∈ E.restrictAmbient hV'

A point of the piece lies in subPieceOpens₁ iff its ambient coordinate lies in the shrunk ambient.

theorem Hironaka.Manifold.PieceEmbedding.range_ofRestrict_eq_range_subPieceOpens₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (X.ofRestrict (X.openOf V'))) = Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((X.restrictOpen (X.openOf V)).ofRestrict (E.subPieceOpens₁ hV')) (X.ofRestrict (X.openOf V))))

The two open immersions into X — of X|V' and of the open of X|V over the shrunk ambient — have the same range, V' (pieceCoord_ambientPoint_mem_restrictAmbient_iff).

theorem Hironaka.Manifold.PieceEmbedding.imageOpens_subPieceOpens₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : AnalyticSpace.KLocallyRingedSpace.imageOpens (X.openOf V) (E.subPieceOpens₁ hV') = X.openOf V'

The image in X of the open of the piece over the shrunk ambient is V' (imageOpens: the range of the composite open immersion).

noncomputable def Hironaka.Manifold.PieceEmbedding.subPieceIso₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : (X.restrictSet V').toKLocallyRingedSpace ≅ (X.restrictOpen (X.openOf V)).restrictOpen (E.subPieceOpens₁ hV')

X|V' ≅ (X|V)|_W, W the open of the piece over the shrunk ambient — the restriction of a restriction is the restriction to the image open (restrictOpen_restrictOpen_iso), the image being V'.

Equations

• E.subPieceIso₁ hV' hsub = CategoryTheory.eqToIso ⋯ ≪≫ (AnalyticSpace.KLocallyRingedSpace.restrictOpen_restrictOpen_iso (X.openOf V) (E.subPieceOpens₁ hV')).symm

theorem Hironaka.Manifold.PieceEmbedding.val_toFun_subPieceIso₁ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) (y : ↑↑(X.restrictSet V').toPresheafedSpace) : ↑(AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((X.restrictOpen (X.openOf V)).ofRestrict (E.subPieceOpens₁ hV')) (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.subPieceIso₁ hV' hsub).hom y)) = ↑y

The isomorphism X|V' ≅ (X|V)|_W is over X on points.

noncomputable def Hironaka.Manifold.PieceEmbedding.restrictAmbientKIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : (E.restrictAmbientSpace hV').KIso (E.ambientSpace.restrictOpen (coordPreimage (E.restrictAmbient hV') E.G))

The K-isomorphism Sp(G') ≅ Sp(G) | coordPreimage G' G — Sp of the diffeomorphism pieceAmbientInclDiffeo, then Sp(U) ≅ Sp(G)|U (ofManifold_restrictOpen_iso).

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.restrictAmbientKIso_hom_comp_ofRestrict {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : CategoryTheory.CategoryStruct.comp (E.restrictAmbientKIso hV').hom (E.ambientSpace.ofRestrict (coordPreimage (E.restrictAmbient hV') E.G)) = AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑(pieceAmbientIncl ⋯) ⋯

The K-isomorphism Sp(G') ≅ Sp(G)|U followed by the open immersion Sp(G)|U → Sp(G) is Sp of the inclusion pieceAmbientIncl.

theorem Hironaka.Manifold.PieceEmbedding.transportIdeal_restrictAmbientKIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') : AnalyticSpace.KLocallyRingedSpace.transportIdeal (E.restrictAmbientKIso hV') (E.ambientSpace.restrictIdeal E.ideal (coordPreimage (E.restrictAmbient hV') E.G)) = Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl ⋯) ⋯ E.ideal

The restricted ideal 𝓘|_U, transported along Sp(G') ≅ Sp(G)|U, is the pullback of 𝓘 along the inclusion Sp(G') → Sp(G) (comap_ofManifoldHom_eq_pullback).

noncomputable def Hironaka.Manifold.PieceEmbedding.restrictPieceEmbIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : (X.restrictSet V').toKLocallyRingedSpace ≅ (AnalyticManifold.IdealSheaf.toAnalyticSpace (Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl ⋯) ⋯ E.ideal)).toKLocallyRingedSpace

The model isomorphism of the restricted embedding, X|V' ≅ Sp(G')/𝓘' — assembled as X|V' ≅ (X|V)|_W ≅ (Sp(G)/𝓘)|_W ≅ (Sp(G)|_U)/(𝓘|_U) ≅ Sp(G')/𝓘' (the pattern of modelPieceEmbIso, PieceModel.lean).

Equations

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

noncomputable def Hironaka.Manifold.PieceEmbedding.restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : PieceEmbedding 𝕜 n X V'

The restricted piece embedding E|V' of an open V' ⊆ V (Włodarczyk's extension of an open embedding Y_Z ⊂ Y_{Z'} of germs to an open embedding U_Z ⊂ U_{Z'} of the ambient manifolds, [Wlo09, §4, (3)⇒(4)]) — the ambient shrunk to restrictAmbient, the SAME ideal pulled back along the inclusion Sp(G') → Sp(G), its stalk conditions transported along the open embedding, the model isomorphism restricted (restrictPieceEmbIso). The embedding to which the independence of the local resolution from the embedding (LocalResolutionIndependentOn) is applied over an overlap of two pieces.

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.restrictPiece_G {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : (E.restrictPiece hV' hsub).G = E.restrictAmbient hV'

The ambient of the restricted embedding is the shrunk ambient (by rfl).

theorem Hironaka.Manifold.PieceEmbedding.restrictPiece_ideal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) : (E.restrictPiece hV' hsub).ideal = Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl ⋯) ⋯ E.ideal

The ideal of the restricted embedding is the pullback of 𝓘 along the inclusion (by rfl); the commutation of the functor with local analytic isomorphisms (IsEmbeddedDesing, [Wlo09, Theorem 2.0.2(4)]) is read on it.

theorem Hironaka.Manifold.PieceEmbedding.val_mem_openOf {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {V V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) (y : ↑↑(X.restrictSet V').toPresheafedSpace) : ↑y ∈ X.openOf V

A point of the sub-piece X|V' as a point of the piece X|V.

theorem Hironaka.Manifold.PieceEmbedding.pieceAmbientIncl_ambientPoint_restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) (y : ↑↑(X.restrictSet V').toPresheafedSpace) : (pieceAmbientIncl ⋯) ((E.restrictPiece hV' hsub).ambientPoint y) = E.ambientPoint ⟨↑y, ⋯⟩

The ambient point of a point of the sub-piece, read in Sp(G), is its ambient point in the piece — the model isomorphism of the restricted embedding lies over the inclusion of the ambients, factor by factor.

theorem Hironaka.Manifold.PieceEmbedding.pieceCoord_ambientPoint_restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) (y : ↑↑(X.restrictSet V').toPresheafedSpace) : pieceCoord (E.restrictPiece hV' hsub).G ((E.restrictPiece hV' hsub).ambientPoint y) = pieceCoord E.G (E.ambientPoint ⟨↑y, ⋯⟩)

The ambient point of a point of the sub-piece is its ambient point in the piece, read in 𝕜ⁿ.

theorem Hironaka.Manifold.PieceEmbedding.embPreimage_restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {V' : Set ↑↑X.toPresheafedSpace} (hV' : IsOpen V') (hsub : V' ⊆ V) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 (E.restrictAmbient hV')).carrier) (y : ↑↑(X.restrictSet V').toPresheafedSpace) : y ∈ (E.restrictPiece hV' hsub).embPreimage W' ↔ E.ambientPoint ⟨↑y, ⋯⟩ ∈ pieceAmbientImageOpens ⋯ W'

The points of the sub-piece over an open W' of the shrunk ambient are the points of the piece over the image of W' (in V').