Extensions of finitely presented module sheaves

Finite presentation of sheaves of modules is closed under extensions. The proof is local on the site. On a finite cover, generators of the quotient are lifted simultaneously; after a second finite refinement, the resulting correction relations are lifted as well. A finite horseshoe presentation then presents the middle term.

This avoids affine cohomology entirely, so the theorem needs no noetherian hypothesis.

Main results

• SheafOfModules.IsFinitePresentation.middle_of_shortExact;
• SheafOfModules.isFinitePresentation_isClosedUnderExtensions.

@[implicit_reducible]

noncomputable def SheafOfModules.instAbelianSheafAddCommGrpCat_derivedAlgGeo {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrpCat] : CategoryTheory.Abelian (CategoryTheory.Sheaf J AddCommGrpCat)

Equations

• SheafOfModules.instAbelianSheafAddCommGrpCat_derivedAlgGeo = CategoryTheory.sheafIsAbelian

@[implicit_reducible]

noncomputable def SheafOfModules.instNonPreadditiveAbelianSheafAddCommGrpCat_derivedAlgGeo {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrpCat] : CategoryTheory.NonPreadditiveAbelian (CategoryTheory.Sheaf J AddCommGrpCat)

Equations

• SheafOfModules.instNonPreadditiveAbelianSheafAddCommGrpCat_derivedAlgGeo = CategoryTheory.Abelian.nonPreadditiveAbelian

noncomputable def SheafOfModules.simultaneousImageCover {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) (X : C) : J.Cover X

Equations

• SheafOfModules.simultaneousImageCover f s X = Finset.univ.inf fun (i : I) => ⟨CategoryTheory.Presheaf.imageSieve ((SheafOfModules.toSheaf R).map f).hom (↑(s i) (Opposite.op X)), ⋯⟩

theorem SheafOfModules.simultaneousImageCover_mem {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) (X : C) (a : (simultaneousImageCover f s X).Arrow) (i : I) : (CategoryTheory.Presheaf.imageSieve ((toSheaf R).map f).hom (↑(s i) (Opposite.op X))).arrows a.f

noncomputable def SheafOfModules.simultaneousImageCoverObjects {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) : (X : C) × (simultaneousImageCover f s X).Arrow → C

Equations

• SheafOfModules.simultaneousImageCoverObjects f s a = a.snd.Y

theorem SheafOfModules.simultaneousImageCoverObjects_coversTop {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) : J.CoversTop (simultaneousImageCoverObjects f s)

noncomputable def SheafOfModules.sectionOfInitial {D : Type u} [CategoryTheory.Category.{u, u} D] {S : CategoryTheory.Functor Dᵒᵖ RingCat} (M : PresheafOfModules S) (X : Dᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (x : ↑(M.obj X)) : M.sections

Equations

• SheafOfModules.sectionOfInitial M X hX x = PresheafOfModules.sectionsMk (fun (Y : Dᵒᵖ) => (CategoryTheory.ConcreteCategory.hom (M.map (hX.to Y))) x) ⋯

@[simp]

theorem SheafOfModules.sectionOfInitial_eval {D : Type u} [CategoryTheory.Category.{u, u} D] {S : CategoryTheory.Functor Dᵒᵖ RingCat} (M : PresheafOfModules S) (X : Dᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (x : ↑(M.obj X)) : ↑(sectionOfInitial M X hX x) X = x

noncomputable def SheafOfModules.overSection {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {X : C} (x : ↑((M.over X).val.obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))))) : (M.over X).sections

Equations

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

@[simp]

theorem SheafOfModules.overSection_eval_mkId {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {X : C} (x : ↑((M.over X).val.obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))))) : ↑(M.overSection x) (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))) = x

theorem SheafOfModules.overSection_ext {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {X : C} (s t : (M.over X).sections) (h : ↑s (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))) = ↑t (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X)))) : s = t

noncomputable def SheafOfModules.overUnitIso {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.Limits.HasBinaryProducts C] (U : C) : unit (R.over U) ≅ (overFunctor R U).obj (unit R)

Equations

• SheafOfModules.overUnitIso U = CategoryTheory.Iso.refl (SheafOfModules.unit (R.over U))

@[simp]

theorem SheafOfModules.unitToPushforwardObjUnit_over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.Limits.HasBinaryProducts C] (U : C) : unitToPushforwardObjUnit (CategoryTheory.CategoryStruct.id (R.over U)) = (overUnitIso U).hom

theorem SheafOfModules.freeHomEquiv_mapFree_over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {N : SheafOfModules R} {I : Type u} (p : free I ⟶ N) (i : I) (U : C) [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] : (N.over U).freeHomEquiv (CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) I (overUnitIso U)).hom ((overFunctor R U).map p)) i = pushforwardSections (CategoryTheory.CategoryStruct.id (R.over U)) (N.freeHomEquiv p i)

noncomputable def SheafOfModules.localLift {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) (a : (X : C) × (simultaneousImageCover f s X).Arrow) : free I ⟶ M.over a.snd.Y

Equations

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

theorem SheafOfModules.localLift_comp {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] {I : Type u} [Finite I] (s : I → N.sections) (a : (X : C) × (simultaneousImageCover f s X).Arrow) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.HasSheafify (J.over a.snd.Y) AddCommGrpCat] [(J.over a.snd.Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R a.snd.Y)] : CategoryTheory.CategoryStruct.comp (localLift f s a) ((overFunctor R a.snd.Y).map f) = CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R a.snd.Y) I (overUnitIso a.snd.Y)).hom ((overFunctor R a.snd.Y).map (N.freeHomEquiv.symm s))

@[reducible, inline]

noncomputable abbrev SheafOfModules.Presentation.mapOver {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {M : SheafOfModules R} (P : M.Presentation) (U : C) [(J.over U).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] : (M.over U).Presentation

Equations

• P.mapOver U = P.map (SheafOfModules.overFunctor R U) (SheafOfModules.overUnitIso U)

instance SheafOfModules.Presentation.mapOver_isFinite {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {M : SheafOfModules R} (P : M.Presentation) [P.IsFinite] (U : C) [(J.over U).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] : (P.mapOver U).IsFinite

@[implicit_reducible]

noncomputable def SheafOfModules.Presentation.instNonPreadditiveAbelian_derivedAlgGeo {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.NonPreadditiveAbelian (SheafOfModules R)

Equations

• SheafOfModules.Presentation.instNonPreadditiveAbelian_derivedAlgGeo = CategoryTheory.Abelian.nonPreadditiveAbelian

@[reducible, inline]

noncomputable abbrev SheafOfModules.Presentation.relationMap {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) : free P.relations.I ⟶ free P.generators.I

Equations

• P.relationMap = CategoryTheory.CategoryStruct.comp P.relations.π (CategoryTheory.Limits.kernel.ι P.generators.π)

@[simp]

theorem SheafOfModules.Presentation.relationMap_presentationOfIsCokernelFree {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective 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').relationMap = f

theorem SheafOfModules.Presentation.relationMap_mapOver {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {M : SheafOfModules R} (P : M.Presentation) (U : C) [(J.over U).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] : (P.mapOver U).relationMap = CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) P.relations.I (overUnitIso U)).hom (CategoryTheory.CategoryStruct.comp ((overFunctor R U).map P.relationMap) (mapFreeIso (overFunctor R U) P.generators.I (overUnitIso U)).inv)

@[simp]

theorem SheafOfModules.Presentation.freeMap_inl_freeSumIso_inv {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I K : Type u) : CategoryTheory.CategoryStruct.comp (freeMap Sum.inl) (freeSumIso I K).inv = CategoryTheory.Limits.coprod.inl

@[simp]

theorem SheafOfModules.Presentation.freeMap_inl_freeSumIso_inv_assoc {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I K : Type u) {Z : SheafOfModules R} (h : free I ⨿ free K ⟶ Z) : CategoryTheory.CategoryStruct.comp (freeMap Sum.inl) (CategoryTheory.CategoryStruct.comp (freeSumIso I K).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h

@[simp]

theorem SheafOfModules.Presentation.freeMap_inr_freeSumIso_inv {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I K : Type u) : CategoryTheory.CategoryStruct.comp (freeMap Sum.inr) (freeSumIso I K).inv = CategoryTheory.Limits.coprod.inr

@[simp]

theorem SheafOfModules.Presentation.freeMap_inr_freeSumIso_inv_assoc {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I K : Type u) {Z : SheafOfModules R} (h : free I ⨿ free K ⟶ Z) : CategoryTheory.CategoryStruct.comp (freeMap Sum.inr) (CategoryTheory.CategoryStruct.comp (freeSumIso I K).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h

noncomputable def SheafOfModules.Presentation.correction {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : free P₃.relations.I ⟶ S.X₁

Equations

• SheafOfModules.Presentation.correction S hS P₃ h hh = ⋯.lift (CategoryTheory.CategoryStruct.comp P₃.relationMap h) ⋯

theorem SheafOfModules.Presentation.correction_comp {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.CategoryStruct.comp (correction S hS P₃ h hh) S.f = CategoryTheory.CategoryStruct.comp P₃.relationMap h

theorem SheafOfModules.Presentation.correction_comp_assoc {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) {Z : SheafOfModules R} (h✝ : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (correction S hS P₃ h hh) (CategoryTheory.CategoryStruct.comp S.f h✝) = CategoryTheory.CategoryStruct.comp P₃.relations.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι P₃.generators.π) (CategoryTheory.CategoryStruct.comp h h✝))

noncomputable def SheafOfModules.Presentation.extensionGeneratorsMap {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) : free (P₁.generators.I ⊕ P₃.generators.I) ⟶ S.X₂

Equations

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

noncomputable def SheafOfModules.Presentation.extensionRelationLeft {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) : free P₁.relations.I ⟶ CategoryTheory.Limits.kernel (extensionGeneratorsMap S P₁ P₃ h)

Equations

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

noncomputable def SheafOfModules.Presentation.extensionRelationRight {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : free P₃.relations.I ⟶ CategoryTheory.Limits.kernel (extensionGeneratorsMap S P₁ P₃ h)

Equations

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

noncomputable def SheafOfModules.Presentation.extensionRelationsMap {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : free (P₁.relations.I ⊕ P₃.relations.I) ⟶ CategoryTheory.Limits.kernel (extensionGeneratorsMap S P₁ P₃ h)

Equations

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

theorem SheafOfModules.Presentation.epi_extensionGeneratorsMap {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.Epi (extensionGeneratorsMap S P₁ P₃ h)

noncomputable def SheafOfModules.Presentation.extensionKernelToRightRelations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.Limits.kernel (extensionGeneratorsMap S P₁ P₃ h) ⟶ CategoryTheory.Limits.kernel P₃.generators.π

Equations

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

theorem SheafOfModules.Presentation.extensionRelationRight_comp_kernelToRightRelations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : CategoryTheory.CategoryStruct.comp (extensionRelationRight S hS P₁ P₃ h hh k hk) (extensionKernelToRightRelations S P₁ P₃ h hh) = P₃.relations.π

noncomputable def SheafOfModules.Presentation.extensionLeftRelationsToKernel {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) : CategoryTheory.Limits.kernel P₁.generators.π ⟶ CategoryTheory.Limits.kernel (extensionGeneratorsMap S P₁ P₃ h)

Equations

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

theorem SheafOfModules.Presentation.extensionLeftRelationsToKernel_comp_kernelToRightRelations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.CategoryStruct.comp (extensionLeftRelationsToKernel S P₁ P₃ h) (extensionKernelToRightRelations S P₁ P₃ h hh) = 0

noncomputable def SheafOfModules.Presentation.extensionKernelOfRightRelationsToLeftRelations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.Limits.kernel (extensionKernelToRightRelations S P₁ P₃ h hh) ⟶ CategoryTheory.Limits.kernel P₁.generators.π

Equations

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

theorem SheafOfModules.Presentation.extensionKernelOfRightRelationsToLeftRelations_comp {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : CategoryTheory.CategoryStruct.comp (extensionKernelOfRightRelationsToLeftRelations S hS P₁ P₃ h hh) (extensionLeftRelationsToKernel S P₁ P₃ h) = CategoryTheory.Limits.kernel.ι (extensionKernelToRightRelations S P₁ P₃ h hh)

theorem SheafOfModules.Presentation.extensionRelationLeft_eq {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) : extensionRelationLeft S P₁ P₃ h = CategoryTheory.CategoryStruct.comp P₁.relations.π (extensionLeftRelationsToKernel S P₁ P₃ h)

theorem SheafOfModules.Presentation.epi_extensionKernelToRightRelations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : CategoryTheory.Epi (extensionKernelToRightRelations S P₁ P₃ h hh)

theorem SheafOfModules.Presentation.epi_extensionRelationsMap {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : CategoryTheory.Epi (extensionRelationsMap S hS P₁ P₃ h hh k hk)

noncomputable def SheafOfModules.Presentation.extension {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) : S.X₂.Presentation

Equations

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

instance SheafOfModules.Presentation.extension_isFinite {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (S : CategoryTheory.ShortComplex (SheafOfModules R)) (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (k : free P₃.relations.I ⟶ free P₁.generators.I) (hk : CategoryTheory.CategoryStruct.comp k P₁.generators.π = correction S hS P₃ h hh) [P₁.IsFinite] [P₃.IsFinite] : (extension S hS P₁ P₃ h hh k hk).IsFinite

instance SheafOfModules.overFunctor_preservesZeroMorphisms {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (U : C) : (overFunctor R U).PreservesZeroMorphisms

theorem SheafOfModules.ShortExact.map_over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) (U : C) [CategoryTheory.HasWeakSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] : (S.map (overFunctor R U)).ShortExact

theorem SheafOfModules.Presentation.correction_mapOver {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (U : C) [(J.over U).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] (hhU : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) P₃.generators.I (overUnitIso U)).hom ((overFunctor R U).map h)) (S.map (overFunctor R U)).g = (P₃.mapOver U).generators.π) : CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) P₃.relations.I (overUnitIso U)).hom ((overFunctor R U).map (correction S hS P₃ h hh)) = correction (S.map (overFunctor R U)) ⋯ (P₃.mapOver U) (CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) P₃.generators.I (overUnitIso U)).hom ((overFunctor R U).map h)) hhU

theorem SheafOfModules.mapOver_lift_comp {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (P₃ : S.X₃.Presentation) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) (U : C) [(J.over U).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over U) AddCommGrpCat] [(J.over U).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R U)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R U) P₃.generators.I (overUnitIso U)).hom ((overFunctor R U).map h)) (S.map (overFunctor R U)).g = (P₃.mapOver U).generators.π

theorem SheafOfModules.localLift_comp_mapOver {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.Epi f] (P : N.Presentation) [P.IsFinite] (a : (X : C) × (simultaneousImageCover f P.generators.s X).Arrow) [(J.over a.snd.Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over a.snd.Y) AddCommGrpCat] [(J.over a.snd.Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R a.snd.Y)] : CategoryTheory.CategoryStruct.comp (localLift f P.generators.s a) ((overFunctor R a.snd.Y).map f) = (P.mapOver a.snd.Y).generators.π

theorem SheafOfModules.localLift_mapOver_generators_comp {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] {M : SheafOfModules R} (P : M.Presentation) {I : Type u} [Finite I] (s : I → M.sections) (a : (X : C) × (simultaneousImageCover P.generators.π s X).Arrow) [(J.over a.snd.Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [CategoryTheory.HasSheafify (J.over a.snd.Y) AddCommGrpCat] [(J.over a.snd.Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, u, u, u + 1, u + 1} (overFunctor R a.snd.Y)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (localLift P.generators.π s a) (mapFreeIso (overFunctor R a.snd.Y) P.generators.I (overUnitIso a.snd.Y)).inv) (P.mapOver a.snd.Y).generators.π = CategoryTheory.CategoryStruct.comp (mapFreeIso (overFunctor R a.snd.Y) I (overUnitIso a.snd.Y)).hom ((overFunctor R a.snd.Y).map (M.freeHomEquiv.symm s))

theorem SheafOfModules.instHasBinaryProductsOver_derivedAlgGeo_2 {C : Type u} [CategoryTheory.Category.{u, u} C] [CategoryTheory.Limits.HasPullbacks C] (X : C) : CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over X)

theorem SheafOfModules.IsFinitePresentation.middle_of_presentations_of_generatorLift {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [hasSheafComposeOver : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (hP₁ : P₁.IsFinite) (hP₃ : P₃.IsFinite) (h : free P₃.generators.I ⟶ S.X₂) (hh : CategoryTheory.CategoryStruct.comp h S.g = P₃.generators.π) : S.X₂.IsFinitePresentation

After the quotient generators have been lifted, one further finite cover lifts the correction relations and produces a finite presentation of the middle term.

theorem SheafOfModules.IsFinitePresentation.middle_of_presentations {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [hasSheafComposeOver : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafComposeOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) (P₁ : S.X₁.Presentation) (P₃ : S.X₃.Presentation) (hP₁ : P₁.IsFinite) (hP₃ : P₃.IsFinite) : S.X₂.IsFinitePresentation

The middle term of a short exact sequence has finite presentation when both endpoints have finite global presentations.

theorem SheafOfModules.IsFinitePresentation.middle_of_shortExact {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafComposeOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {S : CategoryTheory.ShortComplex (SheafOfModules R)} (hS : S.ShortExact) (h₁ : S.X₁.IsFinitePresentation) (h₃ : S.X₃.IsFinitePresentation) : S.X₂.IsFinitePresentation

Finite presentation of sheaves of modules is closed under extensions.

instance SheafOfModules.isFinitePresentation_isClosedUnderExtensions {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafComposeOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] : (isFinitePresentation R).IsClosedUnderExtensions