The padding identity of a datum at the coproduct

The padding comparison at the level of a whole datum: Kollár's commutation of the functor with closed embeddings, j^* B(X, I_X, E) = B(Y, I_Y, E|_Y) [Kol07, 34.4], read at the coproduct slice (compare [Wlo09, §7.1]). A local embedding datum D padded along a coordinate embedding σ : Fin n ↪ Fin n′ (padAlongData: every piece embedding padded by PieceEmbedding.padAlong σ) has the coproduct local resolution, labels and members of D — read over the padded reading opens Wp and the reading opens they carry along the slice (padPreimageOpens):

• the statement: padAlongData, padPreimageOpens, isCompact_closure_padPreimageOpens, PadIdentityOn — an order isomorphism o of the label sets, an isomorphism ψ of the coproduct local resolutions with comap ψ (members (o σp)) = members⁺ σp for every label, and on every piece an isomorphism over the piece;
• the cast leg with an order isomorphism: BlowUpSequence.exists_diffeomorph_last_of_pullback_bijective_iso (list level) and BEDanFamStar.exists_diffeomorph_last_of_cast_iso (functor level), with an order ISOMORPHISM of the label sets: a diffeomorphism pulls back no empty centre, so the erasure of empty blow-ups is the identity (eraseEmpty_pullback_of_surjective) and the last-stage map is pullbackLiftLastDiffeomorphOfBijective;
• the coproduct slice S* := ⋃ᵢ sigmaMk⁺ i '' padSlice σ Gᵢ (sigmaPadSlice, isClosedSubmanifold_sigmaPadSlice); sigmaPadSliceDiffeomorph: the datum's coproduct ambient IS the slice, across the models Fin n and Fin (n′ − (n′ − n)) (the sigma of the per-piece padExtDiffeomorph followed by sigmaSubmanifoldDiffeomorph of Hironaka/Resolution/Analytic/Kol07Thm45/SigmaSubmanifold.lean), with inclusionMap_sigmaPadSliceDiffeomorph; pullback_inclusionMap_sigmaPadSlice: the padded ideal restricted to the slice is the datum's ideal transported (IdealSheaf.ext_of_comap_sigmaMk, pullback_inclusionMap_padIdeal per piece), and idealSheaf_sigmaPadSlice_le; preimage_sigmaPadSliceDiffeomorph_preimageOpens_ambImage: the datum's reading open is the trace of the padded one on the slice; the restricted slice map padRestrictMap : N|U → N⁺|U⁺ (incl_{S*} ∘ Φ on the reading opens), analytic (contMDiff_padRestrictMap), with I|U = m^*(I⁺|U⁺) (restrictOpens_eq_pullback_padRestrictMap);
• THE CORE exists_padIdentityCore: bed.closedEmbedding at (S*, I⁺, J*) makes the padded run the push-forward of the slice run ([Kol07, 34.4]; [Wlo09, Theorem 2.0.2(4)]), exists_closedSubmanifold_last_pushforwardRestrict_boundary (LocalResolutionPad.lean) gives the carried slice S*_r, G₁, the ideal identity, the composite square and the order isomorphism o₁ with the trace identity; the cast leg at (Φ, I, J*) gives G₀ and ε₀; then o := o₁.symm.trans ε₀.symm, ψ := inv (homOfPullbackEq (incl_{S*_r} ∘ (G₁ ∘ G₀))) (the two isomorphisms of exists_isIso_localResolution_padAlong), the member identity in EQUALITY form for every label from the ideal-level trace identity (pullback_idealSheaf_inclusionMap_comp_of_hasSncWithProper, the cast helper at G₀) through the generic member transport, and ψ over the ambients in MORPHISM form — localResolutionMapOn⁺ ∘ ψ⁻¹ = homOfPullbackEq (padRestrictMap) ∘ localResolutionMapOn (the generic quotient square);
• the data exposed as definitions by choice from the core — padIdentityOrderIso (o), padIdentityIso (ψ) — with padIdentityIso_isIso, comap_padIdentityIso_sigmaMembers, localResolutionMapOn_comp_inv_padIdentityIso and its point form localResolutionMapOn_inv_padIdentityIso_apply, and the ASSEMBLY padIdentityOn_of_forall_piece: the padding identity from the core and the piece clause stated against the NAMED ψ (CoproductPadIdentityPiece.lean proves that clause).

Nothing here is new mathematics: the argument is the padding leg of the comparison of two embeddings (LocalResolutionPad.lean) at the coproduct slice, with an order isomorphism where the piece case had an embedding. The generic homOfPullbackEq tools live in HomOfPullbackEqCalculus.lean.

The cast leg with an order ISOMORPHISM (a diffeomorphism erases no centre)

theorem AnalyticManifold.BlowUpSequence.exists_diffeomorph_last_of_pullback_bijective_iso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N N' : AnalyticManifold 𝕜 E} (g : N'.carrier → N.carrier) {U : TopologicalSpace.Opens N.carrier} {U' : TopologicalSpace.Opens N'.carrier} (L : BlowUpSequence ψ₀ (N.restrict U)) (h : AnalyticMap (N'.restrict U') (N.restrict U)) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hb : Function.Bijective ⇑h) (hsq : ∀ (p : (N'.restrict U').carrier), (N.inclusion U) (h p) = g ((N'.inclusion U') p)) (J : (N.restrict U).IdealSheaf) (J' : (N'.restrict U').IdealSheaf) (hJ' : J' = Manifold.IdealSheaf.pullback ⇑h ⋯ J) : ∃ (G : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier (L.stage (Fin.last L.length)).carrier ⊤), (∀ (p : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier), (N.inclusion U) (L.toSuccession.composite (G p)) = g ((N'.inclusion U') ((L.pullback h hh).toSuccession.composite p))) ∧ (L.pullback h hh).toSuccession.strictTransformSubspaceSeq J' (Fin.last (L.pullback h hh).toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length)) ∧ ∃ (ε : ((L.pullback h hh).toSuccession.totalTransformSeq (Fin.last (L.pullback h hh).toSuccession.length)).ι ≃o (L.toSuccession.totalTransformSeq (Fin.last L.toSuccession.length)).ι), ∀ (i : ((L.pullback h hh).toSuccession.totalTransformSeq (Fin.last (L.pullback h hh).toSuccession.length)).ι), ⇑G ⁻¹' (L.toSuccession.totalTransformSeq (Fin.last L.toSuccession.length)).hyp (ε i) = ((L.pullback h hh).toSuccession.totalTransformSeq (Fin.last (L.pullback h hh).toSuccession.length)).hyp i

The list-level cast leg, for the plain pull-back along a BIJECTIVE local isomorphism: the last-stage diffeomorphism is pullbackLiftLastDiffeomorphOfBijective, the strict transforms correspond (strictTransformSubspaceSeq_last_pullbackLiftLast), and the last boundary families correspond through an order ISOMORPHISM (totalTransformSeqFrom_last_pullbackLiftLast at the empty family, exists_orderIso_of_eq).

theorem Hironaka.Manifold.BEDanFamStar.exists_diffeomorph_last_of_cast_iso {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (hcomm : ∀ (m : ℕ), AnalyticFamilyFunctor.CommutesWithLocalIsos (bed.fam m)) {k n : ℕ} (hk : k = n) {N : AnalyticManifold 𝕜 (Fin k → 𝕜)} {N' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) N'.carrier N.carrier ⊤) (I : N.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (I' : N'.IdealSheaf) (hI' : Manifold.IdealSheaf.IsNonzeroEverywhere I') (hII' : I' = Manifold.IdealSheaf.pullback ⇑g ⋯ I) (hT : DomBEDan 𝕜 { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ }) (hT' : DomBEDan 𝕜 { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ }) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) (U' : TopologicalSpace.Opens N'.carrier) (hU' : IsCompact (closure ↑U')) (hUU' : ↑U' = ⇑g ⁻¹' ↑U) : ∃ (G : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').length)).carrier ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).stage (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).length)).carrier ⊤), (∀ (p : ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').length)).carrier), (N.inclusion U) ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.composite (G p)) = g ((N'.inclusion U') ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.composite p))) ∧ (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.strictTransformSubspaceSeq (I'.restrict U') (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G ⋯ ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (I.restrict U) (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.length)) ∧ ∃ (ε : ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.totalTransformSeq (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.length)).ι ≃o ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.length)).ι), ∀ (i : ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.totalTransformSeq (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.length)).ι), ⇑G ⁻¹' ((((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bed.fam k).fam { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty N.carrier, isSnc := ⋯ } hT).seqOn U hU).toSuccession.length)).hyp (ε i) = ((((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.totalTransformSeq (Fin.last (((bed.fam n).fam { I := I', isNonzeroEverywhere := hI', F := Manifold.HypersurfaceFamily.empty N'.carrier, isSnc := ⋯ } hT').seqOn U' hU').toSuccession.length)).hyp i

The functor-level cast leg, with an order ISOMORPHISM of the label sets: along a DIFFEOMORPHISM g (a surjective local isomorphism) the pulled-back list has no empty centre (noEmptyCenters_pullback_of_surjective), so the erasure of empty blow-ups in the functor's value is the identity (eraseEmpty_pullback_of_surjective) and the list-level leg applies.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.padAlongData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : LocalEmbeddingData 𝕜 X U

The datum padded along a coordinate embedding — every piece embedding padded by PieceEmbedding.padAlong σ; padLeftData/padRightData (CoproductSumData.lean) are its instances by rfl.

Equations

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

noncomputable def Hironaka.Manifold.LocalEmbeddingData.padPreimageOpens {𝕜 : 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.ι) : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier

The reading opens of the datum carried by the padded reading opens along the slice (preimageOpens (padExt σ G)).

Equations

• D.padPreimageOpens σ Wp i = Manifold.preimageOpens (Hironaka.Manifold.padExt σ (D.embedding i).G) ⋯ (Wp i)

theorem Hironaka.Manifold.LocalEmbeddingData.isCompact_closure_padPreimageOpens {𝕜 : 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))) (i : D.ι) : IsCompact (closure ↑(D.padPreimageOpens σ Wp i))

The reading opens read back through the padding slice are relatively compact (isCompact_closure_preimage_padExt).

def 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) : Prop

The padding identity of a datum at the coproduct ([Kol07, 34.4] at the coproduct slice): an order isomorphism of the padded datum's label set onto the datum's (the padded run is the run of the coproduct slice, stage by stage), an isomorphism of the coproduct local resolutions carrying the datum's member of label o σp to the padded datum's member of label σp, restricting on every piece to an isomorphism of the piece's local resolutions over the piece.

Equations

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

The coproduct slice of the padding and its identification with the datum's ambient

def Hironaka.Manifold.LocalEmbeddingData.sigmaPadSlice {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : Set (D.padAlongData σ).sigmaAmbient.carrier

The coproduct slice S* = ⋃ᵢ sigmaMk⁺ i '' padSlice σ Gᵢ inside the padded coproduct ambient.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.isClosedSubmanifold_sigmaPadSlice {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n' → 𝕜)) (D.sigmaPadSlice σ) (n' - D.n)

It is a closed submanifold of codimension n′ − n (isClosedSubmanifold_sigmaUnion at the pad slices, isClosedSubmanifold_padSlice).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sigmaPadSliceDiffeomorph {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : Diffeomorph (modelWithCornersSelf 𝕜 (Fin D.n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n' - (n' - D.n)) → 𝕜)) D.sigmaAmbient.carrier ⋯.toAnalyticManifold.carrier ⊤

The datum's coproduct ambient IS the coproduct slice — across models (Fin n against Fin (n′ − (n′ − n))): the sigma of the per-piece padExtDiffeomorph followed by sigmaSubmanifoldDiffeomorph.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.inclusionMap_sigmaPadSliceDiffeomorph {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (i : D.ι) (x : (pieceAmbient 𝕜 (D.embedding i).G).carrier) : ⋯.inclusionMap ((D.sigmaPadSliceDiffeomorph σ) ((Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) x)) = (Manifold.sigmaMk (fun (i : (D.padAlongData σ).ι) => pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G) i) (padExt σ (D.embedding i).G x)

On points: incl_{S*} (Φ (sigmaMk i x)) = sigmaMk⁺ i (padExt σ Gᵢ x).

theorem Hironaka.Manifold.LocalEmbeddingData.pullback_inclusionMap_sigmaPadSlice {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ (D.padAlongData σ).sigmaTriple.I = Manifold.IdealSheaf.pullback ⇑(D.sigmaPadSliceDiffeomorph σ).symm ⋯ D.sigmaTriple.I

The slice ideal is the datum's ideal transported: the padded coproduct ideal restricted to the coproduct slice is D.sigmaTriple.I pulled back along Φ⁻¹ (IdealSheaf.ext_of_comap_sigmaMk, pullback_inclusionMap_padIdeal per piece).

theorem Hironaka.Manifold.LocalEmbeddingData.idealSheaf_sigmaPadSlice_le {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') : ⋯.idealSheaf ≤ (D.padAlongData σ).sigmaTriple.I

The slice lies in the zero set of the padded coproduct ideal (the hypothesis hSI of the push-forward; idealSheaf_padSlice_le_padIdeal per piece).

theorem Hironaka.Manifold.LocalEmbeddingData.preimage_sigmaPadSliceDiffeomorph_preimageOpens_ambImage {𝕜 : 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) : ↑(D.ambImage (D.padPreimageOpens σ Wp)) = ⇑(D.sigmaPadSliceDiffeomorph σ) ⁻¹' ↑(⋯.preimageOpens ((D.padAlongData σ).ambImage Wp))

The datum's reading open is the trace of the padded one on the slice: Φ⁻¹(S* ∩ U⁺) = U for U⁺ = ambImage Wp, U = ambImage (padPreimageOpens σ Wp) (inclusionMap_sigmaPadSliceDiffeomorph, coe_sigmaCoordImage, preimage_sigmaMk_iUnion_image).

The restricted slice map U → U⁺

noncomputable def Hironaka.Manifold.LocalEmbeddingData.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) : (D.sigmaAmbient.restrict (D.ambImage (D.padPreimageOpens σ Wp))).carrier → ((D.padAlongData σ).sigmaAmbient.restrict ((D.padAlongData σ).ambImage Wp)).carrier

The restricted slice map m : N|U → N⁺|U⁺, incl_{S*} ∘ Φ on the reading opens (lands in U⁺ by preimage_sigmaPadSliceDiffeomorph_preimageOpens_ambImage).

Equations

• D.padRestrictMap σ Wp p = ⟨⋯.inclusionMap ((D.sigmaPadSliceDiffeomorph σ) ↑p), ⋯⟩

theorem Hironaka.Manifold.LocalEmbeddingData.inclusion_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) (p : (D.sigmaAmbient.restrict (D.ambImage (D.padPreimageOpens σ Wp))).carrier) : ((D.padAlongData σ).sigmaAmbient.inclusion ((D.padAlongData σ).ambImage Wp)) (D.padRestrictMap σ Wp p) = ⋯.inclusionMap ((D.sigmaPadSliceDiffeomorph σ) ((D.sigmaAmbient.inclusion (D.ambImage (D.padPreimageOpens σ Wp))) p))

It lies over incl_{S*} ∘ Φ (definitional).

theorem Hironaka.Manifold.LocalEmbeddingData.contMDiff_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) : ContMDiff (modelWithCornersSelf 𝕜 (Fin D.n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n' → 𝕜)) ⊤ (D.padRestrictMap σ Wp)

It is analytic (ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff, as AnalyticMap.restrictMap).

theorem Hironaka.Manifold.LocalEmbeddingData.restrictOpens_eq_pullback_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) : D.sigmaTriple.I.restrict (D.ambImage (D.padPreimageOpens σ Wp)) = Manifold.IdealSheaf.pullback (D.padRestrictMap σ Wp) ⋯ ((D.padAlongData σ).sigmaTriple.I.restrict ((D.padAlongData σ).ambImage Wp))

The restricted ideals correspond along it: I|U = m^*(I⁺|U⁺) (pullback_inclusionMap_sigmaPadSlice and pullback_symm_pullback, then pullback_pullback along the inclusions).

The core: the order isomorphism and the isomorphism of the coproduct local resolutions

theorem Hironaka.Manifold.LocalEmbeddingData.exists_padIdentityCore {𝕜 : 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) : ∃ (o : (D.padAlongData σ).sigmaIndex bed Wp hWp ≃o D.sigmaIndex bed (D.padPreimageOpens σ Wp) ⋯) (ψ : bed.localResolutionOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯) (hψ : CategoryTheory.IsIso ψ), (∀ (σp : (D.padAlongData σ).sigmaIndex bed Wp hWp), AnalyticSpace.QuotientSpace.comap (↑ψ) (D.sigmaMembers bed (D.padPreimageOpens σ Wp) ⋯ hbed (o σp)) = (D.padAlongData σ).sigmaMembers bed Wp hWp hbed σp) ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ψ) (bed.localResolutionMapOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯) = CategoryTheory.CategoryStruct.comp (bed.localResolutionMapOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯) (Manifold.IdealSheaf.homOfPullbackEq (D.padRestrictMap σ Wp) ⋯ ⋯)

The padding identity at the coproduct, its data ([Kol07, 34.4] at the coproduct slice): an order isomorphism of the label sets and an isomorphism ψ of the coproduct local resolutions carrying the datum's member of label o σp to the padded datum's member of label σp, and lying over the ambients — the padded coproduct's map to its closed subspace, after ψ⁻¹, is the datum's map followed by the slice identification. The argument: bed.closedEmbedding at (S*, I⁺, J*), exists_closedSubmanifold_last_pushforwardRestrict_boundary (the carried slice S*_r, G₁, the ideal identity, the composite square, the order isomorphism o₁), the cast leg at (Φ, I, J*) (G₀, ε₀), ψ := inv (homOfPullbackEq (incl_{S*_r} ∘ (G₀.trans G₁))), the member identity from pullback_idealSheaf_inclusionMap_comp_of_hasSncWithProper in equality form.

The data exposed: o and ψ by choice from the core, with their clauses; the assembly

noncomputable def Hironaka.Manifold.LocalEmbeddingData.padIdentityOrderIso {𝕜 : 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.padAlongData σ).sigmaIndex bed Wp hWp ≃o D.sigmaIndex bed (D.padPreimageOpens σ Wp) ⋯

The order isomorphism of the label sets o : ι⁺ ≃o ι, chosen from the core exists_padIdentityCore (the padded run is the run of the coproduct slice, stage by stage).

Equations

• D.padIdentityOrderIso σ Wp hWp bed hbed = ⋯.choose

noncomputable def Hironaka.Manifold.LocalEmbeddingData.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) : bed.localResolutionOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯

The isomorphism ψ of the coproduct local resolutions, chosen from the core exists_padIdentityCore; the piece clause (CoproductPadIdentityPiece.lean) is stated against this NAMED ψ.

Equations

• D.padIdentityIso σ Wp hWp bed hbed = ⋯.choose

theorem Hironaka.Manifold.LocalEmbeddingData.padIdentityIso_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) : CategoryTheory.IsIso (D.padIdentityIso σ Wp hWp bed hbed)

ψ is an isomorphism (ψ = inv (homOfPullbackEq (incl_{S*_r} ∘ (G₁ ∘ G₀))), the inverse of an isomorphism).

theorem Hironaka.Manifold.LocalEmbeddingData.comap_padIdentityIso_sigmaMembers {𝕜 : 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) (σp : (D.padAlongData σ).sigmaIndex bed Wp hWp) : AnalyticSpace.QuotientSpace.comap (↑(D.padIdentityIso σ Wp hWp bed hbed)) (D.sigmaMembers bed (D.padPreimageOpens σ Wp) ⋯ hbed ((D.padIdentityOrderIso σ Wp hWp bed hbed) σp)) = (D.padAlongData σ).sigmaMembers bed Wp hWp hbed σp

The members correspond, in equality form for EVERY label: ψ carries the datum's member of label o σp to the padded datum's member of label σp (the ideal-level trace identity pullback_idealSheaf_inclusionMap_comp_of_hasSncWithProper along incl_{S*_r} ∘ G₁, the cast helper at G₀, the generic member transport).

theorem Hironaka.Manifold.LocalEmbeddingData.localResolutionMapOn_comp_inv_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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (D.padIdentityIso σ Wp hWp bed hbed)) (bed.localResolutionMapOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯) = CategoryTheory.CategoryStruct.comp (bed.localResolutionMapOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯) (Manifold.IdealSheaf.homOfPullbackEq (D.padRestrictMap σ Wp) ⋯ ⋯)

ψ lies over the ambients, in MORPHISM form: the padded coproduct's map to its restricted closed subspace, after ψ⁻¹, is the datum's map followed by the closed-subspace morphism over the restricted slice map padRestrictMap : N|U → N⁺|U⁺ (incl_{S*} ∘ Φ on the reading opens) — the generic quotient square along incl_{S*_r} ∘ (G₁ ∘ G₀) and padRestrictMap.

theorem Hironaka.Manifold.LocalEmbeddingData.localResolutionMapOn_inv_padIdentityIso_apply {𝕜 : 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) (z : ↑↑(bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯).toPresheafedSpace) : ↑↑(↑(bed.localResolutionMapOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯) (↑(CategoryTheory.inv (D.padIdentityIso σ Wp hWp bed hbed)) z)) = ⋯.inclusionMap ((D.sigmaPadSliceDiffeomorph σ) ↑↑(↑(bed.localResolutionMapOn D.sigmaTriple ⋯ (D.ambImage (D.padPreimageOpens σ Wp)) ⋯) z))

ψ lies over the ambients, in POINT form (the corollary of the morphism form through toFun_homOfPullbackEq_val and inclusion_padRestrictMap): on points, localResolutionMapOn⁺ (ψ⁻¹ z) lies over incl_{S*} (Φ (localResolutionMapOn z)) in the padded coproduct ambient.

theorem Hironaka.Manifold.LocalEmbeddingData.padIdentityOn_of_forall_piece {𝕜 : 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) (hc : ∀ (i : (D.padAlongData σ).ι), ∃ (ψᵢ : ((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)) : D.PadIdentityOn σ Wp hWp bed hbed

The padding identity from its core and the piece clause: given, on every piece i, an isomorphism ψᵢ over the piece with resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i for the NAMED ψ = padIdentityIso (the piece clause, CoproductPadIdentityPiece.lean), D.PadIdentityOn σ Wp hWp bed hbed holds with the data o, ψ and their clauses.