Locally Free Sheaves

A sheaf of modules is locally free if it is locally isomorphic to a free module.

Main Definitions

• SheafOfModules.LocalGeneratorsData.IsLocallyFreeData: This is defined as a predicate on SheafOfModules.LocalGeneratorData where q : M.LocalGeneratorData is said to be locally free data if (q.generators i).π is an isomorphism for all i in q.I.

• SheafOfModules.IsLocallyFree: M : SheafOfModules R is locally free is there exists locally free data for it.

class SheafOfModules.LocalGeneratorsData.IsLocallyFreeData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (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 q is locally free data if all of the natural morphisms free (q.generators i).I ⟶ M.over (q.X i) are isomorphisms.

• isIso (i : q.I) : CategoryTheory.IsIso (q.generators i).π

instance SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.shrink {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : q.shrink.IsLocallyFreeData

class SheafOfModules.IsLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop

A sheaf of modules is locally free if it is locally isomorphic to free sheaves: There exist local generators satisfying IsLocallyFreeData.

• exists_isLocallyFreeData : ∃ (q : M.LocalGeneratorsData), q.IsLocallyFreeData

theorem SheafOfModules.LocalGeneratorsData.isLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : M.IsLocallyFree

noncomputable def SheafOfModules.free.generatingSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : (free I).GeneratingSections

The generating sections of the free sheaf of modules.

Equations

• SheafOfModules.free.generatingSections I = { I := I, s := fun (i : I) => SheafOfModules.freeSection i, epi := ⋯ }

@[simp]

theorem SheafOfModules.free.generatingSections_s {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) (i : I) : (generatingSections I).s i = freeSection i

@[simp]

theorem SheafOfModules.free.generatingSections_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : (generatingSections I).I = I

@[simp]

theorem SheafOfModules.free.generatingSections_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : (generatingSections I).π = CategoryTheory.CategoryStruct.id (free I)

instance SheafOfModules.instIsIsoπGeneratingSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : CategoryTheory.IsIso (free.generatingSections I).π

instance SheafOfModules.instIsLocallyFreeDataLocalGeneratorsDataGeneratingSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : (free.generatingSections I).localGeneratorsData.IsLocallyFreeData

instance SheafOfModules.instIsLocallyFreeFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : (free I).IsLocallyFree

def SheafOfModules.LocalGeneratorsData.quasiCoherentData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : M.QuasicoherentData

Given locally free data, this is the QuasiCoherentData where there are no relations.

Equations

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

@[simp]

theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_presentation_relations_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (i : q.I) : (q.quasiCoherentData.presentation i).relations.I = ULift.{u, 0} Empty

@[simp]

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

@[simp]

theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (a✝ : q.I) : q.quasiCoherentData.X a✝ = q.X a✝

@[simp]

theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_I {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : q.quasiCoherentData.I = q.I

@[simp]

theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_presentation_relations_s {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (i : q.I) (j : ULift.{u, 0} Empty) : (q.quasiCoherentData.presentation i).relations.s j = Empty.rec (fun (x : Empty) => (CategoryTheory.Limits.kernel (q.generators i).π).sections) j.down

@[simp]

theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_localGeneratorsData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] : q.quasiCoherentData.localGeneratorsData = q

@[instance 100]

instance SheafOfModules.instIsQuasicoherentOfIsLocallyFree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [h : M.IsLocallyFree] : M.IsQuasicoherent