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

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

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

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 := ⋯ }

@[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✝

@[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 = σ

@[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

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.

@[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 = ι

@[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✝

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' }

@[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'

@[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'

def SheafOfModules.Presentation.isColimit {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)] {M : SheafOfModules R} (P : M.Presentation) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ P.generators.π ⋯)

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.

noncomputable def SheafOfModules.Presentation.of_isIso {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)] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.Presentation) : N.Presentation

Mapping a presentation under an isomorphism.

Equations

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

@[simp]

theorem SheafOfModules.Presentation.of_isIso_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)] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.Presentation) : (of_isIso f σ).relations = σ.relations.ofEpi ((CategoryTheory.Limits.kernelCompMono σ.generators.π f).symm ≪≫ CategoryTheory.eqToIso ⋯).hom

@[simp]

theorem SheafOfModules.Presentation.of_isIso_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)] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.Presentation) : (of_isIso f σ).generators = σ.generators.ofEpi f

theorem SheafOfModules.instPreservesColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F

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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} 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.

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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} 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.π)

@[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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : F.obj (unit R) ≅ unit S) : CategoryTheory.CategoryStruct.comp (P.mapRelations F η) (P.mapGenerators F η) = 0

@[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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} 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

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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} 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.

@[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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : F.obj (unit R) ≅ unit S) : (P.map F η).generators.I = P.generators.I

@[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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : F.obj (unit R) ≅ unit S) : (P.map F η).relations.I = P.relations.I

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.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : F.obj (unit R) ≅ unit S) : (P.map F η).generators.π = CategoryTheory.CategoryStruct.comp (mapFree F η P.generators.I).inv (F.map P.generators.π)

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 (max (u + 1) u₁) v₁) (w + 1))

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 w

  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

noncomputable def SheafOfModules.QuasicoherentData.shrink {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.QuasicoherentData

Shrink the indexing type of QuasicoherentData into the universe of the site.

Equations

• q.shrink = { I := ↑(Set.range q.X), X := fun (i : ↑(Set.range q.X)) => q.X (Exists.choose ⋯), coversTop := ⋯, presentation := fun (i : ↑(Set.range q.X)) => q.presentation (Exists.choose ⋯) }

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 }

@[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

@[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✝

@[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

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

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

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

theorem SheafOfModules.QuasicoherentData.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} (q : M.QuasicoherentData) : M.IsQuasicoherent

@[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

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

@[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

• SheafOfModules.isFinitePresentation R = SheafOfModules.IsFinitePresentation

instance SheafOfModules.instIsQuasicoherentOfIsFinitePresentation {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) [M.IsFinitePresentation] : M.IsQuasicoherent

instance SheafOfModules.instIsFiniteTypeOfIsFinitePresentation {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) [M.IsFinitePresentation] : M.IsFiniteType

@[deprecated "Use the lemma `IsFinitePresentation.exists_quasicoherentData` instead." (since := "2025-10-28")]

noncomputable def SheafOfModules.quasicoherentDataOfIsFinitePresentation {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) [M.IsFinitePresentation] : M.QuasicoherentData

A choice of local presentations when M is a sheaf of modules of finite presentation.

Equations

• M.quasicoherentDataOfIsFinitePresentation = ⋯.choose

def SheafOfModules.Presentation.quasicoherentData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : M.QuasicoherentData

Given a sheaf of R-modules M and a Presentation M, we may construct the quasi-coherent data on the trivial cover.

Equations

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

@[simp]

theorem SheafOfModules.Presentation.quasicoherentData_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (a : C) : P.quasicoherentData.X a = id a

@[simp]

theorem SheafOfModules.Presentation.quasicoherentData_presentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (x : C) : P.quasicoherentData.presentation x = P.map (pushforward (CategoryTheory.CategoryStruct.id (R.over x))) (CategoryTheory.Iso.refl ((pushforward (CategoryTheory.CategoryStruct.id (R.over x))).obj (unit R)))

@[simp]

theorem SheafOfModules.Presentation.quasicoherentData_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : P.quasicoherentData.I = C

theorem SheafOfModules.Presentation.isQuasicoherent {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : M.IsQuasicoherent

If a sheaf of R-modules M has a presentation, then M is quasi-coherent.

noncomputable def SheafOfModules.QuasicoherentData.bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {I : Type u} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).QuasicoherentData) : M.QuasicoherentData

Given an cover X and a quasicoherent data for M restricted onto each Mᵢ, we may glue them into a quasicoherent data of M itself.

Equations

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

theorem SheafOfModules.IsQuasicoherent.of_coversTop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {I : Type u} (X : I → C) (hX : J.CoversTop X) [∀ (i : I), (M.over (X i)).IsQuasicoherent] : M.IsQuasicoherent