Isomorphism invariance of finite presentation

Finite local presentation data for a sheaf of modules on an arbitrary ringed site transports across an isomorphism. Consequently, finite presentation defines an isomorphism-closed object property on the category of module sheaves.

Main results

• SheafOfModules.QuasicoherentData.ofIso transports local presentation data;
• SheafOfModules.IsFinitePresentation.of_iso preserves finite presentation;
• SheafOfModules.isFinitePresentation_isClosedUnderIsomorphisms packages the result as an isomorphism-closed object property.

noncomputable def SheafOfModules.QuasicoherentData.ofIso {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafify : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafify : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijective : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.QuasicoherentData) (e : M ≅ N) : N.QuasicoherentData

Transport local presentation data across an isomorphism of sheaves of modules.

This is the project-facing, iso-valued wrapper around Mathlib's QuasicoherentData.ofIsIso.

Equations

• q.ofIso e = SheafOfModules.QuasicoherentData.ofIsIso e.hom q

instance SheafOfModules.QuasicoherentData.isFinitePresentation_ofIso {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafify : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafify : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijective : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.QuasicoherentData) (e : M ≅ N) [q.IsFinitePresentation] : (q.ofIso e).IsFinitePresentation

theorem SheafOfModules.IsFinitePresentation.of_iso {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafify : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafify : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijective : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (e : M ≅ N) (hM : M.IsFinitePresentation) : N.IsFinitePresentation

Finite presentation is preserved by an isomorphism of sheaves of modules.

instance SheafOfModules.isFinitePresentation_isClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafify : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafify : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijective : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : (isFinitePresentation R).IsClosedUnderIsomorphisms