Module

FiniteGeneratingSections.lean

Nyll.SchemeTheory.Modules.FiniteGeneratingSections

1 declaration indexed from sourceView source ↗

Module documentation

Finite generating sections on an affine scheme

The literal finite free sheaf epimorphism becomes a map from a finite free module under the fully faithful tilde functor. The actual quasicoherent counit isomorphism identifies its target with the original global sections. Faithfulness reflects epimorphisms, so the resulting linear map is surjective.

Imports6

Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.CategoryTheory.Functor.EpiMono
Mathlib.RingTheory.Finiteness.Finsupp

Imported by2

theorem

moduleFinite_moduleSpecΓ_of_generatingSections

L33 ↗

AlgebraicGeometry.Scheme.Modules.moduleFinite_moduleSpecΓ_of_generatingSections

Documentation

A finite family generating a quasicoherent sheaf on Spec R makes its actual global-section module finite over R.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem moduleFinite_moduleSpecΓ_of_generatingSections
    {R : CommRingCat.{u}} (M : (Spec R).Modules) [M.IsQuasicoherent]
    (G : M.GeneratingSections) [G.IsFiniteType] :
    Module.Finite R ((moduleSpecΓFunctor (R := R)).obj M)

Module documentation

Finite generating sections on an affine scheme

Declarations

moduleFinite_moduleSpecΓ_of_generatingSections