Analytic triples (M, 𝓘, E) and the classes of maps between them

A blow-up sequence functor takes as inputs triples (X, I, E), where I ⊂ 𝒪_X is an ideal sheaf nonzero on every irreducible component and E a divisor with ordered index set [Kol07, Definition 31]. On analytic manifolds: M an analytic manifold, 𝓘 a locally finitely generated ideal sheaf with 𝓘_a ≠ 0 everywhere, E a simple normal crossings divisor with ordered index set. The corresponding structure for schemes is Hironaka.Triple; the analytic triple is data on the manifold M (AnalyticTriple ψ₀ M, with the model chart ψ₀ : E ≃L[𝕜] 𝕜ⁿ fixed as for CenterList), so that the pulled-back triple (N, h^* 𝓘, h⁻¹(E)) of [Kol07, 34.1] lives on N without an equality of manifolds.

• HypersurfaceFamily.comap h F: the inverse image h⁻¹(E) = (h⁻¹(E^j))_j of a hypersurface family, the index set kept ([Kol07, 34.1]; [Kol07, Definition 30, 30.1]).
• AnalyticTriple ψ₀ M: the triple (M, 𝓘, E); IsPullbackOf T' T h (the analogue of Hironaka.Triple.IsPullbackOf): T' carries the pullback data (N, h^* 𝓘, h⁻¹(E)) of T along h.
• IsAnalyticOpenEmbedding h: a local analytic isomorphism that is injective, an analytic isomorphism onto an open subset, Kollár's open immersion (an injective analytic map with open image is not one: x ↦ x³).
• IsSigmaOf T Ts ι ([Kol07, Warning 38]; the analogue of Hironaka.Triple.IsSigmaOf): T is the disjoint union of the family Ts along the open embeddings ι i with pairwise disjoint ranges covering M, the data of T restricting to those of Ts i; ClosedUnderSigma Dom: the class is closed under countable disjoint unions (the algebraic form is finite).
• IsCoprodOfOpenEmbeddings g ([Kol07, Theorem 105, (1)], "all open immersions", read as its proof and the global case of the proof of [Kol07, Theorem 103] use it, for the coproduct g : X* → X of the injections X^(j) ↪ X; the analogue of openImmersionCoprods): a local analytic isomorphism injective on each piece of a clopen decomposition of its source.
• AnalyticManifold.IsCountableChartUnion M, AnalyticTriple.IsLocal T: the local triples of [Kol07, Proposition 37] on manifolds ("X' := ∐ Uᵢ … is affine"; [Kol07, 44], "a locally defined blow-up sequence functor"): M is a countable disjoint union of chart domains (sources of charts of the maximal atlas).

These are the inputs of the blow-up sequence functors of Hironaka.Manifold.FiniteSuccession.Functor.Basic.

def Manifold.HypersurfaceFamily.comap {M N : Type u} (h : N → M) (F : HypersurfaceFamily M) : HypersurfaceFamily N

The inverse image of a hypersurface family along a map, componentwise, the ordered index set kept.

Equations

• Manifold.HypersurfaceFamily.comap h F = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := fun (j : F.ι) => h ⁻¹' F.hyp j }

@[simp]

theorem Manifold.HypersurfaceFamily.comap_hyp {M N : Type u} (h : N → M) (F : HypersurfaceFamily M) (j : F.ι) : (comap h F).hyp j = h ⁻¹' F.hyp j

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

An analytic triple (M, 𝓘, E) on the analytic manifold M — a locally finitely generated ideal sheaf 𝓘 with nonzero stalks everywhere (Kollár's "nonzero on every irreducible component") and a simple normal crossings divisor E with ordered index set, in the model chart iso ψ₀.

• I : M.IdealSheaf

  The ideal sheaf 𝓘 (IdealSheaf, locally finitely generated by definition).

• isNonzeroEverywhere : IdealSheaf.IsNonzeroEverywhere self.I

  𝓘_a ≠ 0 at every point.

• F : HypersurfaceFamily M.carrier

  The divisor E = (E^j)_j, an ordered countable family of hypersurfaces.

• isSnc : HypersurfaceFamily.IsSnc ψ₀ self.F

  E is a simple normal crossings divisor.

def Manifold.IsAnalyticOpenEmbedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) : Prop

Kollár's open immersions on manifolds: an analytic map that is a local analytic isomorphism and injective — an analytic isomorphism onto an open subset.

Equations

• Manifold.IsAnalyticOpenEmbedding h = (IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h ∧ Function.Injective ⇑h)

def Manifold.IsCoprodOfOpenEmbeddings {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) : Prop

[Kol07, Theorem 105] (1) ("all open immersions") read as its proof and the global case of the proof of [Kol07, Theorem 103] use it, for the induced map g : X' → X of a disjoint union X' := ∐ᵢ Uₓᵢ: g is a coproduct of open embeddings — a local analytic isomorphism that is injective on each piece of a clopen decomposition of its source (the analogue of openImmersionCoprods for schemes).

Equations

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

def AnalyticManifold.IsCountableChartUnion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : Prop

The local schemes of [Kol07, Proposition 37] on manifolds ("X' := ∐ᵢ Uᵢ … is affine"; Warning 38): the manifold is a countable disjoint union of chart domains — it has a countable clopen decomposition into sources of charts of the maximal atlas.

Equations

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

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

[Kol07, 34.1] ("B(Y, h^* I, h⁻¹(E))"): the triple T' on N carries the pullback data of T along h : N → M — its ideal sheaf is the inverse image ideal sheaf (comap) and its divisor the inverse image family (Triple.IsPullbackOf on manifolds).

Equations

• T'.IsPullbackOf T h = (T'.I = Manifold.IdealSheaf.pullback ⇑h ⋯ T.I ∧ T'.F = Manifold.HypersurfaceFamily.comap (⇑h) T.F)

def Manifold.AnalyticTriple.IsSigmaOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) {σ : Type u} {N : σ → AnalyticManifold 𝕜 E} (Ts : (i : σ) → AnalyticTriple ψ₀ (N i)) (ι : (i : σ) → AnalyticMap (N i) M) : Prop

[Kol07, Warning 38] with [Kol07, Notation 64] (1) ("possibly reducible"): the triple T on M is the disjoint union of the family Ts along the analytic open embeddings ι i : N i → M — pairwise disjoint ranges covering M, and the data of T restrict along ι i to the data of Ts i (Triple.IsSigmaOf on manifolds).

Equations

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

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

[Kol07, Warning 38], Theorem 105 (2)(ii) ("LT is closed under disjoint unions"): the class Dom of triples is closed under countable disjoint unions — a triple that is the disjoint union of a countable family of members of the class is a member (the covers are countable).

Equations

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

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

The local triples of [Kol07, Proposition 37] on manifolds ([Kol07, 44], "a locally defined blow-up sequence functor"): the triples on countable disjoint unions of chart domains.

Equations

• x✝.IsLocal = M.IsCountableChartUnion

The support of a pulled-back family (general tool)

@[simp]

theorem Manifold.HypersurfaceFamily.support_comap {M N : Type u} (h : N → M) (F : HypersurfaceFamily M) : (comap h F).support = h ⁻¹' F.support

The support of the pulled-back family is the preimage of the support.