The colon by a finitely generated ideal commutes with flat base change

Włodarczyk's resolution commutes with smooth morphisms [Wlo05, Theorem 1.0.2 (d)], the functoriality proved in [Wlo05, §4.1]. The embedded resolution of Hironaka.Resolution.Algebraic.Wlo05.Embedded replaces, at each step, the ideal I by the colon (I : I_Γ) by the reduced, finitely generated, in general not invertible, ideal I_Γ of the union of the strict transforms of the components already contained in a centre (isolatedTriple). Transporting the construction along a smooth morphism h therefore needs the colon to commute with the pull-back along h: (I : K).comap h = (I.comap h : K.comap h). The lemma colon_comap_of_flat of Hironaka.Scheme.BlowUpSequence.PullbackInduced proves this for an invertible K (a principal stalk); this module proves it for every ideal sheaf on a locally Noetherian scheme (every K is coherent, hence finitely generated on affines and on stalks). It is used by the pull-back of the embedded resolution along smooth morphisms (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedPullback).

The algebra is [Mat89, Theorem 7.4 (iii)]: for a flat R-algebra S and a finitely generated J = (j_1, …, j_r), (I : J) S = (I S : J S). The colon by J is the intersection of the colons by the j_i (Ideal.colon_span, Submodule.colon_iUnion), each of which commutes with flat base change (map_colon_singleton_of_flat of Hironaka.Scheme.BlowUpSequence.PullbackInduced), and a finite intersection commutes with flat base change (Ideal.map_inf_of_flat below, by the equational criterion for flatness [TSPA, Tag 00HK]: an element of I S ∩ J S has two expressions whose difference is a trivial relation).

Main declarations

• Ideal.map_inf_of_flat: (I ⊓ J) S = I S ⊓ J S for flat S.
• Ideal.map_colon_of_fg_of_flat: (I : J) S = (I S : J S) for flat S and finitely generated J.
• stalkIdeal_colon_of_isLocallyNoetherian: the stalk of a colon is the colon of the stalks.
• colon_comap_of_flat_of_isLocallyNoetherian: the colon commutes with flat pull-back.

theorem Ideal.map_inf_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] (I J : Ideal R) : map (algebraMap R S) (I ⊓ J) = map (algebraMap R S) I ⊓ map (algebraMap R S) J

The equational criterion for flatness [TSPA, Tag 00HK], read on an element of I S ∩ J S: a finite intersection of ideals commutes with flat base change. Given x = Σ φ(a_i) s_i = Σ φ(b_j) t_j with a_i ∈ I, b_j ∈ J, the relation Σ φ(a_i) s_i − Σ φ(b_j) t_j = 0 is trivial, s_i = Σ_l c_{il} y_l, t_j = Σ_l d_{jl} y_l with Σ_i a_i c_{il} = Σ_j b_j d_{jl} for every l; the common value e_l lies in I ⊓ J and x = Σ_l φ(e_l) y_l.

theorem Ideal.map_finset_inf_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] {ι : Type u_1} (s : Finset ι) (I : ι → Ideal R) : map (algebraMap R S) (s.inf I) = s.inf fun (i : ι) => map (algebraMap R S) (I i)

A finite infimum of ideals commutes with flat base change.

theorem Ideal.colon_span_finset {T : Type u_1} [CommRing T] (K : Ideal T) (t : Finset T) : Submodule.colon K ↑(span ↑t) = t.inf fun (x : T) => Submodule.colon K {x}

The colon by the span of a finite set is the finite infimum of the colons by its elements (Ideal.colon_span, Submodule.colon_iUnion).

theorem Ideal.map_colon_of_fg_of_flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] (I J : Ideal R) (hJ : J.FG) : map (algebraMap R S) (Submodule.colon I ↑J) = Submodule.colon (map (algebraMap R S) I) ↑(map (algebraMap R S) J)

The colon by a finitely generated ideal commutes with flat base change, (I : J) S = (I S : J S) [Mat89, Theorem 7.4 (iii)].

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_colon_of_isLocallyNoetherian {X : Scheme} [IsLocallyNoetherian X] (I K : X.IdealSheafData) (x : ↥X) : (I.colon K).stalkIdeal x = Submodule.colon (I.stalkIdeal x) ↑(K.stalkIdeal x)

On a locally Noetherian scheme every ideal sheaf is finitely generated on affine opens, so the stalk of a colon is the colon of the stalks (ideal_colon_of_fg of Hironaka.Scheme.BlowUp.Transform, the colon commuting with localization for a finitely generated divisor).

theorem AlgebraicGeometry.Scheme.IdealSheafData.colon_comap_of_flat_of_isLocallyNoetherian {X Y : Scheme} (h : Y ⟶ X) [Flat h] [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (J K : X.IdealSheafData) : (J.colon K).comap h = (J.comap h).colon (K.comap h)

On locally Noetherian schemes the colon commutes with flat pull-back, (J : K).comap h = (J.comap h : K.comap h) ([Mat89, Theorem 7.4 (iii)] on stalks): the lemma colon_comap_of_flat of Hironaka.Scheme.BlowUpSequence.PullbackInduced without the invertibility of K.