Module

FiniteTypeLocalAffineSections.lean

Nyll.SchemeTheory.Modules.FiniteTypeLocalAffineSections

3 declarations indexed from sourceView source ↗

Module documentation

Affine-section finiteness from finite type only on the given open

The finite-type hypothesis concerns the original module restricted to the given open. The proved site-equivalence transport puts it on that actual open subscheme. Its affine-section finiteness is transported back with the existing section and coefficient isomorphisms, then supplied to canonical localization. Global finite type of the ambient module is never required.

Imports5

Nyll.SchemeTheory.Modules.FiniteTypeAffineSections
Nyll.SchemeTheory.Modules.FiniteTypeSchemeRestriction
Nyll.SchemeTheory.Modules.AffineSectionLocalizationFinite
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme

Imported by2

theorem

finite_sections_of_finite_restriction

L31 ↗

AlgebraicGeometry.Scheme.Modules.finite_sections_of_finite_restriction

Source context 4 commands

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

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

Lean source · statement

theorem finite_sections_of_finite_restriction
    {X Y : Scheme.{u}} (M : X.Modules) (j : Y ⟶ X) [IsOpenImmersion j]
    (V : Y.Opens) (hFinite : Module.Finite Γ(Y, V) Γ(M.restrict j, V)) :
    Module.Finite Γ(X, j ''ᵁ V) Γ(M, j ''ᵁ V)

theorem

moduleFinite_sections_of_isFiniteType_over

L50 ↗

AlgebraicGeometry.Scheme.Modules.moduleFinite_sections_of_isFiniteType_over

Documentation

Finite type of the actual module over an affine open suffices for its native module of sections there to be finite.

Source context 4 commands

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

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

Lean source · statement

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

theorem

fg_localized_top_of_isFiniteType_over_basicOpen

L65 ↗

AlgebraicGeometry.Scheme.Modules.fg_localized_top_of_isFiniteType_over_basicOpen

Documentation

Finite type only over the given principal open supplies the canonical localized-top FG condition used in affine finite-submodule extraction.

Source context 4 commands

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

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

Lean source · full declaration

theorem fg_localized_top_of_isFiniteType_over_basicOpen
    {R : CommRingCat.{u}} (M : (Spec R).Modules) [M.IsQuasicoherent] (r : R) :
    let U : (Spec R).Opens := PrimeSpectrum.basicOpen r
    (M.over U).IsFiniteType →
      ((⊤ : Submodule R ((moduleSpecΓFunctor (R := R)).obj M)).localized
        (Submonoid.powers r)).FG := by
  intro U hFinite
  have hΓ : Module.Finite ((Spec R).ringCatSheaf.obj.obj (op U)) (M.val.obj (op U)) :=
    moduleFinite_sections_of_isFiniteType_over M U (IsAffineOpen.Spec_basicOpen r) hFinite
  exact fg_localized_top_of_finite_basicOpen M r hΓ

Module documentation

Affine-section finiteness from finite type only on the given open

Declarations

finite_sections_of_finite_restriction

moduleFinite_sections_of_isFiniteType_over

fg_localized_top_of_isFiniteType_over_basicOpen