Documentation

Hironaka.Scheme.Modules.AffineLocal

Finite presentation from the affine opens #

Mathlib's notion of a sheaf of modules of finite presentation (SheafOfModules.IsFinitePresentation, which implies IsQuasicoherent and IsFiniteType) asks for a covering family of objects of the site and finite presentations of the restrictions over them. For a sheaf of modules F on a scheme X such restrictions come from the affine opens: a finite presentation of the restriction of F to Spec Γ(X, U) ≅ U gives one of F.over U (Scheme.Modules.presentationOverOfRestrict, by Mathlib's transport of presentations along functors that preserve colimits and the unit), and over Spec R a quasi-coherent sheaf M^~ with M finitely presented has a finite presentation (Mathlib's presentationTilde). Hence F is of finite presentation as soon as, over every affine open U, its restriction to Spec Γ(X, U) is the sheaf M^~ of the finitely presented module M = Γ(F, U) (Scheme.Modules.isFinitePresentation_of_forall_affine).

source
noncomputable def AlgebraicGeometry.Scheme.Modules.restrictιIso {X : Scheme} (F : X.Modules) {U : X.Opens} (hU : IsAffineOpen U) :
(F.restrict hU.fromSpec).restrict hU.isoSpec.hom ≅ F.restrict U.ι

The restriction of F to an open U along U.ι is the restriction to Spec Γ(X, U) pushed along U ≅ Spec Γ(X, U).

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.overIso {X : Scheme} (F : X.Modules) (U : X.Opens) :
    (overEquiv U).inverse.obj (F.restrict U.ι) ≅ SheafOfModules.over F U

    F.over U is the restriction of F along U.ι, through overEquiv U.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.presentationOverOfRestrict {X : Scheme} (F : X.Modules) {U : X.Opens} (hU : IsAffineOpen U) (P : SheafOfModules.Presentation (F.restrict hU.fromSpec)) :
      (SheafOfModules.over F U).Presentation

      A presentation of F.over U from one of the restriction of F to Spec Γ(X, U), for an affine open U: transported along the restriction to U ≅ Spec Γ(X, U) and the equivalence overEquiv U, which preserve colimits and the unit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AlgebraicGeometry.Scheme.Modules.isFinite_presentationOverOfRestrict {X : Scheme} (F : X.Modules) {U : X.Opens} (hU : IsAffineOpen U) (P : SheafOfModules.Presentation (F.restrict hU.fromSpec)) [P.IsFinite] :
        (F.presentationOverOfRestrict hU P).IsFinite
        source
        theorem AlgebraicGeometry.Scheme.Modules.isFinitePresentation_of_forall_affine {X : Scheme} (F : X.Modules) (h : ∀ (U : X.Opens) (hU : IsAffineOpen U), ∃ (P : SheafOfModules.Presentation (F.restrict hU.fromSpec)), P.IsFinite) :
        SheafOfModules.IsFinitePresentation F

        Finite presentation from the affine opens: if over every affine open U the restriction of F to Spec Γ(X, U) has a finite presentation, then F is of finite presentation (hence quasi-coherent and of finite type).

        source
        theorem AlgebraicGeometry.Scheme.Modules.exists_isFinite_presentation_restrict {X : Scheme} (F : X.Modules) {V : X.Opens} (hV : IsAffineOpen V) [CategoryTheory.IsIso (F.restrict hV.fromSpec).fromTildeΓ] [Module.FinitePresentation ↑(X.presheaf.obj (Opposite.op V)) ↑(F.presheaf.obj (Opposite.op V))] :
        ∃ (P : SheafOfModules.Presentation (F.restrict hV.fromSpec)), P.IsFinite

        Over an affine open V, if the restriction of F to Spec Γ(X, V) is the sheaf associated to its global sections and Γ(F, V) is a finitely presented Γ(X, V)-module, the restriction has a finite presentation (Mathlib's presentationTilde).

        source
        theorem AlgebraicGeometry.finite_moduleSpecΓ_of_generatingSections {R : CommRingCat} (M : (Spec R).Modules) [CategoryTheory.IsIso M.fromTildeΓ] (G : SheafOfModules.GeneratingSections M) [G.IsFiniteType] :
        Module.Finite ↑R ↑(moduleSpecΓFunctor.obj M)

        Over Spec R, a quasi-coherent sheaf of modules generated by finitely many global sections has finitely generated global sections: through the equivalence M ↦ M^~, which reflects epimorphisms, the epimorphism from the free sheaf on the generators is a surjection R^I → Γ(M).

        source
        theorem AlgebraicGeometry.Scheme.Modules.exists_isAffineOpen_finite_sections {X : Scheme} (F : X.Modules) [SheafOfModules.IsQuasicoherent F] [SheafOfModules.IsFiniteType F] (x : ↥X) :
        ∃ (U : X.Opens) (_ : IsAffineOpen U), x ∈ U ∧ Module.Finite ↑(X.presheaf.obj (Opposite.op U)) ↑(F.presheaf.obj (Opposite.op U))

        A quasi-coherent sheaf of finite type has finitely generated sections over small affine opens: every point has an affine open neighbourhood U with Γ(F, U) a finitely generated Γ(X, U)-module. The finitely many local generators of F over an open W ∋ x, restricted to an affine U ⊆ W and transported to Spec Γ(X, U), generate there the sheaf associated to Γ(F, U) (finite_moduleSpecΓ_of_generatingSections).