The summand inclusions of the pieces' closed subspaces

In the library's form of Kollár's local model (the disjoint union of an affine cover, [Kol07, Proposition 37, proof]), the closed subspace Y₀ = ⊔ᵢ X|Uᵢ of the disjoint union ⊔ᵢ Gᵢ is the disjoint union of the pieces' closed subspaces Sp(Gᵢ)/𝓘ᵢ. Here: the summand inclusion Sp(Gᵢ)/𝓘ᵢ → Sp(⊔ⱼ Gⱼ)/𝓘_Σ — homOfPullbackEq along sigmaMk i, from isPullbackOf_ambientTriple_sigmaTriple (SigmaTripleData.lean) — is an open immersion onto the part of Sp(⊔)/𝓘_Σ over the summand, lying over Sp(sigmaMk i).

Not in the sources; bookkeeping.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sigmaSummandHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : (D.embedding i).ideal.toAnalyticSpace ⟶ D.sigmaTriple.I.toAnalyticSpace

The summand inclusion of the closed subspaces Sp(Gᵢ)/𝓘ᵢ → Sp(⊔ⱼ Gⱼ)/𝓘_Σ: homOfPullbackEq along sigmaMk i ([Kol07, Proposition 37, proof]).

Equations

• D.sigmaSummandHom i = Manifold.IdealSheaf.homOfPullbackEq ⇑(Manifold.sigmaMk (fun (i : D.ι) => Hironaka.Manifold.pieceAmbient 𝕜 (D.embedding i).G) i) ⋯ ⋯

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_sigmaSummandHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.sigmaSummandHom i)

It is an open immersion (isOpenImmersion_homOfPullbackEq_of_injective at the analytic open embedding sigmaMk i).

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_sigmaSummandHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : Set.range ↑(D.sigmaSummandHom i) = {z : ↑↑D.sigmaTriple.I.toAnalyticSpace.toPresheafedSpace | ↑D.sigmaTriple.I.toAnalyticSpaceι z ∈ Set.range ⇑(Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i)}

Its range: the points of Sp(⊔)/𝓘_Σ over the summand.

theorem Hironaka.Manifold.LocalEmbeddingData.sigmaSummandHom_comp_toAnalyticSpaceι {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : CategoryTheory.CategoryStruct.comp (D.sigmaSummandHom i) D.sigmaTriple.I.toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp (D.embedding i).ideal.toAnalyticSpaceι (AnalyticSpace.toSpaceHom (ContinuousLinearEquiv.refl 𝕜 (Fin D.n → 𝕜)) (Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i))

It lies over Sp(sigmaMk i) (homOfPullbackEq_comp_toAnalyticSpaceι).