Finite sums and products of locally finitely generated ideal sheaves

Sums, products and powers of locally finitely generated ideal sheaves are locally finitely generated; the binary + and *, ⊤ and ⊥ are built from their stalks by IdealSheaf.ofStalks, and the power pow by recursion. To write finite sums ∑ i ∈ F, G i and finite products ∏ i ∈ F, G i of ideal sheaves — Kollár's maximal coefficient ideal W_s(I) = ∑_{wt(e) ≥ s} ∏_j (D^j I)^{e_j} [Kol07, Definition 98] is one — this module records the AddCommMonoid and CommMonoid structures of IdealSheaf 𝒪 on those operations: 0 = ⊥, 1 = ⊤, + and * the existing sum and product, and the monoid power npow n J the existing pow (definitionally; five rfl examples check that no second power, unit or zero appears). Every law holds stalkwise (IdealSheaf.ext and the stalk simp lemmas), and taking the stalk at a point is additive and multiplicative on finite families (stalkIdeal_finset_sum, stalkIdeal_finset_prod).

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instZero {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : Zero (IdealSheaf 𝒪)

Equations

• Manifold.IdealSheaf.instZero = { zero := ⊥ }

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instOne {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : One (IdealSheaf 𝒪)

Equations

• Manifold.IdealSheaf.instOne = { one := ⊤ }

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_zero {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (x : ↑X) : stalkIdeal 0 x = ⊥

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_one {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (x : ↑X) : stalkIdeal 1 x = ⊤

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instAddCommMonoid {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : AddCommMonoid (IdealSheaf 𝒪)

The additive monoid of ideal sheaves, 0 = ⊥ and + the sum (stalkwise sup).

Equations

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

instance Manifold.IdealSheaf.instIsOrderedAddMonoid {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : IsOrderedAddMonoid (IdealSheaf 𝒪)

The sum of ideal sheaves is monotone: IdealSheaf 𝒪 is an ordered additive monoid, so that Mathlib's Finset.single_le_sum and Finset.sum_le_sum apply to finite sums of ideal sheaves.

@[instance_reducible]

noncomputable instance Manifold.IdealSheaf.instCommMonoid {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : CommMonoid (IdealSheaf 𝒪)

The multiplicative monoid of ideal sheaves, 1 = ⊤, * the product and J ^ n the existing pow.

Equations

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

theorem Manifold.IdealSheaf.stalkIdeal_finset_sum {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) (x : ↑X) : (∑ i ∈ F, G i).stalkIdeal x = ∑ i ∈ F, (G i).stalkIdeal x

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_finset_prod {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) (x : ↑X) : (∏ i ∈ F, G i).stalkIdeal x = ∏ i ∈ F, (G i).stalkIdeal x

theorem Manifold.IdealSheaf.hasLocalGenerators_stalkIdeal {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (J : IdealSheaf 𝒪) : HasLocalGenerators J.stalkIdeal

The stalks of an ideal sheaf have local generators (its locallyFG field).