Invertible sheaves of modules

Mathlib's SheafOfModules.IsLocallyFree remembers local generating families but deliberately allows their ranks to vary. This file refines that local data by requiring each local generating type to have exactly one element, which is the site-level content of being locally free of rank one. Nothing here is specific to schemes, so everything is stated for a sheaf of modules over an arbitrary site.

Main declarations

• TauCeti.SheafOfModules.LocalGeneratorsData.IsInvertible q says that every presentation free (q.generators i).I ⟶ M.over (q.X i) is an isomorphism and that each indexing type is nonempty and a subsingleton;
• TauCeti.SheafOfModules.IsInvertible M says that such data exists for the sheaf of modules M;
• TauCeti.SheafOfModules.LocalGeneratorsData.ofIso transports local generator data along an isomorphism of sheaves of modules, and TauCeti.SheafOfModules.IsInvertible.of_iso transports invertibility along one.

The predicate implies Mathlib's local freeness (and hence quasi-coherence). Every free sheaf whose indexing type is nonempty and a subsingleton is invertible.

The scheme-level packaging, where such a sheaf is an invertible sheaf on a scheme, is in TauCeti/AlgebraicGeometry/LineBundle/Basic.lean. This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗". No formalization is vendored. The construction reuses Mathlib's SheafOfModules.LocalGeneratorsData, IsLocallyFreeData, and IsLocallyFree API from Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree.

structure TauCeti.SheafOfModules.LocalGeneratorsData.IsInvertible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) : Prop

Local generators exhibit a sheaf of modules as invertible when they freely generate it on a cover and every local generating type has exactly one element.

• isLocallyFreeData : q.IsLocallyFreeData

  The local generators freely generate the restricted sheaf.

• basisNonempty (i : q.I) : Nonempty (q.generators i).I

  Every local free basis has at least one element.

• basisSubsingleton (i : q.I) : Subsingleton (q.generators i).I

  Every local free basis has at most one element.

class TauCeti.SheafOfModules.IsInvertible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop

A sheaf of modules is invertible if it is locally free of rank one. The witness is local generator data whose free presentations are isomorphisms and whose basis types have exactly one element.

• exists_isInvertible : ∃ (q : M.LocalGeneratorsData), LocalGeneratorsData.IsInvertible q

  A rank-one local trivialization of the sheaf.

instance TauCeti.SheafOfModules.IsInvertible.isLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [h : IsInvertible M] : M.IsLocallyFree

An invertible sheaf is locally free.

noncomputable def TauCeti.SheafOfModules.LocalGeneratorsData.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.LocalGeneratorsData) (e : M ≅ N) : N.LocalGeneratorsData

Transport local generator data along an isomorphism of sheaves of modules: the same cover, with each family of local generators pushed forward along the restricted isomorphism.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.LocalGeneratorsData.ofIso_generators {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.LocalGeneratorsData) (e : M ≅ N) (i : q.I) : (ofIso q e).generators i = (q.generators i).ofEpi ((SheafOfModules.overFunctor R (q.X i)).mapIso e).hom

@[simp]

theorem TauCeti.SheafOfModules.LocalGeneratorsData.ofIso_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.LocalGeneratorsData) (e : M ≅ N) (a✝ : q.I) : (ofIso q e).X a✝ = q.X a✝

@[simp]

theorem TauCeti.SheafOfModules.LocalGeneratorsData.ofIso_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (q : M.LocalGeneratorsData) (e : M ≅ N) : (ofIso q e).I = q.I

theorem TauCeti.SheafOfModules.LocalGeneratorsData.IsInvertible.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} {q : M.LocalGeneratorsData} (hq : IsInvertible q) (e : M ≅ N) : IsInvertible (LocalGeneratorsData.ofIso q e)

Rank-one local generator data stays rank one after transport along an isomorphism.

theorem TauCeti.SheafOfModules.IsInvertible.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (e : M ≅ N) [h : IsInvertible M] : IsInvertible N

Invertibility transports along an isomorphism of sheaves of modules.

instance TauCeti.SheafOfModules.free_isInvertible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasWeakSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (Y : C), CategoryTheory.HasSheafify (J.over Y) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] (I : Type u) [Nonempty I] [Subsingleton I] : IsInvertible (SheafOfModules.free I)

A free sheaf whose indexing type has exactly one element is an invertible sheaf.