Quasicoherent sheaves #

A sheaf of modules is quasi-coherent if it admits locally a presentation as the cokernel of a morphism between coproducts of copies of the sheaf of rings. When these coproducts are finite, we say that the sheaf is of finite presentation.

References #

https://stacks.math.columbia.edu/tag/01BD

source

structure SheafOfModules.Presentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (M : SheafOfModules R) :

Type (max (u + 1) u')

A global presentation of a sheaf of modules M consists of a family generators.s of sections s which generate M, and a family of sections which generate the kernel of the morphism generators.π : free (generators.I) ⟶ M.

generators : M.GeneratingSections
generators
relations : (CategoryTheory.Limits.kernel self.generators.π).GeneratingSections
relations

Instances For

source

class SheafOfModules.Presentation.IsFinite {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (p : M.Presentation) :

Prop

A global presentation of a sheaf of module if finite if the type of generators and relations are finite.

isFiniteType_generators : p.generators.IsFiniteType
finite_relations : Finite p.relations.I

Instances

source

def SheafOfModules.generatorsOfIsCokernelFree {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

M.GeneratingSections

Given two morphisms of sheaves of R-modules f : free ι ⟶ free σ and g : free σ ⟶ M satisfying H : f ≫ g = 0 and IsColimit (CokernelCofork.ofπ g H), we obtain generators of Presentation M.

Equations

SheafOfModules.generatorsOfIsCokernelFree f g H H' = { I := σ, s := M.freeHomEquiv g, epi := ⋯ }

Instances For

source

@[simp]

theorem SheafOfModules.generatorsOfIsCokernelFree_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(generatorsOfIsCokernelFree f g H H').I = σ

source

@[simp]

theorem SheafOfModules.generatorsOfIsCokernelFree_s {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) (a✝ : σ) :

(generatorsOfIsCokernelFree f g H H').s a✝ = M.freeHomEquiv g a✝

source

@[simp]

theorem SheafOfModules.generatorsOfIsCokernelFree_π {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(generatorsOfIsCokernelFree f g H H').π = g

source

def SheafOfModules.relationsOfIsCokernelFree {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(CategoryTheory.Limits.kernel (generatorsOfIsCokernelFree f g H H').π).GeneratingSections

Given two morphisms of sheaves of R-modules f : free ι ⟶ free σ and g : free σ ⟶ M satisfying H : f ≫ g = 0 and IsColimit (CokernelCofork.ofπ g H), we obtain relations of Presentation M.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem SheafOfModules.relationsOfIsCokernelFree_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(relationsOfIsCokernelFree f g H H').I = ι

source

@[simp]

theorem SheafOfModules.relationsOfIsCokernelFree_s {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) (a✝ : ι) :

(relationsOfIsCokernelFree f g H H').s a✝ = (CategoryTheory.Limits.kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv (CategoryTheory.Limits.kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯) a✝

source

def SheafOfModules.presentationOfIsCokernelFree {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

M.Presentation

Given two morphisms of sheaves of R-modules f : free ι ⟶ free σ and g : free σ ⟶ M satisfying H : f ≫ g = 0 and IsColimit (CokernelCofork.ofπ g H), we obtain a Presentation M.

Equations

SheafOfModules.presentationOfIsCokernelFree f g H H' = { generators := SheafOfModules.generatorsOfIsCokernelFree f g H H', relations := SheafOfModules.relationsOfIsCokernelFree f g H H' }

Instances For

source

@[simp]

theorem SheafOfModules.presentationOfIsCokernelFree_relations {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(presentationOfIsCokernelFree f g H H').relations = relationsOfIsCokernelFree f g H H'

source

@[simp]

theorem SheafOfModules.presentationOfIsCokernelFree_generators {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {ι σ : Type u} {M : SheafOfModules R} (f : free ι ⟶ free σ) (g : free σ ⟶ M) (H : CategoryTheory.CategoryStruct.comp f g = 0) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) :

(presentationOfIsCokernelFree f g H H').generators = generatorsOfIsCokernelFree f g H H'

source

Given a sheaf of R-modules M and a Presentation M, there is two morphism of sheaves of R-modules f : free ι ⟶ free σ and g : free σ ⟶ M satisfying H : f ≫ g = 0 and IsColimit (CokernelCofork.ofπ g H).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SheafOfModules.Presentation.mapRelations {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

free P.relations.I ⟶ free P.generators.I

Let F be a functor from sheaf of R-module to sheaf of S-module, if F preserves colimits and F.obj (unit R) ≅ unit S, given a P : Presentation M, then we will obtain relations of Presentation (F.obj M).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SheafOfModules.Presentation.mapGenerators {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

free P.generators.I ⟶ F.obj M

Let F be a functor from sheaf of R-module to sheaf of S-module, if F preserves colimits and F.obj (unit R) ≅ unit S, given a P : Presentation M, then we will obtain generators of Presentation (F.obj M).

Equations

P.mapGenerators F η = CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFree F η P.generators.I).inv (F.map P.generators.π)

Instances For

source

@[simp]

theorem SheafOfModules.Presentation.mapRelations_mapGenerators {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

CategoryTheory.CategoryStruct.comp (P.mapRelations F η) (P.mapGenerators F η) = 0

source

@[simp]

theorem SheafOfModules.Presentation.mapRelations_mapGenerators_assoc {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) {Z : SheafOfModules S} (h : F.obj M ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.mapRelations F η) (CategoryTheory.CategoryStruct.comp (P.mapGenerators F η) h) = CategoryTheory.CategoryStruct.comp 0 h

source

def SheafOfModules.Presentation.map {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

(F.obj M).Presentation

Let F be a functor from sheaf of R-module to sheaf of S-module, if F preserves colimits and F.obj (unit R) ≅ unit S, given a P : Presentation M, then we will get a Presentation (F.obj M).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem SheafOfModules.Presentation.map_generators_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

(P.map F η).generators.I = P.generators.I

source

@[simp]

theorem SheafOfModules.Presentation.map_relations_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

(P.map F η).relations.I = P.relations.I

source

theorem SheafOfModules.Presentation.map_π_eq {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {C' : Type u'} [CategoryTheory.Category.{v', u'} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] [J'.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimits F] (η : F.obj (unit R) ≅ unit S) :

(P.map F η).generators.π = CategoryTheory.CategoryStruct.comp (mapFree F η P.generators.I).inv (F.map P.generators.π)

source

structure SheafOfModules.QuasicoherentData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) :

Type (max (max (u + 1) (u' + 1)) v')

This structure contains the data of a family of objects X i which cover the terminal object, and of a presentation of M.over (X i) for all i.

I : Type u'
the index type of the covering
X : self.I → C
a family of objects which cover the terminal object
coversTop : J.CoversTop self.X
presentation (i : self.I) : (M.over (self.X i)).Presentation
a presentation of the sheaf of modules M.over (X i) for any i : I

Instances For

source

def SheafOfModules.QuasicoherentData.localGeneratorsData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) :

M.LocalGeneratorsData

If M is quasicoherent, it is locally generated by sections.

Equations

q.localGeneratorsData = { I := q.I, X := q.X, coversTop := ⋯, generators := fun (i : q.I) => (q.presentation i).generators }

Instances For

source

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_generators {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) (i : q.I) :

q.localGeneratorsData.generators i = (q.presentation i).generators

source

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) :

q.localGeneratorsData.I = q.I

source

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_X {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) (a✝ : q.I) :

q.localGeneratorsData.X a✝ = q.X a✝

source

class SheafOfModules.QuasicoherentData.IsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) :

Prop

A (local) presentation of a sheaf of module M is a finite presentation if each given presentation of M.over (X i) is a finite presentation.

isFinite_presentation (i : q.I) : (q.presentation i).IsFinite

Instances

source

instance SheafOfModules.QuasicoherentData.instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) [q.IsFinitePresentation] :

q.localGeneratorsData.IsFiniteType

source

class SheafOfModules.IsQuasicoherent {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) :

Prop

A sheaf of modules is quasi-coherent if it is locally the cokernel of a morphism between coproducts of copies of the sheaf of rings.

nonempty_quasicoherentData : Nonempty M.QuasicoherentData

Instances

source

@[reducible, inline]

abbrev SheafOfModules.isQuasicoherent {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] :

CategoryTheory.ObjectProperty (SheafOfModules R)

A sheaf of modules is quasi-coherent if it is locally the cokernel of a morphism between coproducts of copies of the sheaf of rings.

Equations

SheafOfModules.isQuasicoherent R = SheafOfModules.IsQuasicoherent

Instances For

source

class SheafOfModules.IsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) :

Prop

A sheaf of modules is finitely presented if it is locally the cokernel of a morphism between coproducts of finitely many copies of the sheaf of rings.

exists_quasicoherentData : ∃ (σ : M.QuasicoherentData), σ.IsFinitePresentation

Instances

source

@[reducible, inline]

abbrev SheafOfModules.isFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] :

CategoryTheory.ObjectProperty (SheafOfModules R)

A sheaf of modules is finitely presented if it is locally the cokernel of a morphism between coproducts of finitely many copies of the sheaf of rings.

Equations