The lift of the glued space into the last transform and the ambient blow-up factorization #
Kollár's resolution of the disjoint union Y₀ = ⊔ᵢ X|Uᵢ ⊆ ⊔ᵢ Uᵢ has, over each piece, the
resolution of the piece [Kol07, Proposition 37, proof]. At a gluing datum Γ of the local
resolutions and a relatively compact family W ≤ Γ.W of opens of the pieces' ambients: the
restriction Ỹ(W') → Ỹ(W) of a piece's local resolution to a smaller open
(LocalResolutionRestrictHom.lean), the part of the glued space over pieceDom i Wᵢ identified
with Ỹ(Wᵢ) (the gluing's partIso), sent into the functor's resolution of the disjoint-union
triple over U_Σ (localResolutionHomOn at the summand inclusion, resIn) and then into the
transported last transform Sp(Y_r) (AmbientEmb.lean) — the lift glueLift i, an isomorphism
onto the part of Sp(Y_r) over the i-th part of Y₀, compatible with Π_r|_{Y_r} and emb i
(glueMap_restrictSet_comp_glueLift); finally the ambient blow-up factorization
ambientBlowUpFactorizationOfGluing for any open covered by the pieces pieceDom i Wᵢ, and
clause (4) of exists_functorial_resolution at U for the glued space's map, with the independence
of the local resolution as the hypothesis hind. Not in the sources beyond Kollár's proof;
bookkeeping.
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpen_preimage_pieceDom
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(i : D.ι)
:
The part of the glued space over pieceDom i Wᵢ is open. Internal.
theorem
Hironaka.Manifold.LocalEmbeddingData.coe_openOf_preimage_pieceDom
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(i : D.ι)
:
The two spellings of the part of the glued space over pieceDom i Wᵢ — restrictSet and the
glue's Opens.comap — are the same open. Internal.
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.partIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(i : D.ι)
:
(Γ.glue.gluedOver.restrictSet
(AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i)))).toKLocallyRingedSpace ⟶ ((D.embedding i).localResolution bed (Γ.W i) ⋯).toKLocallyRingedSpace
The part of the glued space over pieceDom i Wᵢ into the i-th piece
([Wlo09, §4, (3)⇒(4)]: the gluing of the Ṽᵢ) — the gluing's partIso at
P := pieceDom i Wᵢ ≤ dom i, then the inclusion of the part of the piece.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_partIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(i : D.ι)
:
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.partIn bed Γ W hle i)
theorem
Hironaka.Manifold.LocalEmbeddingData.range_toFun_partIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(i : D.ι)
:
Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.partIn bed Γ W hle i)) = {y : ↑↑(bed.lastIdealOn (D.embedding i).ambientTriple ⋯ (Γ.W i) ⋯).toAnalyticSpace.toPresheafedSpace | ↑(((bed.seqOn (D.embedding i).ambientTriple ⋯ (Γ.W i) ⋯).toSuccession.stageMap
(Fin.last (bed.seqOn (D.embedding i).ambientTriple ⋯ (Γ.W i) ⋯).toSuccession.length))
(↑(bed.lastIdealOn (D.embedding i).ambientTriple ⋯ (Γ.W i) ⋯).toAnalyticSpaceι y)) ∈ W i}
Its range: the part of the piece over Wᵢ (in the spelling of LocalResolutionOn.lean).
theorem
Hironaka.Manifold.LocalEmbeddingData.partIn_comp_pieceToSpace
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.partIn bed Γ W hle i) (D.pieceToSpace bed i (Γ.W i) ⋯) = CategoryTheory.CategoryStruct.comp
(Γ.glue.gluedOver.ofRestrict
(Γ.glue.gluedOver.openOf (AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i)))))
Γ.glue.descMap
It lies over des (partIso_inv_comp_over).
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.resIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
((D.embedding i).localResolution bed (W i) ⋯).toKLocallyRingedSpace ⟶ (bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toKLocallyRingedSpace
The local resolution over Wᵢ into the functor's on T_Σ|U_Σ (the lift of
[Kol07, Definition 30.1]): localResolutionHomOn at g := sigmaMk i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_resIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.resIn bed W hW hbed i)
theorem
Hironaka.Manifold.LocalEmbeddingData.range_toFun_resIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resIn bed W hW hbed i)) = {y : ↑↑(bed.lastIdealOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toAnalyticSpace.toPresheafedSpace | ↑(((bed.seqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toSuccession.stageMap
(Fin.last (bed.seqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toSuccession.length))
(↑(bed.lastIdealOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toAnalyticSpaceι y)) ∈ ⇑(Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) '' ↑(W i)}
theorem
Hironaka.Manifold.LocalEmbeddingData.resIn_comp_localResolutionMapOn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.resIn bed W hW hbed i)
(bed.localResolutionMapOn D.sigmaTriple ⋯ (D.ambImage W) ⋯) = CategoryTheory.CategoryStruct.comp ((D.embedding i).localResolutionMap bed (W i) ⋯)
(Manifold.IdealSheaf.homOfPullbackEq
⇑(AnalyticMap.restrictMap (Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) (W i)
(D.ambImage W) ⋯)
⋯ ⋯)
It lies over the summand inclusion of the restricted closed subspaces
(localResolutionHomOn_comp_map).
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.resIso
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
(Γ.glue.gluedOver.restrictSet
(AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i)))).toKLocallyRingedSpace ≅ ((D.embedding i).localResolution bed (W i) ⋯).toKLocallyRingedSpace
The part of the glued space over pieceDom i Wᵢ IS the local resolution over Wᵢ
(isoOfRangeEq of partIn and of the restriction Ỹ(Wᵢ) → Ỹ(Γ.Wᵢ)).
Equations
- D.resIso bed Γ W hW hle hbed i = AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq (D.partIn bed Γ W hle i) ((D.embedding i).localResolutionRestrictHom bed (Γ.W i) ⋯ (W i) ⋯ ⋯ hbed) ⋯
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.resIso_hom_comp_localResolutionRestrictHom
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.resIso bed Γ W hW hle hbed i).hom
((D.embedding i).localResolutionRestrictHom bed (Γ.W i) ⋯ (W i) ⋯ ⋯ hbed) = D.partIn bed Γ W hle i
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.ambLastIsoK
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
:
(D.glueLast W bed hW).toAnalyticSpace.toKLocallyRingedSpace ≅ (bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toKLocallyRingedSpace
The identification Sp(Y_r) ≅ Ỹ_Σ(U_Σ) of AmbientEmb.lean as an isomorphism of K-spaces.
Internal.
Equations
- D.ambLastIsoK bed W hW = CategoryTheory.asIso (bed.ambLastIso D.sigmaTriple ⋯ (D.ambImage W) ⋯ (D.ambTheta W))
Instances For
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.liftIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
(Γ.glue.gluedOver.restrictSet
(AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i)))).toKLocallyRingedSpace ⟶ (D.glueLast W bed hW).toAnalyticSpace.toKLocallyRingedSpace
Y|des⁻¹(pieceDom i Wᵢ) → Sp(Y_r): resIso, resIn, then the identification
ambLastIso⁻¹ (AmbientEmb.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_liftIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.liftIn bed Γ W hW hle hbed i)
theorem
Hironaka.Manifold.LocalEmbeddingData.stageMap_ambLastIso_eq
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(p : ↑↑(D.glueLast W bed hW).toAnalyticSpace.toPresheafedSpace)
:
↑(((bed.seqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toSuccession.stageMap
(Fin.last (bed.seqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toSuccession.length))
(↑(bed.lastIdealOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).toAnalyticSpaceι
(↑(bed.ambLastIso D.sigmaTriple ⋯ (D.ambImage W) ⋯ (D.ambTheta W)) p))) = (D.ambTheta₀ W) (↑(D.glueIdeal W).toAnalyticSpaceι (↑(D.glueMap W bed hW) p))
The ambient image of the last stage of a point of Sp(Y_r), read through ambLastIso, is Θ₀
of the ambient image of its Π_r-image (the point form of the transport square of
AmbientEmb.lean). Internal.
theorem
Hironaka.Manifold.LocalEmbeddingData.range_toFun_liftIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.liftIn bed Γ W hW hle hbed i)) = {p : ↑↑(D.glueLast W bed hW).toAnalyticSpace.toPresheafedSpace | ↑(D.glueMap W bed hW) p ∈ (D.glueIdeal W).overPiece i}
Its range: the points of Y_r over the i-th piece's part of Y₀.
theorem
Hironaka.Manifold.LocalEmbeddingData.homOfPullbackEq_restrictMap_comp_restrictOpensHom
{𝕜 : 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
(Manifold.IdealSheaf.homOfPullbackEq
⇑(AnalyticMap.restrictMap (Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) (W i)
(D.ambImage W) ⋯)
⋯ ⋯)
(Manifold.IdealSheaf.restrictOpensHom D.sigmaTriple.I (D.ambImage W)) = D.sumIn W i
The two maps Sp(Wᵢ)/𝓘ᵢ|Wᵢ → Sp(⊔ⱼ Gⱼ)/𝓘_Σ agree: homOfPullbackEq along the restricted
summand inclusion followed by the restriction open immersion over U_Σ, and the
restriction-of-a-quotient map followed by the summand inclusion (both lie over
Sp(Wᵢ ↪ ⊔ⱼ Gⱼ)). Internal.
theorem
Hironaka.Manifold.LocalEmbeddingData.resIso_hom_comp_localResolutionMap
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.resIso bed Γ W hW hle hbed i).hom
((D.embedding i).localResolutionMap bed (W i) ⋯) = CategoryTheory.CategoryStruct.comp (AnalyticSpace.Hom.restrictSet Γ.glue.descMap ↑(D.pieceDom i (W i)))
(D.pieceIso W i).hom
resIso followed by the local resolution map over Wᵢ is des restricted over
pieceDom i Wᵢ followed by pieceIso (both lie over X: the open immersion of the piece over
Wᵢ is a monomorphism). Internal.
theorem
Hironaka.Manifold.LocalEmbeddingData.liftIn_comp_glueMap_ambIn
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.liftIn bed Γ W hW hle hbed i)
(CategoryTheory.CategoryStruct.comp (D.glueMap W bed hW) (D.ambIn W)) = CategoryTheory.CategoryStruct.comp (D.resIso bed Γ W hW hle hbed i).hom
(CategoryTheory.CategoryStruct.comp ((D.embedding i).localResolutionMap bed (W i) ⋯) (D.sumIn W i))
The compatibility with map and emb under ambIn (glueMap_restrictSet_comp_glueLift before
the restriction to the parts).
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpen_preimage_overPiece
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(i : D.ι)
:
The part Π_r⁻¹(overPiece i) of Sp(Y_r) is open. Internal.
theorem
Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_ofRestrict_preimage_overPiece
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(i : D.ι)
:
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion
↑((D.glueLast W bed hW).toAnalyticSpace.ofRestrict
((D.glueLast W bed hW).toAnalyticSpace.openOf (↑(D.glueMap W bed hW) ⁻¹' (D.glueIdeal W).overPiece i)))
The inclusion of the part Π_r⁻¹(overPiece i) is an open immersion (the KSpace instance,
named so that it can be passed explicitly). Internal.
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.glueLiftIso
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
(Γ.glue.gluedOver.restrictSet
(AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i)))).toKLocallyRingedSpace ≅ ((D.glueLast W bed hW).toAnalyticSpace.restrictSet
(↑(D.glueMap W bed hW) ⁻¹' (D.glueIdeal W).overPiece i)).toKLocallyRingedSpace
The isomorphism behind glueLift i: liftIn against the inclusion of the part
Π_r⁻¹(overPiece i) (isoOfRangeEq). Internal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.glueLift
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
Γ.glue.gluedOver.restrictSet (AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' ↑(D.pieceDom i (W i))) ⟶ (D.glueLast W bed hW).toAnalyticSpace.restrictSet (↑(D.glueMap W bed hW) ⁻¹' (D.glueIdeal W).overPiece i)
Y|des⁻¹(pieceDom i Wᵢ) ≅ Sp(Y_r)|_{Π_r⁻¹(overPiece i)} — the lift of the glued space into
the last transform ([Kol07, Proposition 37, proof]).
Equations
- D.glueLift bed Γ W hW hle hbed i = (D.glueLiftIso bed Γ W hW hle hbed i).hom
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.isIso_glueLift
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.IsIso (D.glueLift bed Γ W hW hle hbed i)
theorem
Hironaka.Manifold.LocalEmbeddingData.glueMap_restrictSet_comp_glueLift
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(i : D.ι)
:
CategoryTheory.CategoryStruct.comp (D.glueLift bed Γ W hW hle hbed i)
(AnalyticSpace.Hom.restrictSet (D.glueMap W bed hW) ((D.glueIdeal W).overPiece i)) = CategoryTheory.CategoryStruct.comp (AnalyticSpace.Hom.restrictSet Γ.glue.descMap ↑(D.pieceDom i (W i)))
(D.glueEmb W i)
Π_r|_{Y_r} restricted over the i-th part, after glueLift i, is emb i after des
restricted over pieceDom i Wᵢ.
noncomputable def
Hironaka.Manifold.LocalEmbeddingData.ambientBlowUpFactorizationOfGluing
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(Γ : D.ResolutionGluing bed)
(W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier)
(hW : ∀ (i : D.ι), IsCompact (closure ↑(W i)))
(hle : ∀ (i : D.ι), W i ≤ Γ.W i)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(V : Set ↑↑X.toPresheafedSpace)
(hcov : V ⊆ ⋃ (i : D.ι), ↑(D.pieceDom i (W i)))
:
The ambient blow-up factorization of the glued space's map over any open V covered by the
pieces pieceDom i Wᵢ, W ≤ Γ.W relatively compact ([Kol07, Proposition 37, proof];
[Kol07, Theorem 45(4)]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hironaka.Manifold.LocalEmbeddingData.nonempty_ambientBlowUpFactorization_resolutionOnFullMap_of_independent
{𝕜 : Type}
[RCLike 𝕜]
{X : AnalyticSpace 𝕜}
{U : Set ↑↑X.toPresheafedSpace}
(D : LocalEmbeddingData 𝕜 X U)
(bed : BEDanFamStar 𝕜)
(hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed)
(hind : LocalResolutionIndependentOn X bed)
:
Clause (4) of exists_functorial_resolution at U for the glued space's map to X
([Kol07, Theorem 45(4)]), with the independence of the local resolution as hind: the
factorization at the gluing datum Classical.choice picks, W := Γ.W, V := U, transported along
resolutionOnFullPair_eq_of_glues.