The locally finite product of ideal sheaves

The monomial part M(I) of an ideal sheaf I with respect to a boundary family F (Kol07, Definition–Lemma 110, in the form used by this library: BMO/MonomialPart.lean) is the product, over the connected components D of the members of F, of the powers 𝓘_D^{ord_D I}. On a non-compact manifold a member can have infinitely many connected components, so the product is infinite; it is nevertheless locally finite, because the components form a locally finite family of closed sets and each factor is the unit ideal off its component. This file defines the locally finite product of a family of ideal sheaves A i with controlling sets S i (each A i is the unit ideal outside S i, and the S i are locally finite): the ideal sheaf whose stalk at x is the finite product of the stalks of the A i with x ∈ S i. It has local generators because, near any point, it agrees with the finite product over the indices whose controlling set meets a neighbourhood of the point.

The statements are about ideal sheaves on an arbitrary sheaf of commutative rings on a topological space; the topological lemma locallyFinite_sigma at the top is general as well. Not in the sources; auxiliary for the monomial part of [Kol07, Definition–Lemma 110] on manifolds.

theorem Hironaka.Manifold.locallyFinite_sigma {X : Type u} [TopologicalSpace X] {ι : Type u_1} {β : ι → Type u_2} {T : ι → Set X} (hT : LocallyFinite T) {S : (i : ι) × β i → Set X} (hS : ∀ (i : ι), LocallyFinite fun (c : β i) => S ⟨i, c⟩) (hsub : ∀ (i : ι) (c : β i), S ⟨i, c⟩ ⊆ T i) : LocallyFinite S

A sigma-indexed family of sets is locally finite when it is dominated by a locally finite outer family T (S ⟨i, c⟩ ⊆ T i) and, for each outer index i, the inner family c ↦ S ⟨i, c⟩ is locally finite: near a point only finitely many outer sets T i are met, and for each of those only finitely many inner sets. Applied to the connected components of the members of a boundary family, indexed by the member and the component.

noncomputable def Manifold.IdealSheaf.activeFinset {X : Type u} [TopologicalSpace X] {κ : Type u} (S : κ → Set X) (hLF : LocallyFinite S) (x : X) : Finset κ

The finite set of indices i whose controlling set S i contains x; finite because the family S is locally finite, so only finitely many S i meet a neighbourhood of x.

Equations

• Manifold.IdealSheaf.activeFinset S hLF x = ⋯.toFinset

@[simp]

theorem Manifold.IdealSheaf.mem_activeFinset {X : Type u} [TopologicalSpace X] {κ : Type u} {S : κ → Set X} {hLF : LocallyFinite S} {x : X} {i : κ} : i ∈ activeFinset S hLF x ↔ x ∈ S i

An index i is active at x exactly when x lies in its controlling set S i.

noncomputable def Manifold.IdealSheaf.lfpStalk {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} {κ : Type u} (A : κ → IdealSheaf 𝒪) (S : κ → Set X) (hLF : LocallyFinite S) (x : X) : Ideal ↑(𝒪.presheaf.stalk x)

The stalk assignment of the locally finite product: at x, the finite product of the stalks of the A i over the indices active at x.

Equations

• Manifold.IdealSheaf.lfpStalk A S hLF x = ∏ i ∈ Manifold.IdealSheaf.activeFinset S hLF x, (A i).stalkIdeal x

theorem Manifold.IdealSheaf.hasLocalGenerators_lfpStalk {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} {κ : Type u} (A : κ → IdealSheaf 𝒪) (S : κ → Set X) (hLF : LocallyFinite S) (hunit : ∀ (i : κ), ∀ x ∉ S i, (A i).stalkIdeal x = ⊤) : HasLocalGenerators (lfpStalk A S hLF)

The stalk assignment lfpStalk has local generators: near any point it agrees with the finite product ∏ i ∈ T, A i over the indices whose controlling set meets a neighbourhood of the point, the inactive factors being the unit ideal by hunit, and the local generators of that finite product, restricted to a smaller open set, generate it.

noncomputable def Manifold.IdealSheaf.locallyFiniteProduct {X : Type u} [TopologicalSpace X] (𝒪 : TopCat.Sheaf CommRingCat ↧X) {κ : Type u} (A : κ → IdealSheaf 𝒪) (S : κ → Set X) (hLF : LocallyFinite S) (hunit : ∀ (i : κ), ∀ x ∉ S i, (A i).stalkIdeal x = ⊤) : IdealSheaf 𝒪

The locally finite product of a family A : κ → IdealSheaf 𝒪 with controlling sets S : κ → Set X (each A i is the unit ideal outside S i) that form a locally finite family: the ideal sheaf whose stalk at x is ∏ i ∈ activeFinset S hLF x, (A i).stalkIdeal x. This is the form in which the monomial part of an ideal sheaf on a non-compact manifold is assembled from its component factors ([Kol07, Definition–Lemma 110]), where a finite product would not do.

Equations

• Manifold.IdealSheaf.locallyFiniteProduct 𝒪 A S hLF hunit = Manifold.IdealSheaf.ofStalks 𝒪 (Manifold.IdealSheaf.lfpStalk A S hLF) ⋯

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_locallyFiniteProduct {X : Type u} [TopologicalSpace X] {𝒪 : TopCat.Sheaf CommRingCat ↧X} {κ : Type u} (A : κ → IdealSheaf 𝒪) (S : κ → Set X) (hLF : LocallyFinite S) (hunit : ∀ (i : κ), ∀ x ∉ S i, (A i).stalkIdeal x = ⊤) (x : X) : (locallyFiniteProduct 𝒪 A S hLF hunit).stalkIdeal x = ∏ i ∈ activeFinset S hLF x, (A i).stalkIdeal x

The stalk of the locally finite product at x is the finite product of the stalks of the factors active at x.