theorem
QuasicoherentData.bind_isFinitePresentation
{C : Type u}
[CategoryTheory.Category.{u, 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)
(hD : ∀ (i : I), (D i).IsFinitePresentation)
:
Glueing finite-presentation quasicoherent data along a covering: if every local
piece D i is finitely presented, so is their bind.
theorem
QuasicoherentData.bind_localGeneratorsData_isFiniteType
{C : Type u}
[CategoryTheory.Category.{u, 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)
(hD : ∀ (i : I) (j : (D i).I), ((D i).presentation j).generators.IsFiniteType)
:
Glueing finite-type generators data: locally finite-type generators glue to a globally finite-type generators datum.
theorem
IsFinitePresentation.of_coversTop
{C : Type u}
[CategoryTheory.Category.{u, 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)).IsFinitePresentation]
:
Local-to-global: if M restricted to each X i is finitely presented and the
X i form a covering, then M is finitely presented.
theorem
IsFiniteType.of_coversTop_of_isFinitePresentation
{C : Type u}
[CategoryTheory.Category.{u, 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)).IsFinitePresentation]
:
Local-to-global (instance form): finite presentation locally implies finite type globally on a covering.
theorem
IsFiniteType.of_coversTop_of_isFinitePresentation'
{C : Type u}
[CategoryTheory.Category.{u, 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)
(hFP : ∀ (i : I), (M.over (X i)).IsFinitePresentation)
:
Same as IsFiniteType.of_coversTop_of_isFinitePresentation, taking the
finite-presentation hypothesis as an explicit argument rather than a typeclass.