Restricting presentations to over sites

Presentations, finite generating families, and quasicoherent presentation data for a sheaf of modules on an arbitrary ringed site restrict to slice sites. The direct restriction first lands on an iterated slice; Over.iteratedSliceEquiv and SheafOfModules.pushforwardPushforwardEquivalence identify it with restriction to the domain object.

Nothing in this construction requires a scheme or a topological space. Affine and coherent-sheaf arguments import this module and add their geometric cover or finiteness input.

Main results

• SheafOfModules.Presentation.over restricts one presentation along an object of a slice site;
• SheafOfModules.GeneratingSections.over restricts a family of generating sections and preserves finiteness of its index;
• SheafOfModules.QuasicoherentData.over restricts a full family of local presentations.

noncomputable def SheafOfModules.Presentation.over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] {M : SheafOfModules R} {U : C} (P : (M.over U).Presentation) (W : CategoryTheory.Over U) [CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over U)] : (M.over W.left).Presentation

Restrict a presentation on U along an object W ⟶ U of the slice site.

The direct restriction has target ((M.over U).over W).Presentation; the iterated-slice equivalence identifies that target with (M.over W.left).Presentation.

Equations

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

noncomputable def SheafOfModules.GeneratingSections.over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] {M : SheafOfModules R} {U : C} (σ : (M.over U).GeneratingSections) (W : CategoryTheory.Over U) [CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over U)] : (M.over W.left).GeneratingSections

Restrict generating sections on U along an object W ⟶ U of the slice site.

Equations

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

instance SheafOfModules.GeneratingSections.isFiniteType_over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] {M : SheafOfModules R} {U : C} (σ : (M.over U).GeneratingSections) [σ.IsFiniteType] (W : CategoryTheory.Over U) [CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over U)] : (σ.over W).IsFiniteType

Restriction to a nested slice preserves finite generation.

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

noncomputable def SheafOfModules.QuasicoherentData.presentationOver {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (q : M.QuasicoherentData) (U : C) (i : q.I) : ((M.over U).over ((CategoryTheory.Over.star U).obj (q.X i))).Presentation

Restrict one of the presentations in q to the product with U.

Equations

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

@[simp]

theorem SheafOfModules.QuasicoherentData.presentationOver_generators_I {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (q : M.QuasicoherentData) (U : C) (i : q.I) : (q.presentationOver U i).generators.I = (q.presentation i).generators.I

@[simp]

theorem SheafOfModules.QuasicoherentData.presentationOver_relations_I {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (q : M.QuasicoherentData) (U : C) (i : q.I) : (q.presentationOver U i).relations.I = (q.presentation i).relations.I

noncomputable def SheafOfModules.QuasicoherentData.over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [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] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (q : M.QuasicoherentData) (U : C) : (M.over U).QuasicoherentData

Restrict local presentation data to an object of the site. The new cover consists of the products of the old covering objects with the object of restriction.

Equations

• q.over U = { I := q.I, X := fun (i : q.I) => (CategoryTheory.Over.star U).obj (q.X i), coversTop := ⋯, presentation := fun (i : q.I) => q.presentationOver U i }