Inverse image along an open immersion and the colon by any ideal sheaf

comap_colon_of_isOpenImmersion (Hironaka/Scheme/BlowUpSequence/Remark33Iso.lean, affine source) and comap_colon_of_isOpenImmersion' (Hironaka/Scheme/BlowUpSequence/Remark33Exceptional.lean, any source) show that the inverse image along an open immersion commutes with the colon by an invertible ideal sheaf; this is the compatibility of the controlled transform with smooth pull-back in the proof of [Wlo05, Proposition 2.4.2]. On a locally Noetherian scheme every ideal of sections is finitely generated, so ideal_colon_of_fg (Hironaka/Scheme/BlowUp/Transform.lean) gives the sections of a colon sheaf on every affine open for any divisor K, and the same two proofs go through: comap_colon_of_isOpenImmersion_of_isAffine and comap_colon_of_isOpenImmersion_of_isLocallyNoetherian. The embedded desingularization uses them to read the ideal of the marked triple after isolating some components, a colon by the reduced ideal of the strict transforms already isolated (the proof of [Wlo05, Theorem 4.7.1]), through an open window. The invertible forms are the special case; they are not restated here.

theorem AlgebraicGeometry.Remark33.ideal_fg_of_isLocallyNoetherian {M : Scheme} [IsLocallyNoetherian M] (K : M.IdealSheafData) (U : ↑M.affineOpens) : (K.ideal U).FG

On a locally Noetherian scheme every ideal sheaf is finitely generated on every affine open; the locally Noetherian form of ideal_fg (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean, finite type over a field).

theorem AlgebraicGeometry.Remark33.ideal_colon_of_isLocallyNoetherian {M : Scheme} [IsLocallyNoetherian M] (I K : M.IdealSheafData) (U : ↑M.affineOpens) : (I.colon K).ideal U = Submodule.colon (I.ideal U) ↑(K.ideal U)

On a locally Noetherian scheme the sections of a colon sheaf on an affine open are the colon of the sections (ideal_colon_of_fg).

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

The generalisation of comap_colon_of_isOpenImmersion (Remark33Iso.lean; invertible K) to any K on a locally Noetherian scheme: inverse image along an open immersion from an affine scheme commutes with the colon; the same proof with ideal_colon_of_isLocallyNoetherian (finitely generated sections, ideal_colon_of_fg) in place of ideal_colon_of_isInvertible.

theorem AlgebraicGeometry.Remark33.comap_colon_of_isOpenImmersion_of_isLocallyNoetherian {M : Scheme} [IsLocallyNoetherian M] {Y : Scheme} (c : Y ⟶ M) [IsOpenImmersion c] (I K : M.IdealSheafData) : (I.colon K).comap c = (I.comap c).colon (K.comap c)

The generalisation of comap_colon_of_isOpenImmersion' (Remark33Exceptional.lean; invertible K) to any K on a locally Noetherian scheme: inverse image along any open immersion commutes with the colon; from the affine case by the same covering argument le_of_comap_le_of_forall_exists.