Formal equivalence of hypersurfaces of maximal contact at a point #
The first half of [Kol07, Definition 91]. Let X be a smooth variety, p ∈ X a point, I an
ideal sheaf with max-ord I = ord_p I = m, E = E¹ + ⋯ + Eˢ a simple normal crossing divisor and
H, H' ⊂ X two hypersurfaces of maximal contact. Write X̂ := Spec_k Ô_{p,X} for the completion
of X at p ([Kol07, Definition 55]) and Î, Ĥ, Ĥ', Êⁱ for the completions of the ideal
sheaves. Then H and H' are formally equivalent at p with respect to (X, I, E) if there
is an automorphism φ : X̂ → X̂ carrying (X, I, H + E) to (X, I, H' + E) and close to the
identity: (1) φ(Ĥ) = Ĥ', (2) φ^*(Î) = Î, (3) φ(Êⁱ) = Êⁱ for i = 1, …, s, and
(4) h − φ^*(h) ∈ \widehat{MC(I)} for every h ∈ Ô_{p,X}.
- The completed ideal ([Kol07, Definition 55]):
Ô_{X,p}is the maximal-adic completionAdicCompletion (maximalIdeal 𝒪_{X,p}) 𝒪_{X,p}of the stalk, and Kollár'sĴis the extensionJ_p Ô_{X,p}of the stalkJ_p(stalkIdeal) along𝒪_{X,p} → Ô_{X,p}(completionIdeal); it is the completion of the moduleJ_p(range_adicCompletion_map_subtype), and the extension reflects inclusions (map_adicCompletion_le_iff; herecompletionIdeal_le_iff, the Krull-intersection remark of Definition 55). - Formal equivalence (the conditions (91.1)–(91.4); throughout
Hironaka/Resolution/Algebraic/MaximalContact/, (91.k) abbreviates condition (k) of Kol07, Definition 91 and (91.k′) its étale counterpart (k′), the shorthand Kollár himself uses once, in [Kol07, 95]): the automorphismφofX̂ = Spec_k Ô_{p,X}is ak-algebra automorphismφ^*ofÔ_{p,X}, for thek-structuref.stalkAlgebra pof the stalk extended to the completion. Read on functions, (1) isφ^*(Ĥ') = Ĥ: the closed subschemeĤ = V(Ĥ)is carried ontoĤ' = V(Ĥ')exactly when the pull-back of the equations ofĤ'generates the ideal ofĤ(withx₁' ↦ x₁in the proof of Theorem 92:φ^*(x₁') = x₁); (2) and (3) areφ^*(Î) = Îandφ^*(Êⁱ) = Êⁱ; (4) is the displayed membership, for the maximal contact idealMC f I mcompleted atp(FormallyEquivalentAt). MCcommutes with completion (Kollár's remark after Definition 91 that\widehat{MC(I)} = MC(Î)because derivatives commute with completion, [Kol07, Lemma 74 (5)]): for coordinatescon the stalk that arek-linear and span thek-derivations, the maximal contact ideal ofÎcomputed with the completed coordinate derivations∂̂ᵢ(Kollár'sDonÔ_{p,X} ≅ K⟦x₁, …, xₙ⟧is the ideal generated by the∂/∂xᵢ-derivatives, [Kol07, Definition 73]) is the completion of the stalk of the sheafMC(I)(adicCompletion_MC_completionIdeal). Proof: the stalk ofDʳ(I)is the coordinateDʳof the stalk (stalkIdeal_derivativeIter,derivativeIter_eq_Dpow; here the stalk bridgestalkIdeal_MC), andDʳpasses across the extension of ideals toR̂(Dpow_adicCompletion). So condition (4) may be read with either side.
Kollár's standing hypotheses of Definition 91 (X smooth over k, p a closed point with
max-ord I = ord_p I = m, E simple normal crossing, H, H' hypersurfaces of maximal contact in
the static form with AlgebraicGeometry.IsSmoothDivisor) are not clauses of the predicate: as for
MC and IsMaximalContact they are hypotheses of the theorems that use it (the formal half of
Theorem 92, Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivExists.lean; the passage from
étale to formal equivalence, Hironaka/Resolution/Algebraic/MaximalContact/EtaleToFormal.lean). The
mark m is an explicit parameter.
The completed ideal Ĵ ⊆ Ô_{X,p} #
The completion of an ideal sheaf at a point (the Î, Ĥ, Êⁱ of [Kol07, Definition 91],
with the completion of [Kol07, Definition 55]): the extension J_p Ô_{X,p} of the stalk J_p
along the canonical map 𝒪_{X,p} → Ô_{X,p} into the maximal-adic completion of the stalk. It is
also the completion of the module J_p.
Equations
- J.completionIdeal p = Ideal.map (algebraMap (↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))) (J.stalkIdeal p)
Instances For
completionIdeal unfolded.
Krull's intersection theorem in the form of [Kol07, Definition 55] (equal completions of two subschemes at a point give equal subschemes near it): on a locally Noetherian scheme the completed ideals compare exactly as the stalks do.
Formal equivalence at a point #
The conditions (91.1)–(91.4) of [Kol07, Definition 91]: H and H' are formally equivalent
at p with respect to (X, I, E), for the mark m, if there is a k-algebra automorphism
φ^* of Ô_{p,X} (an automorphism φ of X̂ = Spec_k Ô_{p,X}) with
(1) φ(Ĥ) = Ĥ', i.e. φ^*(Ĥ') = Ĥ; (2) φ^*(Î) = Î; (3) φ^*(Êⁱ) = Êⁱ for every component
Eⁱ of E; (4) h − φ^*(h) ∈ \widehat{MC(I)} for every h ∈ Ô_{p,X} ("φ is close to the
identity": it is the identity on the closed subscheme V(\widehat{MC(I)})). The k-structure of
Ô_{p,X} is the one induced by f on the stalk (Scheme.Hom.stalkAlgebra) and extended to the
completion. Kollár's standing hypotheses (p closed, max-ord I = ord_p I = m, E snc, H, H'
of maximal contact) are hypotheses of the theorems that use the predicate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The definition unfolded.
MC commutes with completion ([Kol07, Lemma 74 (5)] iterated) #
The stalk bridge for the maximal contact ideal: the sheaf MC f I m and RegularCoords.MC
are the same [Kol07, Definition 79] read at a stalk. For coordinates c on 𝒪_{X,p} that are
k-linear and span the k-derivations, (MC f I m)_p = MC_c((I_p), m), through
stalkIdeal_derivativeIter and derivativeIter_eq_Dpow.
Kollár's remark after [Kol07, Definition 91] that \widehat{MC(I)} = MC(Î), since derivatives
commute with completion ([Kol07, Lemma 74 (5)] iterated): for coordinates c on the stalk
𝒪_{X,p} that are k-linear and span the k-derivations, the maximal contact ideal of Î
computed with the completed coordinate derivations ∂̂ᵢ (Kollár's D on Ô_{p,X} ≅ K⟦x⟧,
[Kol07, Definition 73]) is the completion of the stalk of MC(I). Condition (91.4) may therefore
be read with either side.