Refining quasi-coherent data

Quasi-coherent data for a sheaf of modules M consists of a covering family X i together with a presentation of each restriction M.over (X i). Given a second covering family Y j refining the first one, meaning that each Y j comes with an arrow to some X i, restricting the presentations along these arrows gives quasi-coherent data for M on the family Y j.

Restriction along an arrow f : Y ⟶ X is Mathlib's SheafOfModules.overMap. On a site with pullbacks it is a left adjoint, so it maps presentations to presentations (SheafOfModules.Presentation.map); SheafOfModules.overFunctorMap identifies the restriction of M.over X with M.over Y.

The same restriction applies to local generators (SheafOfModules.LocalGeneratorsData), and it preserves local freeness and finiteness of the generating families. Both restriction along an arrow and the transport of the next paragraph are instances of one construction, SheafOfModules.GeneratingSections.mapIso, from the lower-level generating-sections transport module: generating sections are carried along a colimit-preserving functor by Mathlib's SheafOfModules.GeneratingSections.map and then read through an isomorphism by SheafOfModules.GeneratingSections.equivOfIso.

This lets two quasi-coherent sheaves be presented on a common refinement of their covers, which is how the tensor product and the biproduct of quasi-coherent sheaves are shown to be quasi-coherent.

Restricting a presentation preserves finiteness, and it preserves presentations whose generating morphism is an isomorphism, that is, presentations exhibiting a free sheaf. Hence refining finite quasi-coherent data or locally free data gives data of the same kind.

Main declarations

• SheafOfModules.QuasicoherentData.ofRefinement;
• SheafOfModules.QuasicoherentData.isIso_ofRefinement_presentation_generators_π: refinement preserves presentations with an invertible generating morphism;
• SheafOfModules.LocalGeneratorsData.ofRefinement.

theorem SheafOfModules.GeneratingSections.isIso_ofEpi_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.IsIso p] (h : CategoryTheory.IsIso σ.π) : CategoryTheory.IsIso (σ.ofEpi p).π

Generating sections pushed forward along an isomorphism exhibit a free sheaf if the original ones do.

theorem SheafOfModules.Presentation.isIso_ofIsIso_generators_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (f : M ⟶ N) [hf : CategoryTheory.IsIso f] (σ : M.Presentation) (h : CategoryTheory.IsIso σ.generators.π) : CategoryTheory.IsIso (ofIsIso f σ).generators.π

A presentation transported along an isomorphism has an invertible generating morphism if the original one does.

instance SheafOfModules.Presentation.isFinite_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [CategoryTheory.HasSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : unit S ≅ F.obj (unit R)) [P.IsFinite] : (P.map F η).IsFinite

The image of a finite presentation under a colimit-preserving functor is finite.

theorem SheafOfModules.Presentation.isIso_map_generators_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K RingCat} [CategoryTheory.HasSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : unit S ≅ F.obj (unit R)) (h : CategoryTheory.IsIso P.generators.π) : CategoryTheory.IsIso (P.map F η).generators.π

The image under a colimit-preserving functor of a presentation with an invertible generating morphism has an invertible generating morphism.

noncomputable def SheafOfModules.QuasicoherentData.ofRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : M.QuasicoherentData

Quasi-coherent data for M transported to a refining covering family Y: each Y i maps to the member q.X (index i) of the original cover by map i, and the presentation of M.over (Y i) is the restriction of the presentation of M.over (q.X (index i)) along map i.

Equations

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

@[simp]

theorem SheafOfModules.QuasicoherentData.ofRefinement_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (a✝ : I) : (q.ofRefinement Y coversTop index map).X a✝ = Y a✝

@[simp]

theorem SheafOfModules.QuasicoherentData.ofRefinement_presentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (i : I) : (q.ofRefinement Y coversTop index map).presentation i = Presentation.ofIsIso ((overFunctorMap R (map i)).hom.app M) ((q.presentation (index i)).map (overMap R (map i)) (overMapUnitIso (map i)).symm)

@[simp]

theorem SheafOfModules.QuasicoherentData.ofRefinement_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : (q.ofRefinement Y coversTop index map).I = I

noncomputable def SheafOfModules.LocalGeneratorsData.ofRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : M.LocalGeneratorsData

Local generators for M transported to a refining covering family Y: each Y i maps to the member q.X (index i) of the original cover by map i, and the generators of M.over (Y i) are the restrictions of the generators of M.over (q.X (index i)) along map i.

Equations

• q.ofRefinement Y coversTop index map = { I := I, X := Y, coversTop := coversTop, generators := fun (i : I) => (q.generators (index i)).restrict (map i) }

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofRefinement_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (i : I) : (q.ofRefinement Y coversTop index map).generators i = (q.generators (index i)).restrict (map i)

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofRefinement_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (a✝ : I) : (q.ofRefinement Y coversTop index map).X a✝ = Y a✝

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofRefinement_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : (q.ofRefinement Y coversTop index map).I = I

instance TauCeti.SheafOfModules.instIsLocallyFreeDataOfRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : (q.ofRefinement Y coversTop index map).IsLocallyFreeData

Restricting locally free data to a refinement gives locally free data.

instance TauCeti.SheafOfModules.instIsFiniteTypeOfRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsFiniteType] {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : (q.ofRefinement Y coversTop index map).IsFiniteType

Restricting local generators of finite type to a refinement gives local generators of finite type.

theorem SheafOfModules.QuasicoherentData.isIso_ofRefinement_presentation_generators_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (i : I) (h : CategoryTheory.IsIso (q.presentation (index i)).generators.π) : CategoryTheory.IsIso ((q.ofRefinement Y coversTop index map).presentation i).generators.π

Refining quasi-coherent data preserves presentations with an invertible generating morphism.

theorem SheafOfModules.QuasicoherentData.isFinite_ofRefinement_presentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) [q.IsFinitePresentation] {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) (i : I) : ((q.ofRefinement Y coversTop index map).presentation i).IsFinite

Refining finite quasi-coherent data gives finite presentations.

instance TauCeti.SheafOfModules.instIsFinitePresentationOfRefinement {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) [q.IsFinitePresentation] {I : Type w} (Y : I → C) (coversTop : J.CoversTop Y) (index : I → q.I) (map : (i : I) → Y i ⟶ q.X (index i)) : (q.ofRefinement Y coversTop index map).IsFinitePresentation

Refining finite quasi-coherent data gives finite quasi-coherent data.