Invertible sheaves of modules on a ringed site

This file defines an invertible sheaf of modules intrinsically as a sheaf that is locally free of rank one. The definition and its local trivializations use only a sheaf of rings on an arbitrary Grothendieck site; scheme Picard groups and tensor products are downstream consumers.

Main declarations

• SheafOfModules.LocalGeneratorsData.IsRankOne: every local basis is a singleton;
• SheafOfModules.IsInvertible: local freeness of rank one;
• SheafOfModules.LocalGeneratorsData.rankOneTrivialization: the resulting local identification with the unit sheaf;
• SheafOfModules.IsInvertible.of_trivializations: reconstruction from a covering family of local trivializations.

noncomputable def SheafOfModules.freePUnitIsoUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : free PUnit.{u + 1} ≅ unit R

A free sheaf on one generator is the unit sheaf.

Equations

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

def SheafOfModules.LocalGeneratorsData.IsRankOne {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} (q : M.LocalGeneratorsData) : Prop

Local generator data has rank one when every local basis index is a singleton.

Equations

• q.IsRankOne = ∀ (i : q.I), Nonempty (q.generators i).I ∧ Subsingleton (q.generators i).I

noncomputable def SheafOfModules.LocalGeneratorsData.ofIso {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} (q : M.LocalGeneratorsData) (e : M ≅ N) : N.LocalGeneratorsData

Transport local generator data across an isomorphism.

Equations

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

instance SheafOfModules.LocalGeneratorsData.instIsLocallyFreeDataOfIso {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} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (e : M ≅ N) : (q.ofIso e).IsLocallyFreeData

theorem SheafOfModules.LocalGeneratorsData.isRankOne_ofIso {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} (q : M.LocalGeneratorsData) (e : M ≅ N) (h : q.IsRankOne) : (q.ofIso e).IsRankOne

Transporting local generator data along an isomorphism preserves the rank-one condition.

class SheafOfModules.IsInvertible {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) : Prop

An invertible sheaf is locally free of rank one.

• exists_rankOneData : ∃ (q : M.LocalGeneratorsData), q.IsLocallyFreeData ∧ q.IsRankOne

@[instance 90]

instance SheafOfModules.instIsLocallyFreeOfIsInvertible {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) [h : M.IsInvertible] : M.IsLocallyFree

theorem SheafOfModules.IsInvertible.ofIso {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} [M.IsInvertible] (e : M ≅ N) : N.IsInvertible

Invertibility is invariant under isomorphism of module sheaves.

theorem SheafOfModules.IsInvertible.isFinitePresentation {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} [M.IsInvertible] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] : M.IsFinitePresentation

An invertible sheaf is finitely presented: its rank-one local bases give presentations with one generator and no relations.

instance SheafOfModules.instIsInvertibleFreePUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] : (free PUnit.{u + 1}).IsInvertible

instance SheafOfModules.instIsInvertibleUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] : (unit R).IsInvertible

noncomputable def SheafOfModules.LocalGeneratorsData.rankOneTrivialization {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} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) (i : q.I) : unit (R.over (q.X i)) ≅ M.over (q.X i)

The local trivialization determined by rank-one locally free generator data.

Equations

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

noncomputable def SheafOfModules.LocalGeneratorsData.rankOneTrivializationOver {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} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) (i : q.I) {Y : C} (f : Y ⟶ q.X i) : unit (R.over Y) ≅ M.over Y

Restrict a rank-one trivialization from a cover member to an object over it.

Equations

• q.rankOneTrivializationOver hq i f = (SheafOfModules.overMapUnitIso f).symm ≪≫ (SheafOfModules.overMap R f).mapIso (q.rankOneTrivialization hq i) ≪≫ (SheafOfModules.overFunctorMap R f).app M

theorem SheafOfModules.IsInvertible.of_trivializations {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} {I : Type u₁} (Y : I → C) (hY : J.CoversTop Y) (e : (i : I) → unit (R.over (Y i)) ≅ M.over (Y i)) : M.IsInvertible

A sheaf locally isomorphic to the structure sheaf on a covering family is invertible.