D(f^*I) = f^*D(I) for a smooth morphism f #
[Kol07, Lemma 74 (4)]: "if f : Y → X is smooth, then D(f^*I) = f^*(D(I))", for X smooth over
the field k. For fX : X ⟶ Spec k smooth, f : Y ⟶ X smooth and an ideal sheaf I on X, the
derivative of the pullback ideal sheaf I.comap f on the k-scheme Y (structure morphism
f ≫ fX) is the pullback of the derivative (Scheme.IdealSheafData.derivative_comap_of_smooth),
and likewise for the iterates (derivativeIter_comap_of_smooth).
The proof is stalkwise: two ideal sheaves with the same stalks agree (ext_stalkIdeal,
Hironaka/Scheme/BlowUp/Descent.lean). At y ∈ Y with x = f y, A = 𝒪_{X,x} → B = 𝒪_{Y,y} the
stalk map: D(I)_x = D(I_x) (stalkIdeal_derivative,
Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean), (I.comap f)_y = I_x B (stalkIdeal_comap,
Hironaka/Scheme/IdealSheaf/StalkIdeal.lean), so both sides are D(I_x B) and D(I_x) B, equal by
the affine-local theorem Ideal.derivative_map_of_formallySmooth of
Hironaka/Algebra/Derivative/Extension.lean: B is formally smooth over A because the stalk maps
of a smooth morphism are formally smooth (Mathlib's smooth locus, formallySmooth_stalkMap), and
Ω_{A/k} is finite projective because A is a localization of a standard smooth k-algebra of
finite type, hence formally smooth over k (formallySmooth_stalk, so Ω is projective) and
essentially of finite type over k (essFiniteType_stalk, so Ω is finite). The k-algebra
structures are those induced by fX and f ≫ fX (stalkAlgebra,
Hironaka/Algebra/RegularSmooth/Stalk.lean), and k → 𝒪_{X,x} → 𝒪_{Y,y} is a scalar tower
(isScalarTower_stalkAlgebra_stalkMap).
Used for the étale equivalence and the restriction of hypersurfaces of maximal contact
(Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquiv.lean,
Hironaka/Resolution/Algebraic/MaximalContact/Restrict.lean,
Hironaka/Resolution/Algebraic/Kol07/MaximalContactGlobalization.lean), for the tuning ideal under
pull-back (Hironaka/Resolution/Algebraic/Tuning/Pullback.lean), for functoriality
(Hironaka/Resolution/Algebraic/BoundaryClearing/FunctorialityPullback.lean) and for the change of
the base field (Hironaka/Scheme/IdealSheaf/Derivative/BaseChange.lean).
The k-algebra structure of 𝒪_{Y,y} induced by f ≫ fX is the one of 𝒪_{X, f y} induced
by fX followed by the stalk map of f.
The scalar tower k → 𝒪_{X, f y} → 𝒪_{Y, y} for the structures induced by fX, f ≫ fX and
the stalk map of f.
The stalk maps of a smooth morphism are formally smooth (every point lies in the smooth
locus, Mathlib's Scheme.Hom.smoothLocus_eq_top), as algebras through the stalk map.
The stalk of a scheme smooth over k is formally smooth over k: it is a localization of a
standard smooth k-algebra (AlgebraicGeometry.exists_affineOpen_isStandardSmooth). This is the
[Smooth fX] form of AlgebraicGeometry.formallySmooth_stalk of
Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean, which assumes SmoothOfRelativeDimension n fX; the hypothesis here is Smooth, so the weaker form is needed.
The stalk of a k-scheme locally of finite type is essentially of finite type over k: a
localization of the finite type k-algebra Γ(X, U) at the prime of x. The
[LocallyOfFiniteType fX] form of AlgebraicGeometry.essFiniteType_stalk of
Hironaka/Scheme/Smooth/DifferentialBasis.lean, which assumes SmoothOfRelativeDimension n fX.
[Kol07, Lemma 74 (4)] ("if f : Y → X is smooth, then D(f^*I) = f^*(D(I))"): for X smooth
over k and f : Y ⟶ X smooth, the derivative of the pullback ideal sheaf on the k-scheme Y
(structure morphism f ≫ fX) is the pullback of the derivative; stalkwise, D(I_x B) = D(I_x) B
for the stalk map A → B.
The iterates: Dʳ(f^*I) = f^*(Dʳ(I)).