Colon ideals along ring maps and open immersions; inequalities on covers

Helpers for colon ideals and ideal sheaves, written for the computation of [Kol07, Remark 33] on the affine model (HironakaExamples/Sequence/Remark33Iso.lean):

• Ideal.comap_colon_of_surjective, Ideal.map_colon_of_bijective: the colon commutes with the comap along a surjective ring map and with the map along a bijective one;
• le_of_comap_le_of_iSup_eq_top: an inequality of ideal sheaves holds if it holds after comap along a cover by open immersions from affine schemes;
• comap_colon_of_isOpenImmersion: inverse image along an open immersion from an affine scheme commutes with the colon by an invertible ideal sheaf;
• specIdealSheaf_colon: on Spec R, the colon of ideal sheaves is the ideal sheaf of the colon when the divisor is invertible.

Ring-level helpers: colon ideals along surjective and bijective ring maps

theorem Ideal.comap_colon_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (I J : Ideal S) : comap f (Submodule.colon I ↑J) = Submodule.colon (comap f I) ↑(comap f J)

The comap along a surjective ring map commutes with the colon.

theorem Ideal.map_colon_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Bijective ⇑f) (I J : Ideal R) : map f (Submodule.colon I ↑J) = Submodule.colon (map f I) ↑(map f J)

The map along a bijective ring map commutes with the colon.

Sheaf-level helpers: inequalities on a cover by open immersions, colons along them

theorem AlgebraicGeometry.Remark33.le_of_comap_le_of_iSup_eq_top {M : Scheme} {I J : M.IdealSheafData} {ι : Type u_1} {Y : ι → Scheme} (c : (i : ι) → Y i ⟶ M) [∀ (i : ι), IsOpenImmersion (c i)] [∀ (i : ι), IsAffine (Y i)] (hc : ⨆ (i : ι), Scheme.Hom.opensRange (c i) = ⊤) (h : ∀ (i : ι), I.comap (c i) ≤ J.comap (c i)) : I ≤ J

An inequality of ideal sheaves holds if it holds after comap along the members of a cover by open immersions from affine schemes.

theorem AlgebraicGeometry.Remark33.comap_colon_of_isOpenImmersion {M Y : Scheme} [IsAffine Y] (c : Y ⟶ M) [IsOpenImmersion c] (I : M.IdealSheafData) {K : M.IdealSheafData} (hK : K.IsInvertible) : (I.colon K).comap c = (I.comap c).colon (K.comap c)

Inverse image along an open immersion from an affine scheme commutes with the colon by an invertible ideal sheaf.

theorem AlgebraicGeometry.Remark33.specIdealSheaf_colon {R : Type u} [CommRing R] (P Q : Ideal R) (hQ : (specIdealSheaf Q).IsInvertible) : (specIdealSheaf P).colon (specIdealSheaf Q) = specIdealSheaf (Submodule.colon P ↑Q)

On Spec R, the colon of the ideal sheaves of P and of an invertible Q is the ideal sheaf of the colon.