Generating sections from free epimorphisms

A family of generating sections of a module sheaf is equivalently packaged by an epimorphism from a free module sheaf. Mathlib provides the map from generating sections to such an epimorphism; this file records the converse construction, its finite-index instance, and the resulting recovery lemma.

These declarations require only a sheaf of rings on an arbitrary site. Geometric applications, such as finite generation on an affine chart, import this categorical owner directly.

Main results

• SheafOfModules.GeneratingSections.ofFreeEpi
• SheafOfModules.GeneratingSections.isFiniteType_ofFreeEpi
• SheafOfModules.GeneratingSections.ofFreeEpi_π

noncomputable def SheafOfModules.GeneratingSections.ofFreeEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u} (p : free I ⟶ M) [CategoryTheory.Epi p] : M.GeneratingSections

An epimorphism from a free sheaf of modules determines a family of generating sections.

Equations

• SheafOfModules.GeneratingSections.ofFreeEpi M p = { I := I, s := M.freeHomEquiv p, epi := ⋯ }

instance SheafOfModules.GeneratingSections.isFiniteType_ofFreeEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u} [Finite I] (p : free I ⟶ M) [CategoryTheory.Epi p] : (ofFreeEpi M p).IsFiniteType

A finite free source gives a finite family of generating sections.

@[simp]

theorem SheafOfModules.GeneratingSections.ofFreeEpi_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u} (p : free I ⟶ M) [CategoryTheory.Epi p] : (ofFreeEpi M p).π = p

ofFreeEpi recovers its defining epimorphism under GeneratingSections.π.

theorem SheafOfModules.GeneratingSections.isIso_ofEpi_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] [CategoryTheory.IsIso σ.π] [CategoryTheory.IsIso p] : CategoryTheory.IsIso (σ.ofEpi p).π

Pushing a free presentation forward along an isomorphism keeps it a free presentation: the presentation of σ.ofEpi p is σ.π ≫ p. Stated here, on a general ringed site, because the rewrite along ofEpi_π does not terminate in the default heartbeat budget once the sheaf carries scheme-level instances.