Ideal sheaves on the charts of the blow-up

For an ideal sheaf J' on blowUp I and a chart blowUp.chart I U a : Spec Γ(X, U)[I(U)/a] ⟶ blowUp I, the inverse image J'.comap (chart U a) is the ideal sheaf of a single ideal chartIdeal I J' U a of the chart ring (comap_chart_eq_specIdealSheaf). This module records that dictionary and the chart forms of the ideal sheaves entering the composite of two blow-ups (Hironaka.Scheme.BlowUp.Composite); the chart ideal is also the form in which strict transforms and orders along the exceptional divisor are computed in the worked examples (HironakaExamples.Sequence.Remark33Model, HironakaExamples.OrderReduction.Example106, Hironaka.Scheme.IdealSheaf.Order.ExceptionalOrder).

• specIdealSheaf_le_iff, specIdealSheaf_inj, specIdealSheaf_pow, and isInvertible_specIdealSheaf_span_singleton: specIdealSheaf is an order embedding and a semiring map from ideals of R to ideal sheaves on Spec R;
• blowUp.comap_exceptionalDivisor_chart: on the chart of a the exceptional ideal is (a) (affineBlowUp.comap_exceptionalIdeal_chart through blowUp.chart_eq);
• comap_mul_pow_chart: (J' * E^m).comap (chart U a) = specIdealSheaf (J'_a * (a)^m);
• comap_comap_chart: (K.comap b).comap (chart U a) = specIdealSheaf (K(U)·Γ(X, U)[I(U)/a]) for any ideal sheaf K on X (comap_comap_eq_of_chart_π of Hironaka.Scheme.BlowUp.ProductCenter at the blow-up AlgebraicGeometry.Scheme.IdealSheafData.blowUp).

theorem AlgebraicGeometry.specIdealSheaf_le_iff {R : Type u} [CommRing R] (P Q : Ideal R) : specIdealSheaf P ≤ specIdealSheaf Q ↔ P ≤ Q

On Spec R the ideal sheaf of P is contained in the ideal sheaf of Q iff P ≤ Q.

theorem AlgebraicGeometry.specIdealSheaf_inj {R : Type u} [CommRing R] {P Q : Ideal R} (h : specIdealSheaf P = specIdealSheaf Q) : P = Q

specIdealSheaf is injective.

theorem AlgebraicGeometry.specIdealSheaf_pow {R : Type u} [CommRing R] (P : Ideal R) (m : ℕ) : specIdealSheaf (P ^ m) = specIdealSheaf P ^ m

specIdealSheaf is multiplicative on powers.

theorem AlgebraicGeometry.isInvertible_specIdealSheaf_span_singleton {R : Type u} [CommRing R] {g : R} (hg : g ∈ nonZeroDivisors R) : (specIdealSheaf (Ideal.span {g})).IsInvertible

The ideal sheaf on Spec R of a principal ideal generated by a nonzerodivisor is invertible (on the affine open ⊤, transported along ΓSpecIso).

theorem AlgebraicGeometry.eq_specIdealSheaf {R : Type u} [CommRing R] (L : (Spec ↧R).IdealSheafData) : L = specIdealSheaf (Ideal.comap (CommRingCat.Hom.hom (Scheme.ΓSpecIso ↧R).inv) (L.ideal ⟨⊤, ⋯⟩))

Every ideal sheaf on Spec R is the ideal sheaf of its ideal of global sections.

theorem Ideal.map_span_pair {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] {F : Type u_3} [FunLike F A B] [RingHomClass F A B] (f : F) (a b : A) : map f (span {a, b}) = span {f a, f b}

The image of a two-generator ideal under a ring map, f(a, b) = (f a, f b): Mathlib's Ideal.map_span with Set.image_pair. Used for the chart substitutions of the worked examples.

noncomputable def AlgebraicGeometry.chartIdeal {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : Ideal ↥(affineBlowUpAlgebra (I.ideal U) ↑a)

The ideal of the chart ring Γ(X, U)[I(U)/a] cut out by J' on the chart of a: the ideal of J'.comap (chart U a) on ⊤, transported to the chart ring.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.comap_chart_eq_specIdealSheaf {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : J'.comap (Scheme.IdealSheafData.blowUp.chart I U a) = specIdealSheaf (chartIdeal I J' U a)

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.comap_exceptionalDivisor_chart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) : I.exceptionalDivisor.comap (chart I U a) = specIdealSheaf (Ideal.span {(algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑a)) ↑a})

On the chart of a the exceptional ideal of the blow-up is the ideal sheaf of (a) (affineBlowUp.comap_exceptionalIdeal_chart, through blowUp.chart_eq).

theorem AlgebraicGeometry.comap_mul_pow_chart {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) (m : ℕ) : (J' * I.exceptionalDivisor ^ m).comap (Scheme.IdealSheafData.blowUp.chart I U a) = specIdealSheaf (chartIdeal I J' U a * Ideal.span {(algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑a)) ↑a} ^ m)

The chart form of J' * E^m: on the chart of a it is the ideal sheaf of J'_a * (a)^m.

theorem AlgebraicGeometry.comap_comap_chart {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (a : ↥(I.ideal U)) (K : X.IdealSheafData) : (K.comap I.blowUpπ).comap (Scheme.IdealSheafData.blowUp.chart I U a) = specIdealSheaf (Ideal.map (algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑a)) (K.ideal U))

The chart form of the inverse image of an ideal sheaf K on X: on the chart of a, (K.comap b).comap (chart U a) is the ideal sheaf of K(U)·Γ(X, U)[I(U)/a] (comap_comap_eq_of_chart_π of Hironaka.Scheme.BlowUp.ProductCenter at AlgebraicGeometry.Scheme.IdealSheafData.blowUp).