The embeddings of the pieces into the disjoint-union model, at a gluing datum

Kollár's local model Y₀ = ⊔ᵢ X|Uᵢ ⊆ X' = ⊔ᵢ Uᵢ [Kol07, Proposition 37, proof]: for a gluing datum and any family of relatively compact opens Wᵢ ⋐ Gᵢ of the pieces' ambients (a gluing datum's, or a shrinking of it for the locally finite factorization), the ambient opens Gᵢ' = pieceCoord '' Wᵢ (ambOpens), the ambient ⊔ᵢ Gᵢ' (ambSpace, a sigmaOpens), Θ₀ : ⊔ᵢ Gᵢ' → ⊔ᵢ Sp(Gᵢ) with its image U_Σ and the analytic isomorphism Θ : ⊔ᵢ Gᵢ' ≅ (⊔ᵢ Sp(Gᵢ))|U_Σ (SigmaCoordMap.lean at the datum), the transported data of AmbientTransport.lean at T := D.sigmaTriple, W := U_Σ (glueIdeal, glueSeq, glueLast, glueMap), and the embeddings emb i : X|pieceDom i Wᵢ ≅ (Sp(⊔ⱼ Gⱼ')/J₀)|overPiece i (glueEmb) of the AmbientBlowUpFactorization: X|pieceDom i Wᵢ ≅ Sp(Wᵢ)/𝓘ᵢ|Wᵢ (the inverse of the open immersion of the piece over Wᵢ, named pieceOverHom), into Sp(⊔ⱼ Gⱼ)/𝓘_Σ by the restriction-of-a-quotient map and the summand inclusion of SigmaSummandHom.lean (sumIn), matched against the part over Gᵢ' sent into Sp(⊔ⱼ Gⱼ)/𝓘_Σ by ambIdealIso and the restriction open immersion over U_Σ (ambIn) — isoOfRangeEq on two open immersions with the same range (the summand characterisation ambTheta₀_mem_image_iff). General tools: IdealSheaf.restrictOpensHom (homOfPullbackEq along W ↪ M) and IdealSheaf.isOpen_overPiece.

Not in the sources beyond Kollár's model; bookkeeping.

noncomputable def Manifold.IdealSheaf.restrictOpensHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : M.IdealSheaf) (W : TopologicalSpace.Opens M.carrier) : (J.restrict W).toAnalyticSpace ⟶ J.toAnalyticSpace

The open immersion Sp(W)/J|W → Sp(M)/J of the restricted closed subspace: homOfPullbackEq along the inclusion W ↪ M (the general form of restrictedIdealHom).

Equations

• Manifold.IdealSheaf.restrictOpensHom J W = Manifold.IdealSheaf.homOfPullbackEq ⇑(M.inclusion W) ⋯ ⋯

theorem Manifold.IdealSheaf.isOpenImmersion_restrictOpensHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : M.IdealSheaf) (W : TopologicalSpace.Opens M.carrier) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(restrictOpensHom J W)

theorem Manifold.IdealSheaf.range_toFun_restrictOpensHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : M.IdealSheaf) (W : TopologicalSpace.Opens M.carrier) : Set.range ↑(restrictOpensHom J W) = {z : ↑↑J.toAnalyticSpace.toPresheafedSpace | ↑J.toAnalyticSpaceι z ∈ W}

theorem Manifold.IdealSheaf.toFun_toAnalyticSpaceι_restrictOpensHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : M.IdealSheaf) (W : TopologicalSpace.Opens M.carrier) (z : ↑↑(J.restrict W).toAnalyticSpace.toPresheafedSpace) : ↑J.toAnalyticSpaceι (↑(restrictOpensHom J W) z) = ↑(↑(J.restrict W).toAnalyticSpaceι z)

theorem Manifold.IdealSheaf.isOpen_overPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ι : Type u} [Countable ι] {G : ι → TopologicalSpace.Opens (Fin n → 𝕜)} (J : (AnalyticManifold.sigmaOpens G).IdealSheaf) (i : ι) : IsOpen (J.overPiece i)

The part of Sp(⊔ Gᵢ)/J over a summand is open (the overPiece of AmbientBlowUpFactorization): the preimage of the clopen summand under the continuous canonical map.

noncomputable def Hironaka.Manifold.PieceEmbedding.pieceOverHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : (E.restrictedIdeal W).toAnalyticSpace.toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace

The open immersion of the piece over W into X — the q of exists_openImmersion_toSpaceMap_eq (ResolutionSnc.lean), named: the restriction-of-a-quotient map, the inverse of the embedding, the inclusion of the piece.

Equations

• E.pieceOverHom W = CategoryTheory.CategoryStruct.comp (E.restrictedIdealHom W) (CategoryTheory.CategoryStruct.comp E.embInv (X.ofRestrict (X.openOf V)))

theorem Hironaka.Manifold.PieceEmbedding.isOpenImmersion_pieceOverHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(E.pieceOverHom W)

theorem Hironaka.Manifold.PieceEmbedding.toFun_pieceOverHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.pieceOverHom W) = E.pieceOverIncl W

theorem Hironaka.Manifold.PieceEmbedding.range_toFun_pieceOverHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.pieceOverHom W)) = ↑(E.domOpens W)

theorem Hironaka.Manifold.PieceEmbedding.toSpaceMap_eq_comp_pieceOverHom {𝕜 : 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)) : E.toSpaceMap bed W hW = CategoryTheory.CategoryStruct.comp (E.localResolutionMap bed W hW) (E.pieceOverHom W)

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

The summand inclusion on points lies over sigmaMk i. Internal.

The constructions below are parametrised by an ARBITRARY family W of relatively compact opens of the pieces' ambients (hW), not only by a gluing datum's W: the locally finite factorization needs pieces pieceDom i (W i) INSIDE a prescribed open of X, which is reached by shrinking W (AmbientFactorization.lean).

def Hironaka.Manifold.LocalEmbeddingData.ambOpens {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : TopologicalSpace.Opens (Fin D.n → 𝕜)

The ambient opens of the model: the coordinate images Gᵢ' = pieceCoord '' Wᵢ ⊆ 𝕜ⁿ of the opens Wᵢ (coordImageOpens).

Equations

• D.ambOpens W i = Hironaka.Manifold.coordImageOpens (D.embedding i).G (W i)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.ambSpace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : AnalyticManifold 𝕜 (Fin D.n → 𝕜)

The ambient ⊔ᵢ Gᵢ' of the model (a sigmaOpens).

Equations

• D.ambSpace W = AnalyticManifold.sigmaOpens (D.ambOpens W)

noncomputable def Hironaka.Manifold.LocalEmbeddingData.ambTheta₀ {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : AnalyticMap (D.ambSpace W) D.sigmaAmbient

Θ₀ : ⊔ᵢ Gᵢ' → ⊔ᵢ Sp(Gᵢ) at the gluing datum (sigmaCoordMap).

Equations

• D.ambTheta₀ W = Hironaka.Manifold.sigmaCoordMap (fun (i : D.ι) => (D.embedding i).G) W

noncomputable def Hironaka.Manifold.LocalEmbeddingData.ambImage {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : TopologicalSpace.Opens D.sigmaAmbient.carrier

U_Σ = ⋃ᵢ sigmaMk i '' Wᵢ, the image of Θ₀ (sigmaCoordImage).

Equations

• D.ambImage W = Hironaka.Manifold.sigmaCoordImage (fun (i : D.ι) => (D.embedding i).G) W

theorem Hironaka.Manifold.LocalEmbeddingData.isCompact_closure_ambImage {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : IsCompact (closure ↑(D.ambImage W))

theorem Hironaka.Manifold.LocalEmbeddingData.image_subset_ambImage {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : ⇑(Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) '' ↑(W i) ⊆ ↑(D.ambImage W)

noncomputable def Hironaka.Manifold.LocalEmbeddingData.ambTheta {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin D.n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin D.n → 𝕜)) (D.ambSpace W).carrier (D.sigmaAmbient.restrict (D.ambImage W)).carrier ⊤

Θ : ⊔ᵢ Gᵢ' ≅ (⊔ᵢ Sp(Gᵢ))|U_Σ, the analytic isomorphism onto the image (diffeomorphOntoImage).

Equations

• D.ambTheta W = Hironaka.Manifold.AnalyticMap.diffeomorphOntoImage (D.ambTheta₀ W) ⋯ ⋯

theorem Hironaka.Manifold.LocalEmbeddingData.ambTheta₀_mem_image_iff {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) (a : (D.ambSpace W).carrier) : (D.ambTheta₀ W) a ∈ ⇑(Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) '' ↑(W i) ↔ a.fst = i

The summand characterisation: Θ₀ a lies over the i-th piece's open iff a is in the i-th summand.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.glueIdeal {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : (D.ambSpace W).IdealSheaf

The data of the factorization at the gluing datum: AmbientTransport.lean at T := D.sigmaTriple, W := U_Σ, Θ := ambTheta — the ideal J₀, …

Equations

• D.glueIdeal W = Hironaka.Manifold.BEDanFamStar.ambIdealOn D.sigmaTriple (D.ambImage W) (D.ambTheta W)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.glueSeq {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (bed : BEDanFamStar 𝕜) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin D.n → 𝕜)) (D.ambSpace W)

… the blow-up sequence, …

Equations

• D.glueSeq W bed hW = bed.ambSeqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯ (D.ambTheta W)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.glueLast {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (bed : BEDanFamStar 𝕜) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : ((D.glueSeq W bed hW).toSuccession.stage (Fin.last (D.glueSeq W bed hW).toSuccession.length)).IdealSheaf

… the last strict transform Y_r, …

Equations

• D.glueLast W bed hW = bed.ambLastOn D.sigmaTriple ⋯ (D.ambImage W) ⋯ (D.ambTheta W)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.glueMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (bed : BEDanFamStar 𝕜) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : (D.glueLast W bed hW).toAnalyticSpace ⟶ (D.glueIdeal W).toAnalyticSpace

… and Π_r|_{Y_r}.

Equations

• D.glueMap W bed hW = bed.ambMapOn D.sigmaTriple ⋯ (D.ambImage W) ⋯ (D.ambTheta W)

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_ofRestrict_pieceDom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(X.ofRestrict (X.openOf ↑(D.pieceDom i (W i))))

The inclusion of the open pieceDom i Wᵢ is an open immersion (the instance, named so that it can be passed explicitly). Internal.

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_ofRestrict_pieceDom_eq {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (X.ofRestrict (X.openOf ↑(D.pieceDom i (W i))))) = Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).pieceOverHom (W i)))

The open immersion of the piece over Wᵢ and the inclusion of the open pieceDom i Wᵢ have the same range (domOpens Wᵢ IS pieceDom i Wᵢ). Internal.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.pieceIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : (X.restrictSet ↑(D.pieceDom i (W i))).toKLocallyRingedSpace ≅ ((D.embedding i).restrictedIdeal (W i)).toAnalyticSpace.toKLocallyRingedSpace

X|pieceDom i (W i) ≅ Sp(Wᵢ)/𝓘ᵢ|Wᵢ: the inclusion of the open pieceDom i Wᵢ against the open immersion of the piece over Wᵢ, onto the same range (isoOfRangeEq).

Equations

• D.pieceIso W i = AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq (X.ofRestrict (X.openOf ↑(D.pieceDom i (W i)))) ((D.embedding i).pieceOverHom (W i)) ⋯

theorem Hironaka.Manifold.LocalEmbeddingData.pieceIso_hom_comp_pieceOverHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : CategoryTheory.CategoryStruct.comp (D.pieceIso W i).hom ((D.embedding i).pieceOverHom (W i)) = X.ofRestrict (X.openOf ↑(D.pieceDom i (W i)))

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sumIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : ((D.embedding i).restrictedIdeal (W i)).toAnalyticSpace.toKLocallyRingedSpace ⟶ D.sigmaTriple.I.toAnalyticSpace.toKLocallyRingedSpace

Sp(Wᵢ)/𝓘ᵢ|Wᵢ → Sp(⊔ⱼ Gⱼ)/𝓘_Σ: the restriction-of-a-quotient map followed by the summand inclusion (sigmaSummandHom).

Equations

• D.sumIn W i = CategoryTheory.CategoryStruct.comp ((D.embedding i).restrictedIdealHom (W i)) (D.sigmaSummandHom i)

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_sumIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.sumIn W i)

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_sumIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.sumIn W i)) = {z : ↑↑D.sigmaTriple.I.toAnalyticSpace.toPresheafedSpace | ↑D.sigmaTriple.I.toAnalyticSpaceι z ∈ ⇑(Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) '' ↑(W i)}

noncomputable def Hironaka.Manifold.LocalEmbeddingData.ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : (D.glueIdeal W).toAnalyticSpace.toKLocallyRingedSpace ⟶ D.sigmaTriple.I.toAnalyticSpace.toKLocallyRingedSpace

Sp(⊔ᵢ Gᵢ')/J₀ → Sp(⊔ⱼ Gⱼ)/𝓘_Σ: the identification ambIdealIso along Θ followed by the open immersion of the restricted closed subspace over U_Σ.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.ambIn W)

theorem Hironaka.Manifold.LocalEmbeddingData.toFun_toAnalyticSpaceι_ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (y : ↑↑(D.glueIdeal W).toAnalyticSpace.toPresheafedSpace) : ↑D.sigmaTriple.I.toAnalyticSpaceι (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.ambIn W) y) = (D.ambTheta₀ W) (↑(D.glueIdeal W).toAnalyticSpaceι y)

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.ambIn W)) = {z : ↑↑D.sigmaTriple.I.toAnalyticSpace.toPresheafedSpace | ↑D.sigmaTriple.I.toAnalyticSpaceι z ∈ D.ambImage W}

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_sumIn_eq {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.sumIn W i)) = Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((D.glueIdeal W).toAnalyticSpace.ofRestrict ((D.glueIdeal W).toAnalyticSpace.openOf ((D.glueIdeal W).overPiece i))) (D.ambIn W)))

The two open immersions into Sp(⊔ⱼ Gⱼ)/𝓘_Σ have the same range: the points over sigmaMk i '' Wᵢ (the summand characterisation). Internal.

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_ofRestrict_comp_ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(CategoryTheory.CategoryStruct.comp ((D.glueIdeal W).toAnalyticSpace.ofRestrict ((D.glueIdeal W).toAnalyticSpace.openOf ((D.glueIdeal W).overPiece i))) (D.ambIn W))

The inclusion of the part over Gᵢ' followed by ambIn is an open immersion. Internal.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.glueEmbIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : (X.restrictSet ↑(D.pieceDom i (W i))).toKLocallyRingedSpace ≅ ((D.glueIdeal W).toAnalyticSpace.restrictSet ((D.glueIdeal W).overPiece i)).toKLocallyRingedSpace

The isomorphism behind emb i: pieceIso followed by the isoOfRangeEq of sumIn and of the part's inclusion followed by ambIn. Internal.

Equations

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

noncomputable def Hironaka.Manifold.LocalEmbeddingData.glueEmb {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : X.restrictSet ↑(D.pieceDom i (W i)) ⟶ (D.glueIdeal W).toAnalyticSpace.restrictSet ((D.glueIdeal W).overPiece i)

**X|Uᵢ ≅ the part of Sp(⊔ᵢ Gᵢ')/J₀ over Gᵢ'** (the field embof the factorization; [Kol07, Proposition 37, proof]),Uᵢ = pieceDom i (W i): through Sp(Wᵢ)/𝓘ᵢ|Wᵢand `Sp(⊔ⱼ Gⱼ)/𝓘_Σ (isoOfRangeEqofsumInand of the part's inclusion followed byambIn`).

Equations

• D.glueEmb W i = (D.glueEmbIso W i).hom

theorem Hironaka.Manifold.LocalEmbeddingData.isIso_glueEmb {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : CategoryTheory.IsIso (D.glueEmb W i)

theorem Hironaka.Manifold.LocalEmbeddingData.glueEmb_comp_ambIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (i : D.ι) : CategoryTheory.CategoryStruct.comp (D.glueEmb W i) (CategoryTheory.CategoryStruct.comp ((D.glueIdeal W).toAnalyticSpace.ofRestrict ((D.glueIdeal W).toAnalyticSpace.openOf ((D.glueIdeal W).overPiece i))) (D.ambIn W)) = CategoryTheory.CategoryStruct.comp (D.pieceIso W i).hom (D.sumIn W i)

emb i lies under sumIn (used by the compatibility map_lift).