Products of pairwise disjoint components and their colons

For a finite set C of ideal sheaves with pairwise disjoint supports:

• any two sub-products over disjoint index sets are comaximal (prod_sup_prod_eq_top);
• the product over a finset is the intersection (prod_eq_inf_of_pairwise_disjoint), so for vanishing ideals the vanishing ideal of the union of the supports of a subset A ⊆ C is the product over A (vanishingIdeal_iSup_support_eq_prod);
• the colon of the full product by the product over A is the product over the complement (colon_prod_filter: (∏_C c) : (∏_A c) = ∏_{C ∖ A} c).

The comaximality tools are those of Hironaka.Resolution.Algebraic.Wlo05.ColonCoprime. In Włodarczyk's embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.Embedded) these describe the isolated ideal when Y is smooth: the components of a smooth Y are pairwise disjoint, the ideal of Y is the product of their reduced ideals, and the colon by the reduced ideal of the absorbed components is the ideal of the remaining ones (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilInvariant). The vanishing ideal of a union of disjoint components as a product is also used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP2Entry and Hironaka.Resolution.Algebraic.Wlo05.StrictTransformReduced.

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

The support of a product over a finset, as a Finset.sup of the supports.

theorem AlgebraicGeometry.Scheme.IdealSheafData.prod_sup_prod_eq_top {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) (A B : Finset ι) (hdisj : ∀ a ∈ A, ∀ b ∈ B, Disjoint (I a).support (I b).support) : (∏ j ∈ A, I j) ⊔ ∏ j ∈ B, I j = ⊤

Sub-products of a family with pairwise disjoint supports over disjoint index sets are comaximal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.prod_eq_inf_of_pairwise_disjoint {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) (A : Finset ι) (hdisj : (↑A).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) : ∏ j ∈ A, I j = A.inf I

The product over a finset of a family with pairwise disjoint supports is the intersection.

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup_support_eq_prod {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) (A : Finset ι) (hrad : ∀ a ∈ A, vanishingIdeal (I a).support = I a) (hdisj : (↑A).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) : vanishingIdeal (⨆ j ∈ A, (I j).support) = ∏ j ∈ A, I j

For vanishing ideals with pairwise disjoint supports, the vanishing ideal of the union of the supports over a finset is the product over the finset.

theorem AlgebraicGeometry.Scheme.IdealSheafData.colon_prod_filter {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) (C : Finset ι) (P : ι → Prop) [DecidablePred P] (hrad : ∀ a ∈ C, vanishingIdeal (I a).support = I a) (hdisj : (↑C).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) : (∏ j ∈ C, I j).colon (vanishingIdeal (⨆ j ∈ Finset.filter P C, (I j).support)) = ∏ j ∈ C with ¬P j, I j

The colon by the absorbed components: for a finset C of vanishing ideals with pairwise disjoint supports and a predicate P on it, the colon of the product over C by the vanishing ideal of the union of the supports over C.filter P is the product over C.filter (¬ P).