Blow-up sequence functors on analytic triples and their functoriality clauses

A blow-up sequence functor is a functor B whose inputs are triples (X, I, E) and whose outputs are blow-up sequences with specified centres; the length of the sequence r, the schemes X_i and the centres Z_i all depend on (X, I, E) [Kol07, Definition 31]. The functors on analytic manifolds are valued in lists of centres CenterList ψ₀ M, their toSuccession being what the main theorems use; "commutes with h" as in [Kol07, 34.1], with the class of h restricted to surjective local analytic isomorphisms (first bullet) and open embeddings (second bullet: delete empty blow-ups and reindex); the clause 34.2 (change of fields) has no counterpart on manifolds; 34.3 and 34.4 are kept in the form used by [Kol07, Theorem 103, (3)]. The corresponding definitions for schemes are AlgebraicGeometry.BlowUpSequenceAssignment and its clauses; every definition below is its analogue on manifolds.

• AnalyticBlowUpSequenceFunctor ψ₀ Dom: seq T h : CenterList ψ₀ M for every triple of the class Dom, whose outputs contain no empty blow-ups ([Kol07, 32], the field noEmptyCenters). One functor per model (E, ψ₀), as one functor per field for schemes: Kollár's named functors are indexed by the dimension (BO_{n,m}, BD_{n,m,0}).
• CommutesWith B T T' h hh ([Kol07, 34.1]): B(N, h^* 𝓘, h⁻¹(E)) = h^* B(M, 𝓘, E), an equality of lists, h^* the canonical pull-back BlowUpSequence.pullback along the local analytic isomorphism h; CommutesWithSurjectiveLocalIsos B (first bullet); CommutesWithOpenEmbeddings B (second bullet: the value on the open piece is the pull-back with its empty blow-ups deleted, BlowUpSequence.eraseEmpty); CommutesWithLocalIsos B = both.
• CommutesWithSurjectionsIn B 𝓜 ([Kol07, Theorem 105, (3)]): B commutes with every surjective member of the class 𝓜 of analytic maps.
• CommutesWithClosedEmbeddingsOfEmptyDivisor B' B ([Kol07, 34.3] in the form of [Kol07, Theorem 103, (3)]): for a closed submanifold τ : S ↪ M of codimension s and ideal sheaves 𝓘 on M, J on S with 𝒪_M/𝓘 = τ_*(𝒪_S/J) (𝓘 ⊇ I_S and J = τ^* 𝓘), B(M, 𝓘, ∅) = τ_* B'(S, J, ∅), with B' a functor at the model 𝕜^{n−s} of the submanifolds (the BMO_{n−1,1}(Y, J, 1, ∅) of Theorem 103 (3), the mark 1 absorbed into B') and τ_* the push-forward of lists BlowUpSequence.pushforward.
• The vocabulary of [Kol07, Theorem 105]: GlobalizationData GT LT (clause (2): (i) every point of a global triple lies in the range of an open embedding from a local triple carrying the pullback data, (ii) LT closed under countable disjoint unions); IsLocalCover GT LT T T' g (the proof's g : X' → X: a surjective coproduct of open embeddings from a local triple carrying the pullback data of a global one); IsFibreProduct g₁ g₂ p₁ p₂ (the proof's X'' := X' ×_X X' with its projections τ₁, τ₂: local analytic isomorphisms p₁, p₂ with g₁ ∘ p₁ = g₂ ∘ p₂, jointly a bijection onto the set-theoretic fibre product); LocalCoversFibreClosed GT LT (a hypothesis the proof of Theorem 105 uses tacitly: a fibre product of two local covers carrying the pullback data is in LT).

The globalization is carried out, in the compatible-family form, in Hironaka.Resolution.Analytic.OrderReduction.GlobalizeFam.

structure Manifold.AnalyticBlowUpSequenceAssignment {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop) : Type (max (u + 1) u_1)

A blow-up sequence functor on the class Dom of analytic triples at the model (E, ψ₀) — the list of centres B(M, 𝓘, E) : CenterList ψ₀ M assigned to every triple of the class, "with specified centers" (the list carries them; the length of the sequence, the stages and the centres all depend on the triple), whose outputs contain no empty blow-ups ([Kol07, 32]). The functoriality clauses of Kol07, 34 are separate predicates.

• seq {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) : Dom T → AnalyticManifold.BlowUpSequence ψ₀ M

  The list of centres B(M, 𝓘, E) assigned to a triple of the class.

• noEmptyCenters {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : Dom T) : (self.seq T h).NoEmptyCenters

  [Kol07, 32]: the output contains no empty blow-ups.

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (T' : AnalyticTriple ψ₀ N) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Prop

B commutes with h when B(Y, h^* I, h⁻¹(E)) = h^* B(X, I, E) [Kol07, 34.1]: for triples T on M, T' on N of the class and a local analytic isomorphism h : N → M, the value on T' is the pull-back ([Kol07, Definition 30, 30.1], BlowUpSequence.pullback) of the value on T; an equality of lists of centres. Used with T'.IsPullbackOf T h.

Equations

• B.CommutesWith T T' h hh = ∀ (hT : Dom T) (hT' : Dom T'), B.seq T' hT' = (B.seq T hT).pullback h hh

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithSurjectiveLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) : Prop

[Kol07, 34.1], first bullet, with this class: B commutes with surjective local analytic isomorphisms — with every surjective local analytic isomorphism h : N → M between triples of which T' carries the pullback data of T.

Equations

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

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithOpenEmbeddings {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) : Prop

[Kol07, 34.1], second bullet, with this class: B commutes with open embeddings — for every analytic open embedding h : N → M with T' carrying the pullback data of T, the value on T' is the pull-back h^* B(X, I, E) with every blow-up whose centre is empty deleted and the sequence reindexed (BlowUpSequence.eraseEmpty).

Equations

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

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) : Prop

[Kol07, 34.1], both bullets with these classes ("smooth morphism" → "local analytic isomorphism"): B commutes with local analytic isomorphisms — with the surjective ones, and with open embeddings up to the deletion of empty blow-ups.

Equations

• B.CommutesWithLocalIsos = (B.CommutesWithSurjectiveLocalIsos ∧ B.CommutesWithOpenEmbeddings)

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithSurjectionsIn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) (𝓜 : {M N : AnalyticManifold 𝕜 E} → AnalyticMap N M → Prop) : Prop

B commutes with surjections in 𝓜 [Kol07, Theorem 105, (3)]: B.CommutesWith for every surjective local analytic isomorphism h of the class 𝓜 between triples of which the source carries the pullback data of the target.

Equations

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

def Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithClosedEmbeddingsOfEmptyDivisor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {s : ℕ} {Dom' : {M' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} → AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) M' → Prop} (B' : AnalyticBlowUpSequenceAssignment (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} => Dom') : Prop

[Kol07, 34.3] in the form used by Theorem 103 (3) ("BO_{n,1}(X, I, ∅) = τ_* BMO_{n−1,1}(Y, J, 1, ∅)"): the functor B at the model (E, ψ₀) commutes with closed embeddings whenever E = ∅, through the functor B' at the model 𝕜^{n−s} of the closed submanifolds of codimension s — for every closed submanifold τ : S ↪ M of codimension s and ideal sheaves 𝓘 on M, J on the bundled S with nonzero stalks and O_M/𝓘 = τ_*(O_S/J) (𝓘 contains the ideal sheaf of S and J = τ^* 𝓘), B(M, 𝓘, ∅) = τ_* B'(S, J, ∅) with τ_* the push-forward of lists (BlowUpSequence.pushforward). Theorem 103 (3)'s mark 1 on J is absorbed into B'.

Equations

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

The vocabulary of [Kol07, Theorem 105] on manifolds

def Manifold.IsFibreProduct {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N₁ N₂ P : AnalyticManifold 𝕜 E} (g₁ : AnalyticMap N₁ M) (g₂ : AnalyticMap N₂ M) (p₁ : AnalyticMap P N₁) (p₂ : AnalyticMap P N₂) : Prop

The fibre product X'' := X' ×_X X' with its two projections in the proof of [Kol07, Theorem 105], and X'' := ∐_{i≤j} Uᵢ ∩ Uⱼ in the proof of [Kol07, Proposition 37]: (P, p₁, p₂) is a fibre product of g₁ : N₁ → M and g₂ : N₂ → M — p₁, p₂ local analytic isomorphisms with g₁ ∘ p₁ = g₂ ∘ p₂, jointly a bijection onto the set-theoretic fibre product {(x, y) | g₁ x = g₂ y}.

Equations

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

structure Manifold.AnalyticTriple.GlobalizationData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop) : Prop

Clause (2) of [Kol07, Theorem 105] asks for two classes of triples, GT (global) and LT (local), such that (i) every point of a triple of GT lies in the image of an 𝓜-morphism gₓ : Uₓ → X whose pulled-back triple (Uₓ, g^* I, g⁻¹ E) is in LT, and (ii) LT is closed under disjoint unions. Here, with 𝓜 the open embeddings: (i) every point of a global triple lies in the range of an analytic open embedding from a local triple carrying the pullback data; (ii) LT is closed under countable disjoint unions (Warning 38). No inclusion LT ⊆ GT is assumed; Theorem 105's "extension" is agreement on LT ∩ GT.

• exists_isPullbackOf {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) : GT T → ∀ (x : M.carrier), ∃ (N : AnalyticManifold 𝕜 E) (T' : AnalyticTriple ψ₀ N) (g : AnalyticMap N M), IsAnalyticOpenEmbedding g ∧ x ∈ Set.range ⇑g ∧ T'.IsPullbackOf T g ∧ LT T'

  Clause (2)(i) of [Kol07, Theorem 105]: every point of a global triple has a local triple over it along an open embedding.

• closedUnderSigma : ClosedUnderSigma fun {M : AnalyticManifold 𝕜 E} => LT

  Clause (2)(ii) of [Kol07, Theorem 105]: LT is closed under countable disjoint unions.

def Manifold.AnalyticTriple.IsLocalCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop) {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (T' : AnalyticTriple ψ₀ N) (g : AnalyticMap N M) : Prop

The proof of [Kol07, Theorem 105] chooses 𝓜-morphisms gₓᵢ : Uₓᵢ → X whose images cover X, forms the disjoint union X' := ∐ᵢ Uₓᵢ with the induced g : X' → X, and uses that (X', g^* I, g⁻¹ E) ∈ LT: g : N → M is a local cover of the global triple T by the local triple T' — T ∈ GT, T' ∈ LT, g a surjective coproduct of open embeddings, and T' carries the pullback data of T along g.

Equations

• Manifold.AnalyticTriple.IsLocalCover GT LT T T' g = (GT T ∧ LT T' ∧ Manifold.IsCoprodOfOpenEmbeddings g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g)

def Manifold.AnalyticTriple.LocalCoversFibreClosed {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (GT LT : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop) : Prop

A hypothesis the proof of Theorem 105 uses tacitly: Kollár applies B to X'' := X' ×_X X', which requires X'' with the pullback data to be a local triple although (1)–(3) state no such clause. The class LT is closed under fibre products of local covers: for two local covers g₁ : N₁ → M, g₂ : N₂ → M of a global triple, a triple on a fibre product (P, p₁, p₂) of g₁ and g₂ carrying the pullback data of T₁ along p₁ is in LT.

Equations

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