Module sheaves on a variety are k-linear #
On a variety over k, multiplication by a global function is an endomorphism of
every module sheaf, and it commutes with every morphism. Composing that with the
ring map k → Γ(X, O_X) supplied by the structure morphism makes every
Hom-group a k-module, compatibly with composition — that is, it makes
X.Modules a k-linear category, and Coh X with it.
Every ingredient was already here. Cohomology.globalSectionSmul,
globalSectionAction, baseFieldToGlobalSections, varietyScalarAction and
varietyScalarAction_naturality were built to give coherent cohomology its
k-structure; this file observes that the same action makes the category
linear, which is a strictly stronger statement and one nothing had recorded.
Why this is worth its own file #
Because of what it unlocks rather than what it says. Mathlib's
DerivedCategory.Linear gives Linear R (DerivedCategory C) from
Linear R C, and Linear.fullSubcategory propagates to
DerivedCategory.Bounded C, which is a FullSubcategory of it. So the single
instance below is the whole distance between "Hom in Dᵇ(Coh X) is an abelian
group" and "Hom in Dᵇ(Coh X) is a k-vector space".
That was the one obstruction to stating what a spherical object is:
Hom(E, E⟦i⟧) ≅ k is not expressible against an AddCommGrp, and
Numerical/GrothendieckGroup/MukaiVector.lean's docstring names exactly this
gap when it says sphericity of an object needs an Ext that layer does not
have.
What this does not give #
Finite-dimensionality. Linear k says the Hom-groups are k-modules, not
that they are finite-dimensional, and nothing here bounds them.
FiniteDimensionalCohomology remains supplied data, and the projective case is
issue #332. A Hom-group being a k-vector space of unknown dimension is
exactly enough to state sphericity and not enough to prove anything about it.
Nor does it give a trace, a Serre functor, or any duality. Those need the finiteness this file does not supply.
Main results #
Variety.modulesLinear—X.Modulesisk-linear.Variety.cohLinear—Coh Xisk-linear, inherited as a full subcategory.Variety.smul_eq_action_comp— the scalar action unfolds to precomposition with multiplication by the corresponding global function, which is the only fact a caller needs in order to compute with it.Variety.derivedLinear—Dᵇ(Coh X)isk-linear, soHom(E, F⟦i⟧)is ak-vector space.
Morphisms of module sheaves are a module over the global functions.
The scalar is a global section of the structure sheaf, not an element of a base
field: globalSectionAction M : Γ(X, ⊤) →+* End M is already a ring
homomorphism, and every clause below uses only that plus Preadditive. Nothing
here is specific to a variety, and no field appears.
Variety.homModule is this composed with k → Γ(X, ⊤); it predates this and is
left as it is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Module sheaves on any scheme form a Γ(X, ⊤)-linear category.
comp_smul is the clause with content, and it is globalSectionSmul_naturality:
multiplication by a global function is central on morphisms.
This is what lets a section-valued scalar be moved across a morphism. The
Linear k instance next door only ever moves elements of the base field, which
is not enough when the scalar is a function like fⁿ/gⁿ on a chart.
Equations
- X.modulesLinearGlobal = { homModule := fun (M N : X.Modules) => X.homModuleGlobal M N, smul_comp := ⋯, comp_smul := ⋯ }
Morphisms of module sheaves on a variety form a k-module, by precomposing
with multiplication by the corresponding global function.
Precomposition rather than postcomposition is an arbitrary choice;
varietyScalarAction_naturality says the two agree, and comp_smul below is
where that is spent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Module sheaves on a variety form a k-linear category.
smul_comp is associativity. comp_smul is the only clause with content: it
says the action may be moved across a morphism, which is
varietyScalarAction_naturality, itself globalSectionSmul_naturality — the
statement that multiplication by a global function is central.
Equations
- AlgebraicGeometry.Variety.modulesLinear Y = { homModule := fun (M N : Y.Modules) => AlgebraicGeometry.Variety.homModule Y M N, smul_comp := ⋯, comp_smul := ⋯ }
The scalar action, unfolded. This is the computation rule for everything
above; Linear k alone says a k-module structure exists but not which one.
Coherent sheaves on a variety form a k-linear category, inherited from
the ambient module sheaves as a full subcategory.
Declared rather than inferred because Coh is a def, so instance search does
not see the FullSubcategory underneath it; the Preadditive and Abelian
instances next door are stated the same way.
Equations
- AlgebraicGeometry.Variety.cohLinear Y = { homModule := AlgebraicGeometry.Variety.cohLinear._aux_1 Y, smul_comp := ⋯, comp_smul := ⋯ }
Propagation to the derived category #
Mathlib's DerivedCategory.instLinear fires on its own, and the inferInstance
below is the whole of it. That was not always true: Coh.abelian used to obtain
its toPreadditive from the full subcategory's Abelian instance rather than
from Coh.preadditive, and search could not cross the gap, so this term had to
supply cohLinear by hand. Issue #662 closed that by pinning the field in
CoherentSheaf/Abelian/Basic.lean; see the docstring there for why the two are
not interchangeable and what keeps them pinned.
The derived category of coherent sheaves on a variety is k-linear.