The underlying abelian sheaf of a sheaf of modules on a scheme #

Mathlib packages the forgetful functors out of the category X.Modules of 𝒪_X-modules on a scheme that land in presheaves: AlgebraicGeometry.Scheme.Modules.toPresheafOfModules and AlgebraicGeometry.Scheme.Modules.toPresheaf. This file adds the conversion of sheaf-level isomorphisms back to 𝒪_X-module isomorphisms, the one that lands in abelian sheaves, and records that the latter is exact.

Main declarations #

TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf, the functor sending an 𝒪_X-module to its underlying sheaf of abelian groups, with instances saying that it is additive and preserves finite limits and finite colimits;
TauCeti.AlgebraicGeometry.Scheme.Modules.isoOfSheafIso, which lifts an isomorphism of underlying sheaves of modules to an isomorphism in X.Modules;
AlgebraicGeometry.Scheme.Modules.sectionsLinearEquiv, the Γ(X, U)-linear equivalence of sections over U induced by an isomorphism of 𝒪_X-modules;
TauCeti.AlgebraicGeometry.Scheme.Modules.shortExact_map_toSheaf: a short exact sequence of 𝒪_X-modules stays short exact after forgetting the module structures.

TauCeti/AlgebraicGeometry/Cohomology/Basic.lean defines the cohomology of an 𝒪_X-module as the sheaf cohomology of its underlying abelian sheaf, so this exactness is what puts that cohomology into a long exact sequence; it is Layer B infrastructure for TauCetiRoadmap/JacobianChallenge/README.md. No formalization is vendored: the functor is Mathlib's SheafOfModules.toSheaf for the sheaf of rings X.ringCatSheaf, and its exactness is TauCeti/Algebra/Category/ModuleCat/Sheaf/Exactness.lean.

source

def AlgebraicGeometry.Scheme.Modules.isoOfSheafIso (X : Scheme) {M N : X.Modules} (e : M ≅ N) :

M ≅ N

Convert an isomorphism of sheaves of modules into an isomorphism of 𝒪_X-modules.

Equations

AlgebraicGeometry.Scheme.Modules.isoOfSheafIso X e = { hom := { val := e.hom.val }, inv := { val := e.inv.val }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.isoOfSheafIso_hom_val (X : Scheme) {M N : X.Modules} (e : M ≅ N) :

(isoOfSheafIso X e).hom.val = e.hom.val

source

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.isoOfSheafIso_inv_val (X : Scheme) {M N : X.Modules} (e : M ≅ N) :

(isoOfSheafIso X e).inv.val = e.inv.val

source

noncomputable def AlgebraicGeometry.Scheme.Modules.sectionsLinearEquiv {X : Scheme} {M N : X.Modules} (e : M ≅ N) (U : X.Opens) :

↑(M.presheaf.obj (Opposite.op U)) ≃ₗ[↑(X.presheaf.obj (Opposite.op U))] ↑(N.presheaf.obj (Opposite.op U))

An isomorphism of 𝒪_X-modules induces a Γ(X, U)-linear equivalence between the modules of sections over U, given by the components of the isomorphism and of its inverse at U.

Equations

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

Instances For

source

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsLinearEquiv_apply {X : Scheme} {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : ↑(M.presheaf.obj (Opposite.op U))) :

(sectionsLinearEquiv e U) x = (CategoryTheory.ConcreteCategory.hom (Hom.app e.hom U)) x

The linear equivalence induced by e on sections over U is the component of e.hom.

source

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsLinearEquiv_symm_apply {X : Scheme} {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : ↑(N.presheaf.obj (Opposite.op U))) :

(sectionsLinearEquiv e U).symm x = (CategoryTheory.ConcreteCategory.hom (Hom.app e.inv U)) x

The inverse of the linear equivalence induced by e on sections over U is the component of e.inv.

source

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf (X : AlgebraicGeometry.Scheme) :

CategoryTheory.Functor X.Modules (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat)

The forgetful functor from 𝒪_X-modules to sheaves of abelian groups on X.

This is SheafOfModules.toSheaf for the sheaf of rings X.ringCatSheaf, packaged so that the source is the category X.Modules; compare AlgebraicGeometry.Scheme.Modules.toPresheaf.

Equations