Finite products of ideal sheaves

The support of a finite product of ideal sheaves is the union of their supports. When the supports of finitely many ideal sheaves are pairwise disjoint, their product equals their intersection. This identifies the sum of section divisors with their set-theoretic union, and of disjoint section divisors with their scheme-theoretic union.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_finset_prod {X : Scheme} {ι : Type u_1} (s : Finset ι) (I : ι → X.IdealSheafData) : (∏ i ∈ s, I i).support = s.sup fun (i : ι) => (I i).support

The support of a finite product of ideal sheaves is the supremum of their supports.

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_prod {X : Scheme} {ι : Type u_1} [Fintype ι] (I : ι → X.IdealSheafData) : ↑(∏ i : ι, I i).support = ⋃ (i : ι), ↑(I i).support

The support of a product of ideal sheaves indexed by a finite type, as a set, is the union of their supports.

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 generate the unit ideal sheaf together.

theorem AlgebraicGeometry.Scheme.IdealSheafData.prod_eq_iInf_of_pairwise_disjoint_support {X : Scheme} {ι : Type u_1} [Fintype ι] (I : ι → X.IdealSheafData) (h : Pairwise fun (i j : ι) => Disjoint (I i).support (I j).support) : ∏ i : ι, I i = ⨅ (i : ι), I i

A finite product of ideal sheaves with pairwise disjoint supports equals their intersection.