Smooth divisors

[Kol07, Definition 24] ("each E^i is smooth") and [Hau14, Definition 4.1] (a hypersurface): a smooth divisor of a scheme X smooth over k is a closed subscheme D ⊆ X, smooth over k, whose ideal is generated at every point x ∈ D by one element of 𝔪_x ∖ 𝔪_x². "Smooth over k" is taken as regularity of the closed subscheme (IsRegular; the two agree over a perfect field, Hironaka.Algebra.RegularSmooth.RegularSmoothEquiv), and the ideal of D at x is the stalk D.stalkIdeal x of the ideal sheaf. The equivalence with "V(D) is smooth of relative dimension n − 1" is isSmoothDivisor_of_smoothOfRelativeDimension here and smoothOfRelativeDimension_of_isSmoothDivisor of Hironaka.Scheme.Snc.RelativeDimension. The members of a simple normal crossing family are smooth divisors (Hironaka.Scheme.Snc.Family), and a hypersurface of maximal contact is required to be one (Hironaka.Resolution.Algebraic.MaximalContact.Basic).

def AlgebraicGeometry.IsSmoothDivisor {X : Scheme} (D : X.IdealSheafData) : Prop

D is a smooth divisor of X ([Kol07, Definition 24], "each E^i is smooth"; [Hau14, Definition 4.1]): the closed subscheme V(D) is regular (smooth over the perfect ground field) and at every point x of V(D) the stalk D_x ⊆ 𝒪_{X,x} is generated by one element of 𝔪_x ∖ 𝔪_x².

Equations

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

theorem AlgebraicGeometry.isSmoothDivisor_of_smoothOfRelativeDimension {X : Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (hn : 1 ≤ n) (D : X.IdealSheafData) [SmoothOfRelativeDimension (n - 1) (CategoryTheory.CategoryStruct.comp D.subschemeι f)] : IsSmoothDivisor D

If V(D) is smooth of relative dimension n − 1 over the perfect field k, X being smooth of relative dimension n ≥ 1, then D is a smooth divisor: V(D) is regular, and at x ∈ V(D) the adapted parameters of Hironaka.Scheme.Smooth.AdaptedCoordinates give D_x = (y_0) with y_0 a member of a regular system of parameters, hence in 𝔪_x ∖ 𝔪_x² ([TSPA, Tag 00NR]).