Hypersurfaces of maximal contact: the definitions #
Following [Kol07, 51] and [Kol07, Definitions 78 and 79]. For an ideal sheaf I on a smooth
variety X with m = max-ord I, order reduction for I should follow from order reduction for
(I|_H, m) on a smooth hypersurface H; for this the points where the birational transforms of
I have order ≥ m must stay on the birational transforms of H ([Kol07, 13.3 and 51.1]). The
tool is the derivative ideal.
- The maximal contact ideal ([Kol07, Definition 79]; also [Kol07, 51.2]):
MC(I) := D^{m-1}(I), the iterated derivative ideal sheafderivativeIter f (m - 1) I, the largest nontrivial derivative ideal.MC(I)has order1atxiford_x I = mand order0iford_x I < m([Kol07, Lemma 74 (3)]), socosupp MC(I) = cosupp (I, m) = {x : ord_x I ≥ m}(coe_support_MC,ord_MC_eq_one,ord_MC_eq_zero). - The static form (the hypothesis of [Kol07, Theorem 80 (1)]; Włodarczyk's tangent direction
u ∈ T(I) = D^{μ-1}(I), [Wlo05, Definition 2.7.5]; Bierstone–Milman's sectionz ∈ D^{d-1}_E(I)of maximum order1, [BM08, Corollary 4.1]):His of maximal contact for(I, m)when𝒪_X(−H) ⊆ MC(I), i.e. locallyH = (h = 0)withh ∈ MC(I)(IsMaximalContact). This form is the primary one in the library: the proof of Theorem 92 picks local sectionsx₁, x₁' ∈ MC(I)withH = (x₁ = 0), and the order-reduction functor produces its hypersurfaces in this form; [Kol07, Theorem 80 (1)] (Hironaka/Resolution/Algebraic/MaximalContact/Sequence.lean) shows that a smooth staticHhas the dynamic property. - The dynamic form ([Kol07, Definition 78]):
His a hypersurface of maximal contact when for every openX⁰ ⊆ Xand every smooth blow-up sequence of ordermstarting with(X⁰, I|_{X⁰})(no divisorial partE), the center of every blow-up lies in the birational transform ofH⁰ := H ∩ X⁰(IsDynamicMaximalContact).
Kollár's standing hypothesis "H a smooth hypersurface" is not a clause of either predicate: it
is AlgebraicGeometry.IsSmoothDivisor H ([Kol07, Definition 24]), carried as a hypothesis by the
theorems that use it (Theorem 80, going down), so that the predicates have no smoothness clause
whose locality would have to be proved separately. The mark m is an explicit parameter and
m = max-ord I a hypothesis where used; MC f I 0 = I.
RegularCoords.MC c I m := c.Dpow (m - 1) I (Hironaka/Algebra/Local/MaximalContact.lean) is the
same Definition 79 in coordinates on a regular local ring, not a duplicate: at a stalk the two meet
through stalkIdeal_derivativeIter and derivativeIter_eq_Dpow.
The maximal contact ideal MC(I) := D^{m-1}(I) of I with respect to the mark m
(Kollár: m = max-ord I), the iterated derivative ideal sheaf ([Kol07, Definition 79]).
Equations
Instances For
MC(I) unfolds to D^{m-1}(I) (definitional).
With the mark m + 1, MC(I) = D^m(I) (definitional; m + 1 - 1 = m in ℕ).
The case m = 1: MC(I) = D^0(I) = I.
The static form (the hypothesis of [Kol07, Theorem 80 (1)]; [Wlo05, Definition 2.7.5];
[BM08, Corollary 4.1]): H is of maximal contact for (I, m) when 𝒪_X(−H) ⊆ MC(I), i.e.
locally H = (h = 0) with h ∈ MC(I). Kollár's "smooth hypersurface" is the separate hypothesis
AlgebraicGeometry.IsSmoothDivisor H.
Equations
Instances For
The static form unfolded: 𝒪_X(−H) ⊆ MC(I) as the inclusion of ideal sheaves
H ≤ MC f I m.
The dynamic form ([Kol07, Definition 78]): H is a hypersurface of maximal contact for
(I, m) when, for every open subscheme j : X⁰ ⟶ X and every smooth blow-up sequence of order m
starting with (X⁰, I|_{X⁰}) (with the empty divisorial part, Kollár's "for now we ignore E"),
the center of every blow-up lies in the birational (strict) transform of H⁰ := H|_{X⁰}:
S.strictTransformSeq (H.comap j) i ≤ S.center i as ideal sheaves (V(Z_i) ⊆ V(H_i)). Kollár's
"smooth hypersurface" is the separate hypothesis AlgebraicGeometry.IsSmoothDivisor H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dynamic form unfolded: for every open immersion j : Y ⟶ X and every smooth blow-up
sequence of order m for (Y, I|_Y) with the empty divisor family, every centre lies in the
strict transform of H|_Y.
The order of MC(I) ([Kol07, Lemma 74 (3)]) #
Kollár's "cosupp MC(I) = cosupp (I, m)" ([Kol07, Definition 79]): a point lies on V(MC(I))
iff ord_x I ≥ m (le_ord_iff_mem_support_derivativeIter).
cosupp MC(I) = cosupp (I, m) ([Kol07, Definition 79]).
[Kol07, Lemma 74 (3)] at r = 1: MC(I) has order ≥ 1 at x iff ord_x I ≥ m (the point
lies on V(MC(I))).
[Kol07, Lemma 74 (3)] at r = 2: MC(I) has order ≥ 2 at x iff ord_x I ≥ m + 1; so at
a point of order exactly m the order of MC(I) is exactly 1.
MC(I) has order 1 at a point of order m.
MC(I) has order 0 at a point of order < m.