Sections of products of modules on a scheme #
Limits of 𝒪_X-modules are computed on sections: taking sections over an open U preserves
limits. In particular the sections over U of a product ∏ⱼ Fⱼ of 𝒪_X-modules are the
families of sections of the factors. This file records the consequence used to compute modules
assembled as products of modules supported on disjoint open sets: if every factor other than
Fᵢ has no nonzero section over U, then the projection Γ(∏ⱼ Fⱼ, U) → Γ(Fᵢ, U) is bijective
(AlgebraicGeometry.Scheme.Modules.bijective_app_π_of_subsingleton).
theorem
AlgebraicGeometry.Scheme.Modules.bijective_app_π_of_subsingleton
{X : Scheme}
{ι : Type v}
[Small.{u, v} ι]
(F : ι → X.Modules)
[CategoryTheory.Limits.HasProduct F]
(i : ι)
(U : X.Opens)
(h : ∀ (j : ι), j ≠ i → Subsingleton ↑((F j).presheaf.obj (Opposite.op U)))
:
Over an open U on which every factor other than F i has only the zero section, the
projection from the sections of a product of 𝒪_X-modules to the sections of F i is
bijective.