Invariance of the order under smooth morphisms

[Hau03, Appendix A]: the order is invariant "more generally, with respect to smooth morphisms". For f : Y → X smooth, ord_y (f⁻¹ I) = ord_{f y} I (ord_comap_of_smooth), and the local statement ord (J 𝒪_{Y,y}) = ord J for every ideal J of 𝒪_{X, f y} (ord_map_stalkMap_of_smooth).

The stalk of f⁻¹ I at y is the image of I_{f y} under the stalk map (stalkIdeal_comap, Hironaka/Scheme/IdealSheaf/StalkIdeal.lean), and the order does not drop under a local map (ord_le_ord_map, Hironaka/Algebra/Local/Order.lean); the reverse inequality is the content. On affine opens f y ∈ U ⊆ X, y ∈ V ⊆ f⁻¹U, the stalk map is the localization Γ(U)_p → Γ(V)_q of the smooth ring map Γ(U) → Γ(V) at the primes of y and f y (Mathlib's IsAffineOpen.arrowStalkMapIso), which reflects the powers of the maximal ideal by the local statement of Hironaka/Algebra/Local/OrderSmooth.lean (ordFaithful_localRingHom_of_isSmoothAt: the polynomial case and the étale case); OrdFaithful transports along isomorphisms of arrows (OrdFaithful.of_arrow_iso). Hauser lists the invariance among the functorial properties of the order; the argument here is the library's own.

Used for the pull-back of the resolution data along smooth morphisms (Hironaka/Scheme/BlowUpSequence/PullbackInduced.lean, Hironaka/Scheme/BlowUpSequence/PullbackSnc.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/Parameters.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothLoop.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/UpToUnits.lean).

theorem IsLocalRing.OrdFaithful.of_arrow_iso {A B A' B' : CommRingCat} [IsLocalRing ↑A] [IsLocalRing ↑B] [IsLocalRing ↑A'] [IsLocalRing ↑B'] {φ : A ⟶ B} {ψ : A' ⟶ B'} (i : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk ψ) (h : OrdFaithful (CommRingCat.Hom.hom φ)) : OrdFaithful (CommRingCat.Hom.hom ψ)

OrdFaithful transports along an isomorphism of arrows of commutative rings: if ψ = e₂ ∘ φ ∘ e₁⁻¹ for ring isomorphisms e₁, e₂, then ψ reflects the powers of the maximal ideal when φ does.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_map_stalkMap_of_smooth {X Y : Scheme} (f : Y ⟶ X) [Smooth f] (y : ↥Y) (J : Ideal ↑(X.presheaf.stalk (f y))) : IsLocalRing.ord (Ideal.map (CommRingCat.Hom.hom (Hom.stalkMap f y)) J) = IsLocalRing.ord J

The local statement: the stalk map of a smooth morphism preserves the order of every ideal of the local ring 𝒪_{X, f y}. On affine opens f y ∈ U, y ∈ V ⊆ f⁻¹U, the stalk map is the localization of the smooth ring map Γ(U) → Γ(V) at the primes of y and f y (Mathlib's IsAffineOpen.arrowStalkMapIso), which reflects the powers of the maximal ideal (ordFaithful_localRingHom_of_isSmoothAt).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_comap_of_smooth {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) [Smooth f] (y : ↥Y) : (I.comap f).ord y = I.ord (f y)

[Hau03, Appendix A], invariant "more generally, with respect to smooth morphisms": pullback along a smooth morphism preserves the order, ord_y (f⁻¹ I) = ord_{f y} I.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_comap_of_etale {X : Scheme} (I : X.IdealSheafData) {Y : Scheme} (f : Y ⟶ X) [Etale f] (y : ↥Y) : (I.comap f).ord y = I.ord (f y)

Pullback along an étale morphism preserves the order.