Documentation

Hironaka.Resolution.Algebraic.MaximalContact.Theorem92

Theorem 92: uniqueness of maximal contact up to étale equivalence #

[Kol07, Theorem 92]: for X a smooth variety over a field of characteristic zero, I an MC-invariant ideal sheaf, m = max-ord I, E a simple normal crossing divisor and H, H' ⊂ X two smooth hypersurfaces of maximal contact for I such that H + E and H' + E both have simple normal crossings, H and H' are étale equivalent with respect to (X, I, E). The proof is [Kol07, 95]: at every closed point p of the cosupport cosupp(I, m),

  1. exists_coordinates (Hironaka/Resolution/Algebraic/MaximalContact/Coordinates.lean) chooses coordinates x₁, x₁' ∈ MC(I) with H = (x₁ = 0), H' = (x₁' = 0) and a common complement y = (x₂, …, xₙ) adapted to E; n = d + 1 is the relative dimension;
  2. exists_etaleCoordinates_pair (Hironaka/Scheme/Smooth/CoordinateSystemPair.lean) spreads the two regular systems (x₁, y), (x₁', y) out to étale coordinate maps c, c' : U → 𝔸ⁿ_k on an affine U ∋ p;
  3. the graph U₁(p) = U ×_{𝔸ⁿ} U at the diagonal point (p, p) is an étale neighbourhood pair over k with the graph equations and trivial action on κ(p) (exists_etaleNbhdPair_of_etaleCoordinates, Hironaka/Scheme/Smooth/GraphDiagonalPair.lean);
  4. its automorphism satisfies (91.1)–(91.4): the completion of U₁(p) at (p, p) is the graph of the formal automorphism φₚ (Hironaka/Resolution/Algebraic/MaximalContact/GraphOfAutomorphism.lean);
  5. the conditions (1′)–(4′) of étale equivalence hold on an open U(p) ∋ (p, p) (exists_opens_conditions_of_formalAutomorphism, Hironaka/Resolution/Algebraic/MaximalContact/EtaleNbhdConditions.lean);

and the disjoint union of the U(p) is the étale equivalence (nonempty_etaleEquiv_of_forall_isClosed, Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivSigma.lean). The output is EtaleEquiv f I m E H H', [Kol07, Definition 91] in the form where the images of ψ, ψ' contain the cosupport (Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquiv.lean, Conventions).

Conventions. Kollár's hypotheses that E is simple normal crossing and that H, H' are smooth are not stated separately, since they follow from H + E and H' + E being simple normal crossing; m = max-ord I is weakened to m ≥ 1. The affine form of the theorem (Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivAffine.lean) is what the independence of the order-reduction functor from the hypersurface (Hironaka/Resolution/Algebraic/MaximalContact/FunctorIndependence.lean) uses.

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_etaleNbhdPair_conditions {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) (hI : IsMCInvariant f I m) (E : X.DivisorFamily) (H H' : X.IdealSheafData) (hH : IsMaximalContact f I m H) (hH' : IsMaximalContact f I m H') (hHE : (E.append H).IsSnc) (hH'E : (E.append H').IsSnc) (p : ↥X) (hpc : IsClosed {p}) (hp : ↑m ≤ I.ord p) :
∃ (Q : EtaleNbhdPair X p) (V : Q.W.Opens), Q.q ∈ V ∧ CategoryTheory.CategoryStruct.comp Q.ψ f = CategoryTheory.CategoryStruct.comp Q.ψ' f ∧ H.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = H'.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') ∧ (∀ (i : E.ι), (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) = (E.component i).comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ')) ∧ AgreeOn (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) (CategoryTheory.CategoryStruct.comp V.ι Q.ψ') (MC (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp V.ι Q.ψ) f) (I.comap (CategoryTheory.CategoryStruct.comp V.ι Q.ψ)) m)

The étale neighbourhood of one closed point of the cosupport ([Kol07, 95]): for a closed point p ∈ cosupp(I, m) there is an étale neighbourhood pair Q of p over k and an open V ∋ q on which the conditions (1′)–(4′) hold; steps 1–5 of the module docstring assembled.

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.etaleEquiv_of_isMCInvariant {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) (hI : IsMCInvariant f I m) (E : X.DivisorFamily) (H H' : X.IdealSheafData) (hH : IsMaximalContact f I m H) (hH' : IsMaximalContact f I m H') (hHE : (E.append H).IsSnc) (hH'E : (E.append H').IsSnc) :
Nonempty (EtaleEquiv f I m E H H')

[Kol07, Theorem 92] (proof: [Kol07, 95]): for X smooth over k of characteristic zero, I MC-invariant, m ≥ 1, and H, H' hypersurfaces of maximal contact for I with H + E, H' + E simple normal crossing, H and H' are étale equivalent with respect to (X, I, E) (EtaleEquiv, [Kol07, Definition 91] in the form where the images of ψ, ψ' contain the cosupport). The module docstring says which hypotheses of the printed statement are implied or weakened.