Sections that are locally combinations of a family of global sections

A finite family σ of global sections of a module sheaf G generates G exactly when every section of G is, near every point, a structure-sheaf combination of the restrictions of σ. This file names that condition on one section, IsLocalCombination, proves it closed under the operations a sheafification argument produces -- zero, sums, restriction -- and turns it into the conclusion a generation theorem wants: the map free I ⟶ G classifying σ is an epimorphism.

Why a predicate on one section

Serre's global generation reaches the epimorphism through epi_of_pointwise_preimages, which asks for a local preimage of one section at one point. The section to be handled arrives as a restriction of a finite sum of pure tensors (exists_eq_sum_tmulSection), so the argument has to pass through sums and restrictions before it reaches the pure tensor it can actually compute with. Stating the condition on a single section, with Finset.sum_induction doing the sums, keeps every one of those steps a lemma here rather than an inline bookkeeping block at the call site.

The classifying map

sectionsOfTop reads a section over ⊤ as a global section in Mathlib's sense, a compatible family over every open; freeHomEquiv.symm then packages the family σ as free I ⟶ G. The preimage of a local combination ∑ cₐ • σₐ|_W is ∑ cₐ • ιFree a (1), and that is the whole of epi_freeHomEquiv_symm_of_isLocalCombination.

noncomputable def AlgebraicGeometry.Scheme.Modules.sectionsOfTop {X : Scheme} (G : X.Modules) (σ : ↑(G.presheaf.obj (Opposite.op ⊤))) : (have this := G; this).sections

A section over ⊤, as a global section in Mathlib's sense: the compatible family of its restrictions to every open.

Equations

• G.sectionsOfTop σ = PresheafOfModules.sectionsMk (fun (x : (TopologicalSpace.Opens ↥X)ᵒᵖ) => (CategoryTheory.ConcreteCategory.hom (G.presheaf.map (CategoryTheory.homOfLE ⋯).op)) σ) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsOfTop_val {X : Scheme} (G : X.Modules) (σ : ↑(G.presheaf.obj (Opposite.op ⊤))) (U : X.Opensᵒᵖ) : ↑(G.sectionsOfTop σ) U = (CategoryTheory.ConcreteCategory.hom (G.presheaf.map (CategoryTheory.homOfLE ⋯).op)) σ

def AlgebraicGeometry.Scheme.Modules.IsLocalCombination {X : Scheme} (G : X.Modules) {I : Type u_1} [Fintype I] (σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))) {U : X.Opens} (z : ↑(G.presheaf.obj (Opposite.op U))) : Prop

A section is a local combination of σ when, near every point of its open, it is a structure-sheaf combination of the restrictions of the family σ of sections over ⊤.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.IsLocalCombination.zero {X : Scheme} (G : X.Modules) {I : Type u_1} [Fintype I] (σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))) (U : X.Opens) : G.IsLocalCombination σ 0

theorem AlgebraicGeometry.Scheme.Modules.IsLocalCombination.add {X : Scheme} {G : X.Modules} {I : Type u_1} [Fintype I] {σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))} {U : X.Opens} {z₁ z₂ : ↑(G.presheaf.obj (Opposite.op U))} (h₁ : G.IsLocalCombination σ z₁) (h₂ : G.IsLocalCombination σ z₂) : G.IsLocalCombination σ (z₁ + z₂)

theorem AlgebraicGeometry.Scheme.Modules.IsLocalCombination.finset_sum {X : Scheme} {G : X.Modules} {I : Type u_1} [Fintype I] {σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))} {U : X.Opens} {κ : Type u_2} (S : Finset κ) (f : κ → ↑(G.presheaf.obj (Opposite.op U))) (h : ∀ p ∈ S, G.IsLocalCombination σ (f p)) : G.IsLocalCombination σ (∑ p ∈ S, f p)

theorem AlgebraicGeometry.Scheme.Modules.IsLocalCombination.res {X : Scheme} {G : X.Modules} {I : Type u_1} [Fintype I] {σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))} {U V : X.Opens} (hVU : V ≤ U) {z : ↑(G.presheaf.obj (Opposite.op U))} (h : G.IsLocalCombination σ z) : G.IsLocalCombination σ ((CategoryTheory.ConcreteCategory.hom (G.presheaf.map (CategoryTheory.homOfLE hVU).op)) z)

theorem AlgebraicGeometry.Scheme.Modules.freeHomEquiv_symm_sectionsOfTop_ιFree_app_one {X : Scheme} (G : X.Modules) {I : Type u} (σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))) (a : I) (W : X.Opens) : (ModuleCat.Hom.hom ((CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree a) ((have this := G; this).freeHomEquiv.symm fun (b : I) => G.sectionsOfTop (σ b))).val.app (Opposite.op W))) 1 = (CategoryTheory.ConcreteCategory.hom (G.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (σ a)

The classifying map of σ evaluates ιFree a to the restriction of σ a.

theorem AlgebraicGeometry.Scheme.Modules.epi_freeHomEquiv_symm_of_isLocalCombination {X : Scheme} (G : X.Modules) {I : Type u} [Fintype I] (σ : I → ↑(G.presheaf.obj (Opposite.op ⊤))) (h : ∀ (U : X.Opens) (z : ↑(G.presheaf.obj (Opposite.op U))), G.IsLocalCombination σ z) : CategoryTheory.Epi ((have this := G; this).freeHomEquiv.symm fun (a : I) => G.sectionsOfTop (σ a))

A family every section is locally a combination of classifies an epimorphism.

The local preimage of ∑ cₐ • σₐ|_W under free I ⟶ G is ∑ cₐ • ιFree a (1); the map is linear on sections, and ιFree a composed with the classifying map is σ a.