Finite locally free sheaves have finite local bases

Let R be a sheaf of commutative rings on a small site with pullbacks. A sheaf of R-modules is finite locally free if it is locally free and finitely presented (SheafOfModules.isFiniteLocallyFree). Local freeness alone provides local bases whose index types may be infinite and vary from chart to chart; finite type provides finitely many local generators on possibly different charts. This file shows that a locally free sheaf of finite type admits locally free data with finite local bases (SheafOfModules.IsLocallyFree.exists_isLocallyFreeData_isFiniteType), so that finite local freeness is equivalent to the existence of such data (SheafOfModules.isFiniteLocallyFree_iff_exists_isLocallyFreeData_isFiniteType), the form in which it is used to reduce statements about finite locally free sheaves to finite free sheaves.

The proof passes to a common refinement of the two covers, on which the sheaf is at once free on some index type I and generated by finitely many sections. If I is finite there is nothing to do. Otherwise the free sheaf on I receives an epimorphism from a finite free sheaf, and the degenerate case is that the sheaf of rings vanishes: an epimorphism free J ⟶ free K between finite free sheaves with |J| < |K| dualizes to a monomorphism free K ⟶ free J, whose sections over each object W give an injective R(W)-linear map R(W)^K → R(W)^J, so that R(W) is the zero ring by the strong rank condition (TauCeti.SheafOfModules.subsingleton_of_epi_free_of_card_lt). All sheaves of modules over a vanishing sheaf of rings are zero (TauCeti.SheafOfModules.isZero_of_forall_subsingleton), and the zero sheaf is free on the empty type.

Main declarations

• TauCeti.SheafOfModules.subsingleton_of_epi_free_of_card_lt: an epimorphism free J ⟶ free K with |J| < |K| forces the sheaf of rings to vanish;
• TauCeti.SheafOfModules.natCard_eq_of_iso_free: consequently, isomorphic finite free sheaves over a sheaf of rings with a nonzero ring of sections have index types of the same cardinality, which makes the rank of a finite locally free sheaf well defined;
• SheafOfModules.GeneratingSections.exists_isIso_π_isFiniteType: a sheaf of modules that is free and of finite type is free on a finite type;
• SheafOfModules.IsLocallyFree.exists_isLocallyFreeData_isFiniteType and SheafOfModules.isFiniteLocallyFree_iff_exists_isLocallyFreeData_isFiniteType: the characterization of finite locally free sheaves by finite local bases.

References

• The Stacks Project, Tag 01C6

theorem TauCeti.SheafOfModules.subsingleton_of_epi_free_of_card_lt {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I K : Type u} [Finite I] [Finite K] (f : SheafOfModules.free I ⟶ SheafOfModules.free K) [CategoryTheory.Epi f] (h : Nat.card I < Nat.card K) (W : Cᵒᵖ) : Subsingleton ↑((ringCatSheaf R).obj.obj W)

If there is an epimorphism free J ⟶ free K between free sheaves of modules on finite types with |J| < |K|, then the sheaf of rings vanishes: all its rings of sections are trivial.

theorem TauCeti.SheafOfModules.natCard_eq_of_iso_free {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I K : Type u} [Finite I] [Finite K] (e : SheafOfModules.free I ≅ SheafOfModules.free K) (W : Cᵒᵖ) [Nontrivial ↑((ringCatSheaf R).obj.obj W)] : Nat.card I = Nat.card K

Isomorphic free sheaves of modules on finite types have index types of the same cardinality, as soon as the sheaf of rings has one nonzero ring of sections.

theorem TauCeti.SheafOfModules.subsingleton_of_epi_free_of_infinite {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {I K : Type u} [Finite I] [Infinite K] (f : SheafOfModules.free I ⟶ SheafOfModules.free K) [CategoryTheory.Epi f] (W : Cᵒᵖ) : Subsingleton ↑((ringCatSheaf R).obj.obj W)

If there is an epimorphism from a free sheaf of modules on a finite type to the free sheaf of modules on an infinite type, then the sheaf of rings vanishes.

theorem SheafOfModules.GeneratingSections.exists_isIso_π_isFiniteType {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (σ τ : N.GeneratingSections) [hσ : CategoryTheory.IsIso σ.π] [hτ : τ.IsFiniteType] : ∃ (ρ : N.GeneratingSections), CategoryTheory.IsIso ρ.π ∧ ρ.IsFiniteType

A sheaf of modules which is free, on a possibly infinite index type, and generated by finitely many sections is free on a finite type. If the given basis is infinite, the sheaf of rings vanishes and the sheaf is free on the empty type.

theorem SheafOfModules.IsLocallyFree.exists_isLocallyFreeData_isFiniteType {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasPullbacks C] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) [M.IsLocallyFree] [M.IsFiniteType] : ∃ (q : M.LocalGeneratorsData), q.IsLocallyFreeData ∧ q.IsFiniteType

A locally free sheaf of modules of finite type admits locally free data with finite local bases.

theorem SheafOfModules.isFiniteLocallyFree_iff_exists_isLocallyFreeData_isFiniteType {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasPullbacks C] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : isFiniteLocallyFree (TauCeti.SheafOfModules.ringCatSheaf R) M ↔ ∃ (q : M.LocalGeneratorsData), q.IsLocallyFreeData ∧ q.IsFiniteType

A sheaf of modules is finite locally free, that is, locally free and finitely presented, if and only if it admits locally free data with finite local bases.