NYLL
Module

SubmoduleGluingQuasicoherent.lean

Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent
7 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of the actual gluing of submodules

Restriction of a native submodule to the slice site is computed on its actual section submodules. The local section equalities of glueOn thus identify its restrictions with the two given quasicoherent modules. The native cover-locality theorem supplies quasicoherence of the glued object.

Imports4
Imported by9

Declarations

def

over

L33 ↗
SheafOfModules.Submodule.over
Documentation

Restrict an actual submodule to the slice site.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · full declaration
def over (N : M.Submodule) (U : C) : (M.over U).Submodule where
  toSubmodule :=
    { obj X := N.toSubmodule.obj (op X.unop.left)
      map f := N.toSubmodule.map f.unop.left.op }
  isSheaf := by
    intro X s hs
    apply N.isSheaf s
    apply J.superset_covering _ ((J.mem_over_iff _).mp hs)
    intro V i hi
    exact (Sieve.overEquiv_iff _ i).mp hi
def

overSheafIso

L45 ↗
SheafOfModules.Submodule.overSheafIso
Documentation

The module of the restricted native submodule is the restriction of its module.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · statement
def overSheafIso (N : M.Submodule) (U : C) :
    (N.over U).toSheafOfModules ≅ N.toSheafOfModules.over U
theorem

overSheafIso_hom_ι

L51 ↗
SheafOfModules.Submodule.overSheafIso_hom_ι
Documentation

The comparison of the actual restricted modules respects their embeddings.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · statement
theorem overSheafIso_hom_ι (N : M.Submodule) (U : C) :
    (overSheafIso N U).hom ≫ N.ι.over U = (N.over U).ι
theorem

over_eq_of_obj_eq

L62 ↗
SheafOfModules.Submodule.over_eq_of_obj_eq
Documentation

Local section equalities give equality of the actual restricted submodules.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · statement
theorem over_eq_of_obj_eq (N P : M.Submodule) (U : C)
    (h : ∀ (V : C) (_i : V ⟶ U),
      N.toSubmodule.obj (op V) = P.toSubmodule.obj (op V)) :
    N.over U = P.over U
def

glueOnOverIsoLeft

L72 ↗
SheafOfModules.Submodule.glueOnOverIsoLeft
Documentation

The two local sheaves of a glued submodule are the actual prescribed sheaves.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · statement
def glueOnOverIsoLeft (N P : M.Submodule) (U V : C)
    (h : ∀ (Z : C) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z)) :
    (glueOn N P U V).toSheafOfModules.over U ≅ N.toSheafOfModules.over U
def

glueOnOverIsoRight

L83 ↗
SheafOfModules.Submodule.glueOnOverIsoRight
Documentation

The second local sheaf of a glued submodule is its prescribed actual sheaf.

Source context 5 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
Lean source · statement
def glueOnOverIsoRight (N P : M.Submodule) (U V : C)
    (h : ∀ (Z : C) (_a : Z ⟶ U) (_b : Z ⟶ V),
      N.toSubmodule.obj (op Z) = P.toSubmodule.obj (op Z)) :
    (glueOn N P U V).toSheafOfModules.over V ≅ P.toSheafOfModules.over V
theorem

isQuasicoherent_glueOn

L102 ↗
SheafOfModules.Submodule.isQuasicoherent_glueOn
Documentation

The actual gluing is quasicoherent if its two prescribed local modules are quasicoherent and the two objects cover the site.

Source context 7 commands

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

noncomputable section
universe v v₁ u₁ u
open CategoryTheory Opposite
namespace SheafOfModules.Submodule
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}} {M : SheafOfModules.{v} R}
section Quasicoherent
variable [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
  [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
  [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · full declaration
theorem isQuasicoherent_glueOn {M' : SheafOfModules.{u} R}
    (N P : M'.Submodule) (U V : C)
    (hCover : J.CoversTop (fun b : ULift.{u} Bool => cond b.down U V))
    (h : ∀ (Z : C) (_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.IsQuasicoherent := by
  have hLocal : ∀ b : ULift.{u} Bool,
      ((glueOn N P U V).toSheafOfModules.over (cond b.down U V)).IsQuasicoherent := by
    intro b
    rcases b with ⟨b⟩
    cases b
    · exact (SheafOfModules.isQuasicoherent (R.over V)).prop_of_iso
        (glueOnOverIsoRight N P U V h).symm hP
    · exact (SheafOfModules.isQuasicoherent (R.over U)).prop_of_iso
        (glueOnOverIsoLeft N P U V h).symm hN
  exact SheafOfModules.IsQuasicoherent.of_coversTop
    (glueOn N P U V).toSheafOfModules
    (fun b : ULift.{u} Bool => cond b.down U V) hCover

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.