Maximal contact under restriction to open subschemes

Kollár's proof of [Kol07, Theorem 80 (1)] opens with the remark that being a hypersurface of maximal contact is a local question, so that one may assume L = 𝒪_X, and [Kol07, Definition 78] quantifies over every open X⁰ ⊆ X with the restricted data (X⁰, I|_{X⁰}) and H⁰ = H ∩ X⁰. This file supplies the two restriction facts those steps use.

• The maximal contact ideal restricts ([Kol07, Lemma 74 (4)]): for a smooth g : Y ⟶ X, in particular an open immersion, MC(g^* I) = g^*(MC(I)), because derivatives commute with smooth pull-back (derivativeIter_comap_of_smooth); hence the static form 𝒪_X(−H) ⊆ MC(I) restricts to g^*: 𝒪_Y(−g^*H) ⊆ MC(g^* I) (IsMaximalContact.comap).
• A smooth hypersurface restricts to a smooth hypersurface of an open subscheme (Kollár's tacit H⁰ := H ∩ X⁰): the closed subscheme of g^* H is an open subscheme of that of H (isOpenImmersion_subschemeMap_of_comap), so its stalks are regular; and the stalk of g^* H at y is the image of the stalk of H at g y under the isomorphism of stalks of an open immersion, whose generator still has order one, since the order of an ideal sheaf is invariant under open immersions (ord_comap_of_isOpenImmersion) and an element of a regular local ring has order one exactly when it lies in 𝔪 ∖ 𝔪² (ordElem_eq_one_iff).
• The static form is local: 𝒪_X(−H) ⊆ MC(I) holds iff it holds on the members of an open cover; (⇒) by restriction, (⇐) because an inclusion of ideal sheaves descends along a jointly surjective family of open immersions (le_of_comap_le_of_forall_exists), MC commuting with the restrictions. This is the precise content of the reduction to L = 𝒪_X: a section h ∈ H⁰(X, L ⊗ MC(I)) with zero divisor H is the inclusion 𝒪_X(−H) ⊆ MC(I) on every open trivializing L, and the inclusion glues.

These facts are used throughout Hironaka/Resolution/Algebraic/MaximalContact/ (the local existence, the transform of a hypersurface through the centre, going down) and in Hironaka/Resolution/Algebraic/Snc/SmoothDivisorLocal.lean.

theorem AlgebraicGeometry.Scheme.IdealSheafData.MC_comap_of_smooth {k : Type u} [Field k] {X Y : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (g : Y ⟶ X) [Smooth g] (I : X.IdealSheafData) (m : ℕ) : MC (CategoryTheory.CategoryStruct.comp g f) (I.comap g) m = (MC f I m).comap g

[Kol07, Lemma 74 (4)] iterated: the maximal contact ideal commutes with smooth pull-back, in particular with restriction to an open subscheme.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact.comap {k : Type u} [Field k] {X Y : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I H : X.IdealSheafData} {m : ℕ} (h : IsMaximalContact f I m H) (g : Y ⟶ X) [Smooth g] : IsMaximalContact (CategoryTheory.CategoryStruct.comp g f) (I.comap g) m (H.comap g)

The static form 𝒪_X(−H) ⊆ MC(I) restricts along every smooth g, in particular to every open subscheme, as the restricted data of [Kol07, Definition 78] require.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isMaximalContact_iff_forall_opens {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m : ℕ) (H : X.IdealSheafData) {ι : Type u_1} (U : ι → X.Opens) (hU : iSup U = ⊤) : IsMaximalContact f I m H ↔ ∀ (α : ι), IsMaximalContact (CategoryTheory.CategoryStruct.comp (U α).ι f) (I.comap (U α).ι) m (H.comap (U α).ι)

The reduction "we may assume that L = 𝒪_X" opening the proof of [Kol07, Theorem 80]: the static form is local, 𝒪_X(−H) ⊆ MC(I) iff it holds on every member of an open cover. (⇒) is IsMaximalContact.comap; (⇐) descends the inclusion along the covering open immersions (le_of_comap_le_of_forall_exists), MC commuting with them.

theorem AlgebraicGeometry.IsSmoothDivisor.comap_of_isOpenImmersion {X Y : Scheme} {H : X.IdealSheafData} (hH : IsSmoothDivisor H) (g : Y ⟶ X) [IsOpenImmersion g] : IsSmoothDivisor (H.comap g)

Kollár's H⁰ := H ∩ X⁰ in [Kol07, Definition 78]: a smooth hypersurface restricts to a smooth hypersurface of every open subscheme. The closed subscheme of the restriction is an open subscheme of V(H), hence regular; the stalk at y is the isomorphic image of the stalk at g y, and its generator has order one because the order is invariant under open immersions.