The padding identity at the coproduct — the piece clause

The third conjunct of PadIdentityOn (CoproductPadIdentity.lean): Kollár's commutation of the functor with closed embeddings [Kol07, 34.4] at the coproduct slice, summand by summand. The core names the isomorphism ψ := padIdentityIso of the coproduct local resolutions and proves that it carries the members and lies over the ambients. Here, on every piece i, the summand inclusions resIn⁺ i : Ỹ⁺ᵢ → Y⁺ and resIn i : Ỹᵢ → Y (open immersions, AmbientLift.lean) are matched through ψ:

• range_toFun_resIn_padAlong_comp_padIdentityIso: resIn⁺ i ≫ ψ and resIn i have the same range — the summand i of the padded reading opens is carried by ψ to the summand i of the datum's (the point form of ψ over the ambients, range_toFun_resIn, the slice diffeomorphism's summand compatibility, the disjointness of the summands);
• piecePadIdentityIso, piecePadIdentityHom: the induced isomorphism ψᵢ : Ỹ⁺ᵢ ≅ Ỹᵢ of open immersions with equal ranges (isoOfRangeEq), with resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i (resIn_padAlong_comp_padIdentityIso, by construction);
• localResolutionMap_comp_piecePadIdentityHom: ψᵢ lies over the restricted ideals along the zero extension padExtOn, as the morphism padExtOnHom (the morphism form of ψ over the ambients, the two summand squares resIn_comp_localResolutionMapOn, the composite identity homOfPullbackEq_sigmaMk_comp_padRestrictMap of the quotient homs, the cancellation of the open immersion H⁺ᵢ);
• localResolutionToPiece_comp_piecePadIdentityHom: hence ψᵢ lies over the piece (localResolutionToPiece = embInv ∘ restrictedIdealHom ∘ localResolutionMap, embInv_padAlong, padSliceHom_comp_restrictedIdealHom_comp_padExtOnHom: the slice morphism undoes the padding);
• exists_piece_padIdentityIso: the piece clause of PadIdentityOn against the NAMED ψ, and padIdentityOn: the padding identity of every datum (padIdentityOn_of_forall_piece).

The identification is by ranges and the calculus of the quotient homs, never by a uniqueness principle, so no independence hypothesis enters. Not in the sources beyond Kollár's commutation; bookkeeping.

The zero extension on the reading opens

theorem Hironaka.Manifold.LocalEmbeddingData.image_padExt_padPreimageOpens_subset {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : padExt σ (D.embedding i).G '' ↑(D.padPreimageOpens σ Wp i) ⊆ ↑(Wp i)

The zero extension padExt σ Gᵢ maps the datum's reading open padPreimageOpens i = padExt⁻¹(Wp i) into the padded reading open Wp i.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.padExtOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : ((pieceAmbient 𝕜 (D.embedding i).G).restrict (D.padPreimageOpens σ Wp i)).carrier → ((pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).restrict (Wp i)).carrier

The zero extension restricted to the reading opens, padPreimageOpens i → Wp i (across the models Fin n → 𝕜 and Fin n' → 𝕜, so a raw map with its analyticity contMDiff_padExtOn, as padRestrictMap).

Equations

• D.padExtOn σ Wp i x = ⟨Hironaka.Manifold.padExt σ (D.embedding i).G ↑x, ⋯⟩

theorem Hironaka.Manifold.LocalEmbeddingData.inclusion_padExtOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) (x : ((pieceAmbient 𝕜 (D.embedding i).G).restrict (D.padPreimageOpens σ Wp i)).carrier) : ((pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).inclusion (Wp i)) (D.padExtOn σ Wp i x) = padExt σ (D.embedding i).G (((pieceAmbient 𝕜 (D.embedding i).G).inclusion (D.padPreimageOpens σ Wp i)) x)

It lies over the zero extension (definitional).

theorem Hironaka.Manifold.LocalEmbeddingData.contMDiff_padExtOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : ContMDiff (modelWithCornersSelf 𝕜 (Fin D.n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n' → 𝕜)) ⊤ (D.padExtOn σ Wp i)

The restricted zero extension is analytic (ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff, as contMDiff_padRestrictMap).

theorem Hironaka.Manifold.LocalEmbeddingData.restrictedIdeal_eq_pullback_padExtOnMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : (D.embedding i).restrictedIdeal (D.padPreimageOpens σ Wp i) = Manifold.IdealSheaf.pullback (D.padExtOn σ Wp i) ⋯ (((D.padAlongData σ).embedding i).restrictedIdeal (Wp i))

The datum's restricted ideal is the pull-back of the padded datum's along the restricted zero extension (compare [Wlo09, §7.1]; pullback_padExt_padIdeal on the reading opens, pullback_pullback).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.padExtOnHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : ((D.embedding i).restrictedIdeal (D.padPreimageOpens σ Wp i)).toAnalyticSpace ⟶ (((D.padAlongData σ).embedding i).restrictedIdeal (Wp i)).toAnalyticSpace

The morphism of the restricted closed subspaces over the restricted zero extension, Sp(I|padPreimageOpens i) → Sp(I⁺|Wp i) (homOfPullbackEq).

Equations

• D.padExtOnHom σ Wp i = Manifold.IdealSheaf.homOfPullbackEq (D.padExtOn σ Wp i) ⋯ ⋯

The summand identification

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_resIn_padAlong_comp_padIdentityIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) (D.padIdentityIso σ Wp hWp bed hbed))) = Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resIn bed (D.padPreimageOpens σ Wp) ⋯ hbed i))

resIn⁺ i ≫ ψ and resIn i have the same range ([Kol07, 34.4] summand by summand) — the padded summand i is carried by ψ onto the datum's summand i (the point form localResolutionMapOn_inv_padIdentityIso_apply, range_toFun_resIn for both data, inclusionMap_sigmaPadSliceDiffeomorph, coe_sigmaCoordImage, Sigma.mk.inj_iff).

theorem Hironaka.Manifold.LocalEmbeddingData.isOpenImmersion_resIn_padAlong_comp_padIdentityIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) (D.padIdentityIso σ Wp hWp bed hbed))

resIn⁺ i ≫ ψ is an open immersion — the composite of the open immersion resIn⁺ i (isOpenImmersion_resIn) with the isomorphism ψ (padIdentityIso_isIso; LocallyRingedSpace.IsOpenImmersion.of_isIso, .comp).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.piecePadIdentityIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : (((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯).toKLocallyRingedSpace ≅ ((D.embedding i).localResolution bed (D.padPreimageOpens σ Wp i) ⋯).toKLocallyRingedSpace

The isomorphism ψᵢ : Ỹ⁺ᵢ ≅ Ỹᵢ of the two open immersions into Y with the same range (isoOfRangeEq).

Equations

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

noncomputable def Hironaka.Manifold.LocalEmbeddingData.piecePadIdentityHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : ((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯ ⟶ (D.embedding i).localResolution bed (D.padPreimageOpens σ Wp i) ⋯

The piece isomorphism as a morphism of analytic spaces.

Equations

• D.piecePadIdentityHom σ Wp hWp bed hbed i = (D.piecePadIdentityIso σ Wp hWp bed hbed i).hom

theorem Hironaka.Manifold.LocalEmbeddingData.piecePadIdentityHom_isIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : CategoryTheory.IsIso (D.piecePadIdentityHom σ Wp hWp bed hbed i)

ψᵢ is an isomorphism (the hom of an Iso).

theorem Hironaka.Manifold.LocalEmbeddingData.resIn_padAlong_comp_padIdentityIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) (D.padIdentityIso σ Wp hWp bed hbed) = CategoryTheory.CategoryStruct.comp (D.piecePadIdentityHom σ Wp hWp bed hbed i) (D.resIn bed (D.padPreimageOpens σ Wp) ⋯ hbed i)

resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i (isoOfRangeEq_hom_comp).

Over the restricted ideals, then over the piece

theorem Hironaka.Manifold.LocalEmbeddingData.homOfPullbackEq_sigmaMk_comp_padRestrictMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).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) (D.padPreimageOpens σ Wp i) (D.ambImage (D.padPreimageOpens σ Wp)) ⋯) ⋯ ⋯) (Manifold.IdealSheaf.homOfPullbackEq (D.padRestrictMap σ Wp) ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (D.padExtOnHom σ Wp i) (Manifold.IdealSheaf.homOfPullbackEq ⇑(AnalyticMap.restrictMap (Manifold.sigmaMk (fun (i : (D.padAlongData σ).ι) => pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G) i) (Wp i) ((D.padAlongData σ).ambImage Wp) ⋯) ⋯ ⋯)

The two quotient homs into the padded coproduct's closed subspace agree — along padRestrictMap ∘ sigmaMk i = sigmaMk⁺ i ∘ padExt on the reading opens (homOfPullbackEq_comp_fun twice and homOfPullbackEq_congr_fun, with inclusionMap_sigmaPadSliceDiffeomorph).

theorem Hironaka.Manifold.LocalEmbeddingData.localResolutionMap_comp_piecePadIdentityHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (D.piecePadIdentityHom σ Wp hWp bed hbed i) ((D.embedding i).localResolutionMap bed (D.padPreimageOpens σ Wp i) ⋯)) (D.padExtOnHom σ Wp i) = ((D.padAlongData σ).embedding i).localResolutionMap bed (Wp i) ⋯

ψᵢ lies over the restricted ideals along the zero extension — padExtOnHom ∘ Πᵢ ∘ ψᵢ = Π⁺ᵢ (the two summand squares resIn_comp_localResolutionMapOn, the morphism form localResolutionMapOn_comp_inv_padIdentityIso, homOfPullbackEq_sigmaMk_comp_padRestrictMap, and the cancellation of the open immersion homOfPullbackEq along sigmaMk⁺ i — isOpenImmersion_homOfPullbackEq_of_injective).

theorem Hironaka.Manifold.LocalEmbeddingData.padSliceHom_comp_restrictedIdealHom_comp_padExtOnHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (D.padExtOnHom σ Wp i) (((D.padAlongData σ).embedding i).restrictedIdealHom (Wp i))) (padSliceHom σ (D.embedding i).ideal) = (D.embedding i).restrictedIdealHom (D.padPreimageOpens σ Wp i)

The slice morphism undoes the padding on the restricted closed subspaces — padSliceHom ∘ restrictedIdealHom⁺ ∘ padExtOnHom = restrictedIdealHom (padCoordProj ∘ padExt = id; quotient homs along a composite of functions, Hom.ext_of_comp_quotientι).

theorem Hironaka.Manifold.LocalEmbeddingData.localResolutionToPiece_comp_piecePadIdentityHom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : CategoryTheory.CategoryStruct.comp (D.piecePadIdentityHom σ Wp hWp bed hbed i) ((D.embedding i).localResolutionToPiece bed (D.padPreimageOpens σ Wp i) ⋯) = ((D.padAlongData σ).embedding i).localResolutionToPiece bed (Wp i) ⋯

ψᵢ lies over the piece — Πᵢ ∘ ψᵢ = Π⁺ᵢ for the maps to the piece X|V (localResolutionToPiece = embInv ∘ restrictedIdealHom ∘ localResolutionMap, embInv_padAlong, the two identities above).

The clause and the padding identity

theorem Hironaka.Manifold.LocalEmbeddingData.exists_piece_padIdentityIso {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : ∃ (ψᵢ : ((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯ ⟶ (D.embedding i).localResolution bed (D.padPreimageOpens σ Wp i) ⋯), CategoryTheory.IsIso ψᵢ ∧ CategoryTheory.CategoryStruct.comp ψᵢ ((D.embedding i).localResolutionToPiece bed (D.padPreimageOpens σ Wp i) ⋯) = ((D.padAlongData σ).embedding i).localResolutionToPiece bed (Wp i) ⋯ ∧ CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) (D.padIdentityIso σ Wp hWp bed hbed) = CategoryTheory.CategoryStruct.comp ψᵢ (D.resIn bed (D.padPreimageOpens σ Wp) ⋯ hbed i)

The piece clause of PadIdentityOn against the NAMED ψ = padIdentityIso — the hypothesis hc of padIdentityOn_of_forall_piece: on every piece an isomorphism ψᵢ of the piece's local resolutions over the piece with resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i.

theorem Hironaka.Manifold.LocalEmbeddingData.padIdentityOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : D.PadIdentityOn σ Wp hWp bed hbed

The padding identity holds for every datum ([Kol07, 34.4] at the coproduct slice) — padIdentityOn_of_forall_piece at the piece clause.