Locally free sheaves of modules

Let R be a sheaf of commutative rings on a small site with pullbacks. If M and N are locally free sheaves of R-modules, then so is M ⊗ N: on a common refinement of covers on which M and N are free, the restriction of M ⊗ N is the tensor product of two free sheaves, which is free on the product of the index types. If the site also has binary products, the unit is free on one generator, so local freeness is a monoidal property of sheaves of modules. Together with the corresponding result for finite presentation (TauCeti.SheafOfModules.isMonoidal_isFinitePresentation), this shows that finite locally free sheaves of modules form a monoidal full subcategory (ObjectProperty.fullMonoidalSubcategory). In appropriate geometric settings, these are the sheaves of sections of vector bundles.

Finite locally free sheaves also contain the zero sheaf (the free sheaf on the empty type) and are closed under direct sums, hence under finite products, so they form an additive full subcategory.

Local freeness is also shown to be invariant under isomorphism, by transporting local bases along an isomorphism (SheafOfModules.LocalGeneratorsData.ofIsIso).

Finally, local freeness descends along a covering family: local bases chosen after restricting to every member of a covering family can be combined into local bases on the original site. This descent construction is adapted from Brian Nugent's implementation.

Main declarations

• SheafOfModules.isLocallyFree: local freeness as an ObjectProperty; it is closed under isomorphisms;
• TauCeti.SheafOfModules.isLocallyFree_tensorObj: M ⊗ N is locally free when M and N are;
• TauCeti.SheafOfModules.isMonoidal_isLocallyFree: local freeness is an ObjectProperty.IsMonoidal;
• SheafOfModules.isFiniteLocallyFree: the property of being locally free and finitely presented, and TauCeti.SheafOfModules.isMonoidal_isFiniteLocallyFree: it is an ObjectProperty.IsMonoidal;
• SheafOfModules.LocalGeneratorsData.bind combines local-generator atlases over a cover, and SheafOfModules.IsLocallyFree.of_coversTop shows that local freeness descends from a cover;
• TauCeti.SheafOfModules.containsZero_isFiniteLocallyFree and TauCeti.SheafOfModules.isClosedUnderFiniteProducts_isFiniteLocallyFree: finite locally free sheaves contain a zero object and are closed under finite products.

References

• The Stacks Project, Tag 01C6

noncomputable def SheafOfModules.LocalGeneratorsData.ofIsIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (q : M.LocalGeneratorsData) : N.LocalGeneratorsData

Local generators data transported along an isomorphism f : M ⟶ N: the covering family is unchanged, and the generating sections of M.over (q.X i) are pushed forward along the restriction of f.

Equations

• SheafOfModules.LocalGeneratorsData.ofIsIso f q = { I := q.I, X := q.X, coversTop := ⋯, generators := fun (i : q.I) => (q.generators i).ofEpi (SheafOfModules.Hom.over f (q.X i)) }

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofIsIso_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (q : M.LocalGeneratorsData) : (ofIsIso f q).I = q.I

Transporting local generators preserves the cover's index type.

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofIsIso_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (q : M.LocalGeneratorsData) : (ofIsIso f q).X = fun (i : (ofIsIso f q).I) => q.X (⋯.mp i)

Transporting local generators preserves the covering objects.

@[simp]

theorem SheafOfModules.LocalGeneratorsData.ofIsIso_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (q : M.LocalGeneratorsData) (i : (ofIsIso f q).I) : (ofIsIso f q).generators i = cast ⋯ ((q.generators (⋯.mp i)).ofEpi (Hom.over f (q.X (⋯.mp i))))

Transporting local generators pushes each generating family along the restricted isomorphism.

instance TauCeti.SheafOfModules.instIsLocallyFreeDataOfIsIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : (SheafOfModules.LocalGeneratorsData.ofIsIso f q).IsLocallyFreeData

Locally free data transported along an isomorphism is locally free data.

@[reducible, inline]

abbrev SheafOfModules.isLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.ObjectProperty (SheafOfModules R)

Local freeness of sheaves of modules, as a property of objects.

Equations

• SheafOfModules.isLocallyFree R = SheafOfModules.IsLocallyFree

instance TauCeti.SheafOfModules.instIsClosedUnderIsomorphismsSheafOfModulesIsLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : (SheafOfModules.isLocallyFree R).IsClosedUnderIsomorphisms

Local freeness is invariant under isomorphism.

theorem SheafOfModules.LocalGeneratorsData.isIso_quasiCoherentData_presentation_generators_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (i : q.I) : CategoryTheory.IsIso (q.quasiCoherentData.presentation i).generators.π

The quasi-coherent data associated with locally free data presents each restriction by the free sheaf on its local basis.

@[reducible, inline]

abbrev SheafOfModules.isFiniteLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.ObjectProperty (SheafOfModules R)

A sheaf of modules is finite locally free if it is locally free and finitely presented.

Equations

• SheafOfModules.isFiniteLocallyFree R = SheafOfModules.isLocallyFree R ⊓ SheafOfModules.isFinitePresentation R

noncomputable def SheafOfModules.LocalGeneratorsData.bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) : M.LocalGeneratorsData

Combine local-generator atlases on the restrictions of M to a covering family.

The resulting atlas is indexed by a covering object and then by a member of the atlas chosen on its slice, and its generators are the chosen ones, read off the iterated slice by SheafOfModules.GeneratingSections.ofIteratedSlice.

Equations

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

@[simp]

theorem SheafOfModules.LocalGeneratorsData.bind_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) : (bind X hX D).I = ((i : I) × (D i).I)

Combining local-generator atlases indexes the cover by a covering object and a member of the atlas chosen on its slice.

@[simp]

theorem SheafOfModules.LocalGeneratorsData.bind_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) : (bind X hX D).X = fun (i : (bind X hX D).I) => ((D (⋯.mp i).fst).X (⋯.mp i).snd).left

The covering objects of a combined atlas are the underlying objects of the chosen slices.

@[simp]

theorem SheafOfModules.LocalGeneratorsData.bind_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) (i : (bind X hX D).I) : (bind X hX D).generators i = cast ⋯ ((D (⋯.mp i).fst).generators (⋯.mp i).snd).ofIteratedSlice

The generators in a combined atlas are those from the chosen slice atlas, transported off the iterated slice.

instance SheafOfModules.LocalGeneratorsData.isLocallyFreeData_bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) [∀ (i : I), (D i).IsLocallyFreeData] : (bind X hX D).IsLocallyFreeData

Combining locally free atlases over a cover produces locally free data on the original site.

instance SheafOfModules.LocalGeneratorsData.isFiniteType_bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).LocalGeneratorsData) [∀ (i : I), (D i).IsFiniteType] : (bind X hX D).IsFiniteType

Combining finite-type local-generator atlases over a cover preserves finite type.

theorem SheafOfModules.IsLocallyFree.of_coversTop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u_1} (X : I → C) (hX : J.CoversTop X) [∀ (i : I), (M.over (X i)).IsLocallyFree] : M.IsLocallyFree

If a sheaf of modules is locally free after restriction to every member of a covering family, then it is locally free.

instance TauCeti.SheafOfModules.isClosedUnderBinaryProducts_isFiniteLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : (SheafOfModules.isFiniteLocallyFree R).IsClosedUnderBinaryProducts

Finite locally free sheaves of modules are closed under binary products, which are the direct sums M ⊞ N.

instance TauCeti.SheafOfModules.containsZero_isFiniteLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isFiniteLocallyFree R).ContainsZero

The zero sheaf of modules is finite locally free, being the free sheaf on the empty type.

instance TauCeti.SheafOfModules.isClosedUnderFiniteProducts_isFiniteLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isFiniteLocallyFree R).IsClosedUnderFiniteProducts

Finite locally free sheaves of modules are closed under finite products, which are the finite direct sums.

instance TauCeti.SheafOfModules.isLocallyFree_tensorObj {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (ringCatSheaf R)} [M.IsLocallyFree] [N.IsLocallyFree] : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).IsLocallyFree

The tensor product of two locally free sheaves of modules is locally free.

instance TauCeti.SheafOfModules.isMonoidal_isLocallyFree {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isLocallyFree (ringCatSheaf R)).IsMonoidal

Local freeness of sheaves of modules is a monoidal property: the unit is locally free and locally free sheaves are closed under tensor products.

instance TauCeti.SheafOfModules.isMonoidal_isFiniteLocallyFree {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isFiniteLocallyFree (ringCatSheaf R)).IsMonoidal

Finite local freeness of sheaves of modules is a monoidal property. Hence finite locally free sheaves of modules form a monoidal full subcategory.