Base transport of a blow-up sequence along a diffeomorphism

A smooth blow-up sequence B of M and a diffeomorphism g : M' ≃ M give a smooth blow-up sequence of M' with the same later stages: the first centre is pulled back along g and the first blow-down is followed by g⁻¹ (IsBlowUp.diffeomorph_comp); everything from stage 1 on is the data of B itself. The marked transforms, the boundaries and the strict transforms of a subset agree with those of B from stage 1 on (the base change of the marked transform along a diffeomorphism, the naturality of the reduced transform, the preimage of the strict transform), so the order and normal-crossings clauses of [Kol07, Definition 66] transport, and the centres lie in the strict transforms of g⁻¹(H) iff those of B lie in the strict transforms of H. The construction stays at the level of data: no equality or isomorphism of sequences is used.

• FiniteSuccession.firstCenter, firstMap, firstCenterSub, firstIsBlowUp: the stage-0 data read on M (stage 0 is finStages M later (castSucc 0), definitionally M).
• FiniteSuccession.transportBase g B: the transported sequence.
• markedTransformSeqAux_transportBase, boundarySeqAux_transportBase, strictTransformSeqAux_transportBase: the identities from stage 1 on.
• IdealSheaf.ordAlongIdeal_pullback_diffeomorph: the order along a centre transports.
• isOfOrderGe_transportBase, isOfOrder_transportBase, centersIn_transportBase_iff.
• AnalyticManifold.restrictTopDiffeomorph: M.restrict ⊤ ≃ M.

theorem Manifold.IdealSheaf.ordAlongIdeal_pullback_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (D J : M.IdealSheaf) (a : M'.carrier) : (pullback ⇑g ⋯ D).ordAlongIdeal (pullback ⇑g ⋯ J) a = ordAlongIdeal D J (g a)

The order of J along the centre D transports along a diffeomorphism: the stalk ideals are carried by the bijective germ map, which preserves inclusions and powers.

theorem Manifold.IdealSheaf.pullback_pullback_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (J : M.IdealSheaf) : pullback ⇑g.symm ⋯ (pullback ⇑g ⋯ J) = J

Pulling back along g and then along g⁻¹ is the identity.

def AnalyticManifold.restrictTopDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (M.restrict ⊤).carrier M.carrier ⊤

The open subset ⊤ ⊆ M as a manifold is M: the inclusion is an analytic isomorphism.

Equations

• M.restrictTopDiffeomorph = { toFun := Subtype.val, invFun := fun (x : M.carrier) => ⟨x, trivial⟩, left_inv := ⋯, right_inv := ⋯, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem AnalyticManifold.coe_restrictTopDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : ⇑M.restrictTopDiffeomorph = ⇑(M.inclusion ⊤)

The stage-0 data, read on M

def AnalyticManifold.FiniteSuccession.firstCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (h : 0 < B.length) : M.IdealSheaf

The first centre C_0 as an ideal sheaf on M (the structure types it on finStages M later (castSucc 0), which is M definitionally but not syntactically).

Equations

• B.firstCenter h = B.center ⟨0, h⟩

def AnalyticManifold.FiniteSuccession.firstMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (h : 0 < B.length) : AnalyticMap (B.later ⟨0, h⟩) M

The first blow-down σ_1 : U_1 → M.

Equations

• B.firstMap h = B.map ⟨0, h⟩

theorem AnalyticManifold.FiniteSuccession.firstCenterSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (h : 0 < B.length) : Manifold.IsClosedSubmanifold (B.chartAt ⟨0, h⟩) (Manifold.IdealSheaf.support (B.firstCenter h)) (B.codim ⟨0, h⟩)

Z_0 ⊆ M is a closed submanifold.

theorem AnalyticManifold.FiniteSuccession.firstIsBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (h : 0 < B.length) : Manifold.IsBlowUp (B.chartAt ⟨0, h⟩) (Manifold.IdealSheaf.support (B.firstCenter h)) (B.codim ⟨0, h⟩) ⇑(B.firstMap h)

σ_1 is a blowing-up of M along Z_0.

theorem AnalyticManifold.FiniteSuccession.idealSheaf_firstCenterSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (h : 0 < B.length) : ⋯.idealSheaf = B.firstCenter h

theorem AnalyticManifold.FiniteSuccession.pullback_firstCenter_eq_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (h : 0 < B.length) : Manifold.IdealSheaf.pullback ⇑g ⋯ (B.firstCenter h) = ⋯.idealSheaf

The pulled-back first centre is the ideal sheaf of the closed submanifold g⁻¹(Z_0) (comap_idealSheaf_of_isLocalDiffeomorph).

theorem AnalyticManifold.FiniteSuccession.support_pullback_firstCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (h : 0 < B.length) : (Manifold.IdealSheaf.pullback ⇑g ⋯ (B.firstCenter h)).support = ⇑g ⁻¹' Manifold.IdealSheaf.support (B.firstCenter h)

The transported sequence

noncomputable def AnalyticManifold.FiniteSuccession.transportBaseCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (i : Fin B.length) : (M'.finStages B.later i.castSucc).IdealSheaf

The centres of the transported sequence: the first pulled back along g, the others B's.

Equations

• B.transportBaseCenter g ⟨0, h⟩ = Manifold.IdealSheaf.pullback ⇑g ⋯ (B.firstCenter h)
• B.transportBaseCenter g ⟨k.succ, h⟩ = B.center ⟨k + 1, h⟩

def AnalyticManifold.FiniteSuccession.transportBaseMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (i : Fin B.length) : AnalyticMap (M'.finStages B.later i.succ) (M'.finStages B.later i.castSucc)

The blow-downs of the transported sequence: the first followed by g⁻¹, the others B's.

Equations

• B.transportBaseMap g ⟨0, h⟩ = ⟨⇑g.symm ∘ ⇑(B.firstMap h), ⋯⟩
• B.transportBaseMap g ⟨k.succ, h⟩ = B.map ⟨k + 1, h⟩

theorem AnalyticManifold.FiniteSuccession.transportBase_isMonoidal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (i : Fin B.length) : (B.transportBaseMap g i).IsMonoidalTransformation (B.transportBaseCenter g i)

Each transported blow-down is a monoidal transformation with the transported centre: at stage 0, the centre g⁻¹(Z_0) is a closed submanifold with the pulled-back ideal sheaf (comap_idealSheaf_of_isLocalDiffeomorph) and g⁻¹ ∘ σ_1 is a blowing-up along it (IsBlowUp.diffeomorph_comp); from stage 1 on the data are those of B.

noncomputable def AnalyticManifold.FiniteSuccession.transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) : M'.FiniteSuccession

The sequence B carried to M' along the diffeomorphism g : M' ≃ M: the same length and later stages, the first centre pulled back along g, the first blow-down followed by g⁻¹. A blow-up sequence in the sense of [Kol07, Definition 29]; not in the sources, an auxiliary construction.

Equations

• B.transportBase g = { length := B.length, later := B.later, center := B.transportBaseCenter g, map := B.transportBaseMap g, isMonoidal := ⋯ }

theorem AnalyticManifold.FiniteSuccession.transportBase_length {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) : (B.transportBase g).length = B.length

theorem AnalyticManifold.FiniteSuccession.transportBase_firstCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (h : 0 < (B.transportBase g).length) : (B.transportBase g).firstCenter h = Manifold.IdealSheaf.pullback ⇑g ⋯ (B.firstCenter h)

theorem AnalyticManifold.FiniteSuccession.transportBase_center_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (k : ℕ) (h : k + 1 < B.length) : (B.transportBase g).center ⟨k + 1, h⟩ = B.center ⟨k + 1, h⟩

theorem AnalyticManifold.FiniteSuccession.transportBase_map_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (k : ℕ) (h : k + 1 < B.length) : (B.transportBase g).map ⟨k + 1, h⟩ = B.map ⟨k + 1, h⟩

theorem AnalyticManifold.FiniteSuccession.transportBase_firstMap_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (h : 0 < (B.transportBase g).length) (p : (B.later ⟨0, h⟩).carrier) : ((B.transportBase g).firstMap h) p = g.symm ((B.firstMap h) p)

The stage-≥ 1 identities

theorem AnalyticManifold.FiniteSuccession.strictTransformSeqAux_transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (H : Set M.carrier) (k : ℕ) (h : k + 1 < B.length + 1) : (B.transportBase g).strictTransformSeqAux (⇑g ⁻¹' H) (k + 1) h = B.strictTransformSeqAux H (k + 1) h

The strict transforms of g⁻¹(H) along the transported sequence are those of H along B from stage 1 on.

theorem AnalyticManifold.FiniteSuccession.centersIn_transportBase_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (H : Set M.carrier) : (B.transportBase g).CentersIn (⇑g ⁻¹' H) ↔ B.CentersIn H

The centres of the transported sequence lie in the strict transforms of g⁻¹(H) iff the centres of B lie in those of H.

theorem AnalyticManifold.FiniteSuccession.boundarySeqAux_transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) (E₀ : M.IdealSheaf) (k : ℕ) (h : k + 1 < B.length + 1) : (B.transportBase g).boundarySeqAux (Manifold.IdealSheaf.pullback ⇑g ⋯ E₀) (k + 1) h = B.boundarySeqAux E₀ (k + 1) h

The boundaries of the transported sequence started with g^* E₀ are those of B started with E₀ from stage 1 on (the naturality of the reduced transform on the square σ_1 = g ∘ (g⁻¹ ∘ σ_1) with the identity of stage 1).

theorem AnalyticManifold.FiniteSuccession.markedTransformSeqAux_transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {I E₀ : M.IdealSheaf} {m : ℕ} (hB : B.IsOfOrderGe I m E₀) (k : ℕ) (h : k + 1 < B.length + 1) : (B.transportBase g).markedTransformSeqAux (Manifold.IdealSheaf.pullback ⇑g ⋯ I) m (k + 1) h = B.markedTransformSeqAux I m (k + 1) h

The marked transforms of (g^* I, m) along the transported sequence are those of (I, m) along B from stage 1 on, for B of order ≥ m (so that the mark is legitimate at stage 0): the base change of the marked transform along a diffeomorphism (birationalTransform_image_diffeomorph), with the congruence of the blow-up witnesses (MarkedIdealSheaf.birationalTransform_congr).

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {I E₀ : M.IdealSheaf} {m : ℕ} (hB : B.IsOfOrderGe I m E₀) : (B.transportBase g).IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑g ⋯ I) m (Manifold.IdealSheaf.pullback ⇑g ⋯ E₀)

A sequence of order ≥ m for (I, m) with the boundary E₀ transports to one of order ≥ m for (g^* I, m) with the boundary g^* E₀: stage 0 by the transport of clause (3′) along g (HasOnlyNormalCrossingsWith.pullback_diffeomorph) and of the order along the centre, the later stages by the identities of the marked transforms and boundaries.

theorem AnalyticManifold.FiniteSuccession.isOfOrder_transportBase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M'.carrier M.carrier ⊤) {I E₀ : M.IdealSheaf} {m : ℕ} (hB : B.IsOfOrder I E₀ m) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) : (B.transportBase g).IsOfOrder (Manifold.IdealSheaf.pullback ⇑g ⋯ I) (Manifold.IdealSheaf.pullback ⇑g ⋯ E₀) m

A sequence of order exactly m transports to one of order exactly m. The proof passes through the ≥ m form and [Kol07, Remark 67] (ord being invariant under a diffeomorphism) rather than transporting the weak transforms directly, which is why the hypothesis hmax : ∀ y, I.ord y ≤ m is carried.