Nyll.SchemeTheory.Modules.FiniteSubmoduleUnionExtension

Module documentation

Global representatives of finite submodules glued on a union

The two actual submodules are glued on the union of their prescribed opens. The native quasicoherent extension construction then produces a global representative with both exact restrictions and finite type on the union. Global finite type is not asserted outside that union.

theorem

exists_finiteType_union_extension

L35 ↗

AlgebraicGeometry.Scheme.Modules.exists_finiteType_union_extension

Documentation

Glue the prescribed finite restrictions on two compact opens, and extend the actual glued submodule to a global quasicoherent representative.

Source context 5 commands

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

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

Lean source · statement

theorem exists_finiteType_union_extension {X : Scheme.{u}} [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] (N P : F.Submodule)
    [N.toSheafOfModules.IsQuasicoherent] [P.toSheafOfModules.IsQuasicoherent]
    (U V : X.Opens) (hU : IsCompact (U : Set X)) (hV : IsCompact (V : Set X))
    (h : ∀ (Z : X.Opens) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z))
    (hNft : (N.toSheafOfModules.over U).IsFiniteType)
    (hPft : (P.toSheafOfModules.over V).IsFiniteType) :
    ∃ L : F.Submodule, L.toSheafOfModules.IsQuasicoherent ∧
      (L.toSheafOfModules.over (U ⊔ V)).IsFiniteType ∧
      L.over U = N.over U ∧ L.over V = P.over V

Module documentation

Global representatives of finite submodules glued on a union

Declarations

exists_finiteType_union_extension