Covers by open immersions, and blow-ups of restrictions to opens

General lemmas written for the exceptional divisors of [Kol07, Remark 33] on the affine model (HironakaExamples/Sequence/Remark33Exceptional.lean):

• le_of_comap_le_of_forall_exists: an inequality of ideal sheaves holds if it holds after comap along a jointly surjective family of open immersions (the affine version is le_of_comap_le_of_iSup_eq_top);
• comap_colon_of_isOpenImmersion': inverse image along any open immersion commutes with the colon by an invertible ideal sheaf;
• isOpenImmersion_blowUpMap, exists_blowUpMap_eq: along an open immersion h, blowUpMap h D is an open immersion (the base change of h along IdealSheafData.blowUpπ D, isPullback_blowUpMap) whose image is the preimage of the range of h;
• specIdealSheaf_top: the ideal sheaf of the unit ideal is the unit ideal sheaf.

Covers by open immersions from arbitrary schemes

theorem AlgebraicGeometry.Remark33.le_of_comap_le_of_forall_exists {M : Scheme} {I J : M.IdealSheafData} {ι : Type u_1} {Y : ι → Scheme} (c : (i : ι) → Y i ⟶ M) [∀ (i : ι), IsOpenImmersion (c i)] (hc : ∀ (x : ↥M), ∃ (i : ι) (y : ↥(Y i)), (c i) y = x) (h : ∀ (i : ι), I.comap (c i) ≤ J.comap (c i)) : I ≤ J

An inequality of ideal sheaves holds if it holds after comap along a jointly surjective family of open immersions (the affine version is le_of_comap_le_of_iSup_eq_top).

theorem AlgebraicGeometry.Remark33.comap_colon_of_isOpenImmersion' {M Y : Scheme} (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 any open immersion commutes with the colon by an invertible ideal sheaf (from the affine case comap_colon_of_isOpenImmersion).

The blow-up of a restriction to an open covers the preimage of that open

instance AlgebraicGeometry.Remark33.isOpenImmersion_blowUpMap {Y X : Scheme} (h : Y ⟶ X) [IsOpenImmersion h] (D : X.IdealSheafData) : IsOpenImmersion (Scheme.Hom.blowUpMap h D)

blowUpMap h D along an open immersion h is an open immersion: it is the base change of h along IdealSheafData.blowUpπ D (the pullback square isPullback_blowUpMap).

theorem AlgebraicGeometry.Remark33.exists_blowUpMap_eq {Y X : Scheme} (h : Y ⟶ X) [IsOpenImmersion h] (D : X.IdealSheafData) (x : ↥D.blowUp) (y : ↥Y) (hxy : D.blowUpπ x = h y) : ∃ (z : ↥(D.comap h).blowUp), (Scheme.Hom.blowUpMap h D) z = x

A point of blowUp D over the range of the open immersion h comes from blowUp (D|_U).

theorem AlgebraicGeometry.Remark33.specIdealSheaf_top {R : Type u} [CommRing R] : specIdealSheaf ⊤ = ⊤

The ideal sheaf of the unit ideal is the unit ideal sheaf.