Order reduction on analytic manifolds: the classes and the first centre

Kollár's order reduction for ideals, Theorem 103, and its ingredient Lemma 102 are stated for triples (X, I, E) with dim X = n and max-ord I ≤ m ([Kol07, Lemma 102], [Kol07, Theorem 103]). This module fixes the analytic form of their hypotheses on an analytic triple T = (M, 𝓘, E) (a manifold M modelled on E ≃ 𝕜ⁿ, an ideal sheaf 𝓘 nonzero at every point, a boundary E with simple normal crossings and ordered index set) and defines the first centre of Lemma 102.

• AnalyticTriple.BOClass m — the class on which the order-reduction functors BO_{n,m} are defined: 1 ≤ m, the order of 𝓘 is at most m at every point (the pointwise form of max-ord I ≤ m), and only finitely many members of the boundary are nonempty (Kollár's finite index set E = ∑_{i=1}^s E^i; on a manifold this replaces quasi-compactness, and it is restored on every relatively compact open subset in Finiteness.lean). The dimension is that of the model space and needs no clause.
• AnalyticTriple.HasMaximalContact m — the hypothesis of Step 2 of the proof of Theorem 103, "there is a smooth hypersurface of maximal contact H ⊂ X", in the static form of [Kol07, Theorem 80]: a closed hypersurface whose ideal sheaf lies in the maximal contact ideal MC(𝓘) = D^{m-1} 𝓘 of [Kol07, Definition 79].
• AnalyticTriple.ClosedUnderLocalIsoPullbackOverCosupp Dom m — a class Dom of triples is closed under pull-back along local analytic isomorphisms whose image contains cosupp(𝓘, m); this is the hypothesis on the class in Step 2.3 of [Kol07, 104], the independence of the hypersurface of maximal contact.
• AnalyticTriple.LocalMCClass m — the class on which Step 2 of the proof of Theorem 103 defines the functor: the triples of BOClass m with a global hypersurface of maximal contact (the pieces X^{(j)} of Step 3).
• BD.Zminus1 𝓘 m Y — the first centre Z_{-1} of the proof of [Kol07, Lemma 102]: the union of the irreducible components of the hypersurface Y = E^j contained in cosupp(𝓘, m); on a manifold the irreducible components of a smooth hypersurface are its connected components.
• AnalyticBlowUpSequenceAssignment.IndifferentToEmptyMembers — deleting empty members from the boundary does not change the value of the functor; not in the sources, the counterpart for the members of the boundary of Kollár's empty blow-up convention [Kol07, 32], which concerns centres.

These definitions are the vocabulary of the whole of OrderReduction/: Lemma 102's functor (BD*.lean), Steps 2.1–2.2 of the proof of Theorem 103 (Step21*.lean, Step22*.lean), its globalization (Globalize*.lean) and the assembled structure BOanFam.

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

The class of the order-reduction functors BO_{n,m} ([Kol07, Lemma 102] and [Kol07, Theorem 103]: triples (X, I, E) with dim X = n and max-ord I ≤ m): 1 ≤ m, the order of 𝓘 is at most m at every point, and only finitely many members of the boundary are nonempty (Kollár's finite index set; the substitute for quasi-compactness on a manifold). The dimension is that of the model space, so no dimension clause is stated.

Equations

• Manifold.AnalyticTriple.BOClass m T = (1 ≤ m ∧ (∀ (x : ↑↧M✝.carrier), Manifold.IdealSheaf.ord T.I x ≤ ↑m) ∧ Finite { j : T.F.ι // T.F.hyp j ≠ ∅ })

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

The hypothesis of Step 2 of the proof of [Kol07, Theorem 103], "there is a smooth hypersurface of maximal contact H ⊂ X", in the static form of [Kol07, Theorem 80]: a closed hypersurface of M whose ideal sheaf lies in MC(𝓘) = D^{m-1} 𝓘 ([Kol07, Definition 79]).

Equations

• Manifold.AnalyticTriple.HasMaximalContact m T = ∃ (H : Set M.carrier) (hH : Manifold.IsClosedSubmanifold ψ₀ H 1), hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (m - 1)

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

The class on which Step 2 of the proof of [Kol07, Theorem 103] defines the order-reduction functor (the "maximal contact case"; the pieces X^{(j)} of Step 3): the triples of BOClass m with a global hypersurface of maximal contact.

Equations

• Manifold.AnalyticTriple.LocalMCClass m T = (Manifold.AnalyticTriple.BOClass m T ∧ Manifold.AnalyticTriple.HasMaximalContact m T)

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

The class Dom is closed under pull-back along local analytic isomorphisms covering the cosupport cosupp(𝓘, m) = {ord 𝓘 ≥ m}: a triple carrying the pull-back data of a member of the class along a local analytic isomorphism whose image contains cosupp(𝓘, m) is a member. This is the hypothesis on the class in Step 2.3 of [Kol07, 104], where the functor is evaluated on pull-backs covering the cosupport.

Equations

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

def Hironaka.Manifold.BD.Zminus1 {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (m : ℕ) (Y : Set M.carrier) : Set M.carrier

The first centre of the proof of [Kol07, Lemma 102], "let Z_{-1} be the union of those irreducible components E^{jk} ⊂ E^j that are contained in cosupp(I, m)", with the irreducible components of the smooth hypersurface Y = E^j read as its connected components: the points of Y whose connected component in Y lies in {ord 𝓘 ≥ m}.

Equations

• Hironaka.Manifold.BD.Zminus1 I m Y = {x : M.carrier | x ∈ Y ∧ connectedComponentIn Y x ⊆ {y : M.carrier | ↑m ≤ Manifold.IdealSheaf.ord I y}}

def Manifold.AnalyticBlowUpSequenceAssignment.IndifferentToEmptyMembers {𝕜 : 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

A blow-up sequence functor on a class of analytic triples is indifferent to empty boundary members when deleting empty members does not change its value: for every triple T, every boundary F' on M with simple normal crossings embedding order-preservingly into T.F along e, with the members matched along e and the empty hypersurface at every index outside the range of e, the values at T and at T with boundary F' agree. Not in the sources: the counterpart, for the members of the boundary, of Kollár's convention that empty blow-ups are ignored ([Kol07, 32]; [Kol07, 34.1]). Only the deletion of empty members is covered; no invariance under permutations of the index set is asserted.

Equations

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