Colon ideals of comaximal ideal sheaves

Ideal sheaves with disjoint supports are comaximal (sup_eq_top_of_disjoint_support), the product of comaximal ideal sheaves is their intersection (mul_eq_inf_of_sup_eq_top), and the colon of the product by one factor is the other (colon_mul_left_of_sup_eq_top: (I · J) : I = J when I + J = 𝒪, since x · I ⊆ I · J ⊆ J and x = x·a + x·b for 1 = a + b). Everything is proved sectionwise on the affine opens, through ideal_sup, ideal_mul, le_def and the colon (le_colon_iff_mul_le, colon_mul_le).

These are the tools for the products of pairwise disjoint components (Hironaka.Resolution.Algebraic.Wlo05.ComponentsColon) in Włodarczyk's embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.Embedded): when the loop isolates the strict transforms of some components of Y before any blow-up, the ideal of the remaining components is the colon of the ideal of Y by the ideal of the isolated ones, the two being comaximal because the components of a smooth Y are disjoint (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilInvariant).

theorem AlgebraicGeometry.Scheme.IdealSheafData.sup_eq_top_of_disjoint_support {X : Scheme} (I J : X.IdealSheafData) (h : Disjoint I.support J.support) : I ⊔ J = ⊤

Ideal sheaves with disjoint supports are comaximal: supp (I ⊔ J) = supp I ⊓ supp J = ∅.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup_eq_top_of_sup_eq_top {X : Scheme} (I J : X.IdealSheafData) (h : I ⊔ J = ⊤) (U : ↑X.affineOpens) : I.ideal U ⊔ J.ideal U = ⊤

On every affine open, comaximal ideal sheaves have comaximal ideals of sections.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_eq_inf_of_sup_eq_top {X : Scheme} (I J : X.IdealSheafData) (h : I ⊔ J = ⊤) : I * J = I ⊓ J

The product of comaximal ideal sheaves is their intersection (Mathlib's Ideal.mul_eq_inf_of_coprime on every affine open).

theorem AlgebraicGeometry.Scheme.IdealSheafData.colon_mul_left_of_sup_eq_top {X : Scheme} (I J : X.IdealSheafData) (h : I ⊔ J = ⊤) : (I * J).colon I = J

The colon of the product by the first factor is the second, for comaximal ideal sheaves: (I · J) : I = J.