NYLL
Module

FiniteQuasicoherentSum.lean

Nyll.SchemeTheory.Modules.FiniteQuasicoherentSum
11 declarations indexed from sourceView source ↗

Module documentation

Actual finite joins of finite-type quasicoherent subsheaves

The native sheaf-lattice join is identified with the actual image of the map from the coproduct. The proof uses the least-submodule property of the image and both original inclusions. No pointwise-sum description of the sheaf join is assumed.

Imports4
Imported by2

Declarations

def

homOfLE

L35 ↗
SheafOfModules.Submodule.homOfLE
Documentation

Inclusion of native submodules from their actual pointwise containment.

Source context 6 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
Lean source · statement
def Submodule.homOfLE {M : SheafOfModules.{u} R} {N P : M.Submodule} (h : N ≤ P) :
    N.toSheafOfModules ⟶ P.toSheafOfModules
theorem

homOfLE_ι

L40 ↗
SheafOfModules.Submodule.homOfLE_ι
Documentation

The containment-induced map respects both embeddings into the ambient sheaf.

Source context 6 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
Lean source · statement
theorem Submodule.homOfLE_ι {M : SheafOfModules.{u} R} {N P : M.Submodule}
    (h : N ≤ P) : Submodule.homOfLE h ≫ P.ι = N.ι
theorem

imageSubmodule_coprod_eq_sup

L47 ↗
SheafOfModules.imageSubmodule_coprod_eq_sup
Documentation

The sheaf-lattice join is the actual image of the coproduct of the inclusions.

Source context 7 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem imageSubmodule_coprod_eq_sup {M : SheafOfModules.{u} R} (N P : M.Submodule) :
    imageSubmodule (coprod.desc N.ι P.ι) = N ⊔ P
theorem

imageSubmodule_zero

L64 ↗
SheafOfModules.imageSubmodule_zero
Documentation

The actual image of a zero morphism is the bottom native submodule.

Source context 7 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem imageSubmodule_zero (M N : SheafOfModules.{u} R) :
    imageSubmodule (0 : M ⟶ N) = ⊥
theorem

isFiniteType_free_finite

L76 ↗
SheafOfModules.isFiniteType_free_finite
Source context 9 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
section FiniteType
variable [HasBinaryProducts C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem isFiniteType_free_finite (I : Type u) [Finite I] :
    (free (R := R) I).IsFiniteType
theorem

isFiniteType_bot

L91 ↗
SheafOfModules.Submodule.isFiniteType_bot
Documentation

The bottom native submodule is of finite type.

Source context 9 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
section FiniteType
variable [HasBinaryProducts C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
Lean source · statement
theorem Submodule.isFiniteType_bot (M : SheafOfModules.{u} R) :
    (⊥ : M.Submodule).toSheafOfModules.IsFiniteType
theorem

isFiniteType_sup

L102 ↗
SheafOfModules.Submodule.isFiniteType_sup
Documentation

The actual sheaf-lattice join of two finite-type submodules is finite type.

Source context 10 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
section FiniteType
variable [HasBinaryProducts C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasPullbacks C]
Lean source · statement
theorem Submodule.isFiniteType_sup {M : SheafOfModules.{u} R}
    (N P : M.Submodule) [N.toSheafOfModules.IsFiniteType] [P.toSheafOfModules.IsFiniteType] :
    (N ⊔ P).toSheafOfModules.IsFiniteType
theorem

isFiniteType_finset_sup

L111 ↗
SheafOfModules.Submodule.isFiniteType_finset_sup
Documentation

The actual finite join of finite-type native submodules is finite type.

Source context 10 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section General
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
variable [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
section FiniteType
variable [HasBinaryProducts C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasPullbacks C]
Lean source · statement
theorem Submodule.isFiniteType_finset_sup {M : SheafOfModules.{u} R}
    {ι : Type w} (s : Finset ι) (N : ι → M.Submodule)
    (h : ∀ i ∈ s, (N i).toSheafOfModules.IsFiniteType) :
    (s.sup N).toSheafOfModules.IsFiniteType
theorem

isQuasicoherent_bot

L136 ↗
SheafOfModules.Submodule.isQuasicoherent_bot
Documentation

The bottom native submodule of a quasicoherent sheaf is quasicoherent.

Source context 6 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section Quasicoherent
variable {X : Scheme.{u}} {M : SheafOfModules.{u} X.ringCatSheaf} [M.IsQuasicoherent]
Lean source · statement
theorem Submodule.isQuasicoherent_bot :
    (⊥ : M.Submodule).toSheafOfModules.IsQuasicoherent
theorem

isQuasicoherent_sup

L143 ↗
SheafOfModules.Submodule.isQuasicoherent_sup
Documentation

The actual sheaf-lattice join of two quasicoherent submodules is quasicoherent.

Source context 6 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section Quasicoherent
variable {X : Scheme.{u}} {M : SheafOfModules.{u} X.ringCatSheaf} [M.IsQuasicoherent]
Lean source · statement
theorem Submodule.isQuasicoherent_sup (N P : M.Submodule)
    [N.toSheafOfModules.IsQuasicoherent] [P.toSheafOfModules.IsQuasicoherent] :
    (N ⊔ P).toSheafOfModules.IsQuasicoherent
theorem

isQuasicoherent_finset_sup

L153 ↗
SheafOfModules.Submodule.isQuasicoherent_finset_sup
Documentation

The actual finite join of quasicoherent native submodules is quasicoherent.

Source context 6 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits AlgebraicGeometry
namespace SheafOfModules
section Quasicoherent
variable {X : Scheme.{u}} {M : SheafOfModules.{u} X.ringCatSheaf} [M.IsQuasicoherent]
Lean source · statement
theorem Submodule.isQuasicoherent_finset_sup {ι : Type w}
    (s : Finset ι) (N : ι → M.Submodule)
    (h : ∀ i ∈ s, (N i).toSheafOfModules.IsQuasicoherent) :
    (s.sup N).toSheafOfModules.IsQuasicoherent

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