Theorems · Theorem · algebraic geometry

SheafOfModules.Presentation.mapRelations_mapGenerators_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.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

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

0 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.CategoryCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.Limits.PreservesColimitsOfSize