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
• isFiniteType_relations : p.relations.IsFiniteType

@[deprecated SheafOfModules.Presentation.IsFinite.isFiniteType_relations (since := "2026-04-14")]

theorem SheafOfModules.Presentation.IsFinite.finite_relations {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) [p.IsFinite] : Finite p.relations.I

noncomputable 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

noncomputable 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_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✝

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

noncomputable 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_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'

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

noncomputable 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.ofIsIso {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.ofIsIso_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) : (ofIsIso f σ).generators = σ.generators.ofEpi f

@[simp]

theorem SheafOfModules.Presentation.ofIsIso_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) : (ofIsIso f σ).relations = σ.relations.ofEpi ((CategoryTheory.Limits.kernelCompMono σ.generators.π f).symm ≪≫ CategoryTheory.eqToIso ⋯).hom

@[deprecated SheafOfModules.Presentation.ofIsIso (since := "2026-04-15")]

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

Alias of SheafOfModules.Presentation.ofIsIso.

---

Mapping a presentation under an isomorphism.

Equations

• @SheafOfModules.Presentation.of_isIso = @SheafOfModules.Presentation.ofIsIso

instance SheafOfModules.instIsFiniteOfIsIso {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) [σ.IsFinite] : (Presentation.ofIsIso f σ).IsFinite

theorem SheafOfModules.instPreservesColimitsOfSize_1 {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

noncomputable 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] (η : unit S ≅ F.obj (unit R)) : 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.

@[reducible, inline]

noncomputable abbrev 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] (η : unit S ≅ F.obj (unit R)) : 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 η = P.generators.mapFreeHom F η

@[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] (η : unit S ≅ F.obj (unit R)) : 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] (η : unit S ≅ F.obj (unit R)) {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

noncomputable 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] (η : unit S ≅ F.obj (unit R)) : (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] (η : unit S ≅ F.obj (unit R)) : (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] (η : unit S ≅ F.obj (unit R)) : (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] (η : unit S ≅ F.obj (unit R)) : (P.map F η).generators.π = CategoryTheory.CategoryStruct.comp (mapFreeIso F P.generators.I η).hom (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_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

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

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

noncomputable def SheafOfModules.QuasicoherentData.pushforward {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] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), (K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) : ((SheafOfModules.pushforward φ).obj M).QuasicoherentData

The pushforward of SheafOfModules.QuasicoherentData along a continuous and cocontinuous functor.

Equations

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

@[simp]

theorem SheafOfModules.QuasicoherentData.pushforward_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] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), (K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) (i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)) : (pushforward G φ η h P).X i = i.fst

@[simp]

theorem SheafOfModules.QuasicoherentData.pushforward_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] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), (K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (SheafOfModules.pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} (P : M.QuasicoherentData) : (pushforward G φ η h P).I = ((X : D) × (i : P.I) × (G.obj X ⟶ P.X i))

theorem SheafOfModules.isQuasicoherent_pushforward {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] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), (K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (pushforward φ).obj (unit R) ≅ unit S) [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] (h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y), CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} (pushforward (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))) {M : SheafOfModules R} [M.IsQuasicoherent] : ((pushforward φ).obj M).IsQuasicoherent

theorem SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint {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] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), (K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [K.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C) [G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R) (η : (pushforward φ).obj (unit R) ≅ unit S) [G.IsLeftAdjoint] [CategoryTheory.IsIso φ] [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPullbacks D] {M : SheafOfModules R} [M.IsQuasicoherent] : ((pushforward φ).obj M).IsQuasicoherent

noncomputable 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 (unit (R.over x)))

@[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.ofIsIso {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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.QuasicoherentData) : N.QuasicoherentData

Mapping quasicoherent data under an isomorphism.

Equations

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

@[simp]

theorem SheafOfModules.QuasicoherentData.ofIsIso_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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.QuasicoherentData) : (ofIsIso f σ).I = σ.I

@[simp]

theorem SheafOfModules.QuasicoherentData.ofIsIso_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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.QuasicoherentData) (a✝ : σ.I) : (ofIsIso f σ).X a✝ = σ.X a✝

@[simp]

theorem SheafOfModules.QuasicoherentData.ofIsIso_presentation {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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.QuasicoherentData) (i : σ.I) : (ofIsIso f σ).presentation i = Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i)

instance SheafOfModules.instIsClosedUnderIsomorphismsIsQuasicoherent {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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : (isQuasicoherent R).IsClosedUnderIsomorphisms

instance SheafOfModules.instIsFinitePresentationOfIsIso {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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (σ : M.QuasicoherentData) [σ.IsFinitePresentation] : (QuasicoherentData.ofIsIso f σ).IsFinitePresentation

instance SheafOfModules.instIsClosedUnderIsomorphismsIsFinitePresentation {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.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : (isFinitePresentation R).IsClosedUnderIsomorphisms

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

theorem SheafOfModules.isQuasicoherent_over {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.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] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] (M : SheafOfModules R) (X : C) [M.IsQuasicoherent] : (M.over X).IsQuasicoherent