Invariance of the order under open immersions, isomorphisms and completion

[Hau03, Appendix A]: the order "is invariant with respect to field extensions, passage to the completion and local isomorphisms". This module: ord is invariant under isomorphisms, under restriction to opens, and under completion; smooth morphisms are Hironaka/Scheme/IdealSheaf/Order/Smooth.lean.

• Open immersions and isomorphisms (ord_comap_of_isOpenImmersion, ord_comap_of_isIso, ord_comap_ι): the stalk of the inverse image f⁻¹ I at y is the image of the stalk I_{f y} under the stalk map (stalkIdeal_comap, Hironaka/Scheme/IdealSheaf/StalkIdeal.lean), which is an isomorphism of local rings for an open immersion, and the order of an ideal is transported along ring isomorphisms (IsLocalRing.ord_map_ringEquiv, Hironaka/Algebra/Local/TransformOrder.lean).
• Completion (ord_eq_ord_map_adicCompletion): ord_x I = ord (I_x Ô_{X,x}) in the maximal-adic completion of the Noetherian local ring 𝒪_{X,x} (ord_map_adicCompletion of Hironaka/Algebra/Local/CompletionCoords.lean: 𝔪̂ʳ ∩ 𝒪 = 𝔪ʳ by Krull's intersection theorem, which [Kol07, 55] recalls from [AM69, 10.17]).

The maximal order is invariant under isomorphisms as well (maxOrd_comap_of_isIso, in the namespace of its user Hironaka/Resolution/Algebraic/Hir64/OrderReductionRound.lean).

Used for the transport of orders along open covers and isomorphisms (Hironaka/Scheme/BlowUpSequence/OpenTransport.lean, Hironaka/Resolution/Algebraic/Kol07/CosuppTransport.lean, Hironaka/Scheme/BlowUpSequence/DisjointUnion.lean, Hironaka/Resolution/Algebraic/Kol07/MaximalContactGlobalization.lean, Hironaka/Resolution/Algebraic/MaximalContact/Existence.lean, Hironaka/Resolution/Algebraic/MaximalContact/Restrict.lean, Hironaka/Resolution/Algebraic/BoundaryClearing/Transform.lean).

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

The order is invariant under open immersions, ord_y (f⁻¹ I) = ord_{f y} I ("local isomorphisms", [Hau03, Appendix A]).

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

The order is invariant under isomorphisms.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_comap_ι {X : Scheme} (I : X.IdealSheafData) (U : X.Opens) (u : ↥U) : (I.comap U.ι).ord u = I.ord (U.ι u)

The order is invariant under restriction to an open U ⊆ X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_eq_ord_map_adicCompletion {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] (x : ↥X) : I.ord x = IsLocalRing.ord (Ideal.map (algebraMap (↑(X.presheaf.stalk x)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)) ↑(X.presheaf.stalk x))) (I.stalkIdeal x))

"Passage to the completion" ([Hau03, Appendix A]): ord_x I = ord (I_x Ô_{X,x}) in the maximal-adic completion of 𝒪_{X,x}, since 𝔪̂ʳ ∩ 𝒪 = 𝔪ʳ by Krull's intersection theorem (ord_map_adicCompletion).

max-ord under an isomorphism

theorem AlgebraicGeometry.maxOrd_comap_of_isIso {X Y : Scheme} (I : X.IdealSheafData) (f : Y ⟶ X) [CategoryTheory.IsIso f] : (I.comap f).maxOrd = I.maxOrd

max-ord is invariant under the inverse image along an isomorphism (ord_comap_of_isIso pointwise); in the namespace of its user Hironaka/Resolution/Algebraic/Hir64/OrderReductionRound.lean.