Module

SubmoduleGluingUnion.lean

Nyll.SchemeTheory.Modules.SubmoduleGluingUnion

3 declarations indexed from sourceView source ↗

Module documentation

Finite-type quasicoherent gluing on a union of opens

The two actual opens cover their union in its slice site. Consequently, the actual glued submodule restricts to a finite-type quasicoherent module on that union whenever the prescribed local submodules have those properties and their embedded section submodules agree on the overlap.

Imports3

Nyll.SchemeTheory.Modules.FiniteTypeSubopen
Nyll.SchemeTheory.Modules.SubmoduleGluingFiniteType
Mathlib.Topology.Sheaves.SheafCondition.Sites

Imported by2

theorem

coversTop_union

L28 ↗

SheafOfModules.Submodule.coversTop_union

Source context 4 commands

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

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

Lean source · full declaration

theorem coversTop_union {X : Scheme.{u}} (U V : X.Opens) :
    ((Opens.grothendieckTopology X).over (U ⊔ V)).CoversTop
      (fun b : ULift.{u} Bool => cond b.down
        (Over.mk (homOfLE (le_sup_left : U ≤ U ⊔ V)))
        (Over.mk (homOfLE (le_sup_right : V ≤ U ⊔ V)))) := by
  intro W
  apply ((Opens.grothendieckTopology X).mem_over_iff _).mpr
  intro x hx
  have hxUV : x ∈ U ⊔ V := (leOfHom W.hom) hx
  rcases hxUV with hxU | hxV
  · refine ⟨W.left ⊓ U, homOfLE inf_le_left, ?_, ⟨hx, hxU⟩⟩
    apply (Sieve.overEquiv_iff _ _).mpr
    exact ⟨⟨true⟩, ⟨Over.homMk (homOfLE inf_le_right)⟩⟩
  · refine ⟨W.left ⊓ V, homOfLE inf_le_left, ?_, ⟨hx, hxV⟩⟩
    apply (Sieve.overEquiv_iff _ _).mpr
    exact ⟨⟨false⟩, ⟨Over.homMk (homOfLE inf_le_right)⟩⟩

theorem

isFiniteType_glueOn_over_sup

L46 ↗

SheafOfModules.Submodule.isFiniteType_glueOn_over_sup

Documentation

The actual glued submodule has finite type on the union of its two prescribed opens.

Source context 4 commands

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

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

Lean source · statement

theorem isFiniteType_glueOn_over_sup {X : Scheme.{u}}
    {M : SheafOfModules.{u} X.ringCatSheaf} (N P : M.Submodule) (U V : X.Opens)
    (h : ∀ (Z : X.Opens) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z))
    (hN : (N.toSheafOfModules.over U).IsFiniteType)
    (hP : (P.toSheafOfModules.over V).IsFiniteType) :
    ((glueOn N P U V).toSheafOfModules.over (U ⊔ V)).IsFiniteType

theorem

isQuasicoherent_glueOn_over_sup

L73 ↗

SheafOfModules.Submodule.isQuasicoherent_glueOn_over_sup

Documentation

The actual glued submodule is quasicoherent on the union of its prescribed opens.

Source context 4 commands

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

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

Lean source · statement

theorem isQuasicoherent_glueOn_over_sup {X : Scheme.{u}}
    {M : SheafOfModules.{u} X.ringCatSheaf} (N P : M.Submodule) (U V : X.Opens)
    (h : ∀ (Z : X.Opens) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z))
    (hN : (N.toSheafOfModules.over U).IsQuasicoherent)
    (hP : (P.toSheafOfModules.over V).IsQuasicoherent) :
    ((glueOn N P U V).toSheafOfModules.over (U ⊔ V)).IsQuasicoherent

Module documentation

Finite-type quasicoherent gluing on a union of opens

Declarations

coversTop_union

isFiniteType_glueOn_over_sup

isQuasicoherent_glueOn_over_sup