Simple normal crossings along a hypersurface: the lifting direction

The proof of [Kol07, Corollary 85]: adding E to (X, I) and E|_H to (H, I|_H, m) "poses the same restriction on order reduction" — a centre Z ⊆ H has simple normal crossings with E in X iff it has simple normal crossings with H + E in X iff Z|_H has simple normal crossings with E|_H in H. The restriction direction, from X to H, is hasSncWith_comap_of_isClosedImmersion of Hironaka.Scheme.Snc.RestrictHypersurface; the passage from E to H + E is hasSncWith_append_of_le of Hironaka.Scheme.BlowUpSequence.RestrictDivisors. This module proves the two remaining directions and the two equivalences, which Hironaka.Resolution.Algebraic.Kol07.GoingUp uses to pass between the snc clause of a sequence on X and that of its restriction to H.

• hasSncWith_append_of_comap_of_isClosedImmersion — the lifting direction, for any closed immersion g : Y ↪ X with H := g.ker and regular stalks on X: adapted coordinates on H lift along the surjection φ : 𝒪_{X,x} → 𝒪_{X,x}/(h) = 𝒪_{H,y} (ker_stalkMap_of_isClosedImmersion). Given a regular system of parameters z' of 𝒪_{H,y} adapted to E|_H with Z|_H = (z'_t : t ∈ s'), and a regular system w of 𝒪_{X,x} adapted to H + E (from (E.append H).IsSnc) with h = w_{h₀} the equation of H: the components E^i through x are principal, E^i_x = (a_i), and (φ a_i) = (z'_{c'(i)}) in the domain 𝒪_{H,y}, so z'_{c'(i)} = φ a_i · u_i for a unit u_i, which lifts to a unit v_i of 𝒪_{X,x}; the lifted coordinates are ℓ_{c'(i)} := a_i v_i at the E-indices and arbitrary preimages of the z'_t elsewhere (Function.extend), and the new system is z := (h, ℓ). It is a regular system of parameters (𝔪_X = (h) + (ℓ) because φ(𝔪_X) = 𝔪_H = (φ ℓ); n' + 1 = dim 𝒪_{X,x} because dim 𝒪_{H,y} = dim 𝒪_{X,x} − 1, natCast_sub_card_eq_ringKrullDim_of_ker of Hironaka.Scheme.Snc.ParameterSubset), adapted to H + E (H_x = (h), E^i_x = (a_i) = (a_i v_i)), and Z_x = (h) + (ℓ_t : t ∈ s') because φ(Z_x) = (Z|_H)_y = (z'_t : t ∈ s') and (h) ⊆ Z_x.
• HasSncWith.of_append — the sub-family direction (from H + E to E): the same coordinates with the index map restricted to the members of E.
• hasSncWith_iff_hasSncWith_append, hasSncWith_append_iff_hasSncWith_comap — the two equivalences on a smooth X, from the four directions.

theorem AlgebraicGeometry.HasSncWith.of_append {X : Scheme} {E : X.DivisorFamily} {J Z : X.IdealSheafData} (h : (E.append J).HasSncWith Z) : E.HasSncWith Z

Simple normal crossings with E + J implies simple normal crossings with the sub-family E — the same adapted coordinates, the index map restricted to the members of E (the proof of [Kol07, Corollary 85]).

theorem AlgebraicGeometry.exists_eq_of_mem_support_ker {X Y : Scheme} (g : Y ⟶ X) [IsClosedImmersion g] {x : ↥X} (hx : x ∈ (Scheme.Hom.ker g).support) : ∃ (y : ↥Y), g y = x

A point of the closed subscheme V(ker g) of a closed immersion g lies in the image of g (the image is closed, so Mathlib's support_ker needs no closure).

theorem AlgebraicGeometry.hasSncWith_append_of_comap_of_isClosedImmersion {X Y : Scheme} (g : Y ⟶ X) [IsClosedImmersion g] (hreg : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) {E : X.DivisorFamily} {Z : X.IdealSheafData} (hEH : (E.append (Scheme.Hom.ker g)).IsSnc) (hle : Scheme.Hom.ker g ≤ Z) (hZ : (E.comap g).HasSncWith (Z.comap g)) : (E.append (Scheme.Hom.ker g)).HasSncWith Z

The lifting direction of the proof of [Kol07, Corollary 85] ([Kol07, Definition 24]): for a closed immersion g : Y ↪ X with H := g.ker, if H + E has simple normal crossings, H ≤ Z and Z|_H has simple normal crossings with E|_H in H, then Z has simple normal crossings with H + E in X. Adapted coordinates on H lift along 𝒪_{X,x} → 𝒪_{X,x}/(h) to adapted coordinates on X with h as the extra parameter; see the module docstring.

theorem AlgebraicGeometry.hasSncWith_iff_hasSncWith_append {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [Smooth f] {E : X.DivisorFamily} {H Z : X.IdealSheafData} (hE : (E.append H).IsSnc) (hle : H ≤ Z) : E.HasSncWith Z ↔ (E.append H).HasSncWith Z

The first equivalence of the proof of [Kol07, Corollary 85]: for Z ⊆ H on a smooth X with H + E snc, Z has simple normal crossings with E iff it has simple normal crossings with H + E — hasSncWith_append_of_le and HasSncWith.of_append.

theorem AlgebraicGeometry.hasSncWith_append_iff_hasSncWith_comap {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [Smooth f] {E : X.DivisorFamily} {H Z : X.IdealSheafData} (hE : (E.append H).IsSnc) (hle : H ≤ Z) : (E.append H).HasSncWith Z ↔ (E.comap H.subschemeι).HasSncWith (Z.comap H.subschemeι)

The second equivalence of the proof of [Kol07, Corollary 85]: for Z ⊆ H on a smooth X with H + E snc, Z has simple normal crossings with H + E in X iff Z|_H has simple normal crossings with E|_H in H — hasSncWith_comap_of_isClosedImmersion and the lifting direction hasSncWith_append_of_comap_of_isClosedImmersion, along H.subschemeι whose kernel is H.