Hypersurfaces of maximal contact under smooth pull-back

The remark closing [Kol07, Theorem 103, Step 2.3], that "the functoriality package is local" (with [Kol07, 34.1]): for a smooth h : Y → X, h⁻¹(H) is a smooth hypersurface of maximal contact for h^*I. The maximal contact comes from MC(h^*I) = h^*MC(I) ([Kol07, Lemma 74 (4)], MC_comap_of_smooth), and the smooth divisor pulls back to a smooth divisor: the one-member family (∅, H) is simple normal crossing, its inverse image is simple normal crossing (isSnc_comap_of_smooth), and the members of a simple normal crossing family are smooth divisors (isSmoothDivisor_of_snc_data).

Both statements are used in Step 3 of the proof of [Kol07, Theorem 103], the globalization (Hironaka/Resolution/Algebraic/OrderReduction/Step3Globalization.lean, Step3Clauses.lean, Step3Cover.lean), where the functor is pulled back along smooth morphisms.

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

The inverse image of a hypersurface of maximal contact (in the static sense of [Kol07, Theorem 80 (1)]) under a smooth morphism is one for the pulled-back ideal, since MC commutes with smooth pull-back ([Kol07, Lemma 74 (4)]).

theorem Hironaka.Snc.isSmoothDivisor_comap_of_smooth {k : Type u} [Field k] {X Y : AlgebraicGeometry.Scheme} [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) : AlgebraicGeometry.IsSmoothDivisor (H.comap h)

The inverse image of a smooth divisor under a smooth morphism of smooth k-schemes is a smooth divisor.