Module

FiniteTypeAffineSections.lean

Nyll.SchemeTheory.Modules.FiniteTypeAffineSections

4 declarations indexed from sourceView source ↗

Module documentation

Affine sections of finite-type quasicoherent modules

The actual local finite generators restrict to every subordinate affine open. Their free epimorphisms yield finite section modules there. Basic opens subordinate to the given generator cover span the unit ideal of an affine chart, and the native section-localization maps allow the existing finite-localization theorem to extract finitely many generators.

Imports13

Nyll.SchemeTheory.Modules.FiniteGeneratingSections
Nyll.SchemeTheory.Modules.SectionLocalization
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Mathlib.Algebra.Category.ModuleCat.Sheaf.Submodule
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.Topology.Sheaves.Module
Mathlib.RingTheory.Localization.Finiteness

Imported by3

theorem

finite_sections_of_finite_spec_restriction

L39 ↗

AlgebraicGeometry.Scheme.Modules.finite_sections_of_finite_spec_restriction

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem finite_sections_of_finite_spec_restriction
    {X : Scheme.{u}} (M : X.Modules) {R : CommRingCat.{u}}
    (j : Spec R ⟶ X) [IsOpenImmersion j]
    [Module.Finite R ((moduleSpecΓFunctor (R := R)).obj (M.restrict j))] :
    Module.Finite Γ(X, j ''ᵁ ⊤) Γ(M, j ''ᵁ ⊤)

theorem

moduleFinite_sections_of_generatingSections_over

L70 ↗

AlgebraicGeometry.Scheme.Modules.moduleFinite_sections_of_generatingSections_over

Documentation

Finite actual generators over an open set give a finite module of sections over each subordinate affine open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem moduleFinite_sections_of_generatingSections_over
    {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent]
    {U W : X.Opens} (hU : IsAffineOpen U) (hUW : U ≤ W)
    (G : (M.over W).GeneratingSections) [G.IsFiniteType] :
    Module.Finite Γ(X, U) Γ(M, U)

theorem

moduleFinite_sections_of_isFiniteType

L124 ↗

AlgebraicGeometry.Scheme.Modules.moduleFinite_sections_of_isFiniteType

Documentation

A finite-type quasicoherent module has a finite module of sections on every affine open, with the original coefficient ring and section action.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem moduleFinite_sections_of_isFiniteType
    {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent] [M.IsFiniteType]
    (U : X.Opens) (hU : IsAffineOpen U) : Module.Finite Γ(X, U) Γ(M, U)

theorem

fg_sections_submodule_of_isFiniteType

L160 ↗

AlgebraicGeometry.Scheme.Modules.fg_sections_submodule_of_isFiniteType

Documentation

The affine-section finiteness statement for an actual native submodule.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · full declaration

theorem fg_sections_submodule_of_isFiniteType
    {X : Scheme.{u}} {M : X.Modules} (N : M.Submodule)
    [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
    [N.toSheafOfModules.IsFiniteType]
    (U : X.Opens) (hU : IsAffineOpen U) : (N.toSubmodule.obj (op U)).FG := by
  let R : RingCat.{u} := X.ringCatSheaf.obj.obj (op U)
  let P : Submodule R (M.val.obj (op U)) := N.toSubmodule.obj (op U)
  have hfinite : Module.Finite R P :=
    moduleFinite_sections_of_isFiniteType (show X.Modules from N.toSheafOfModules) U hU
  exact (Module.Finite.iff_fg (R := R) (N := P)).mp hfinite

Module documentation

Affine sections of finite-type quasicoherent modules

Declarations

finite_sections_of_finite_spec_restriction

moduleFinite_sections_of_generatingSections_over

moduleFinite_sections_of_isFiniteType

fg_sections_submodule_of_isFiniteType