The sheafified tensor product and Picard classes of a scheme #
For a scheme, Scheme.Modules.tensorObj M N is the associated sheaf of the objectwise tensor
product of the underlying presheaves. The unit, symmetry, and the associator before iterated
sheafification are exported. Scheme.Modules.PicardClass X is the set of isomorphism classes of
invertible sheaves, with its distinguished structure-sheaf class. Intrinsic invertibility and
rank-one local trivializations are imported from their arbitrary-site owner.
Equations
- AlgebraicGeometry.Scheme.Modules.instCategory_derivedAlgGeo = { toCategoryStruct := AlgebraicGeometry.Scheme.Modules.instCategory.toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
Instances For
Equations
Instances For
Equations
Instances For
The sheafification of the objectwise tensor product of two sheaves of modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tensoring with a fixed sheaf on the left preserves composition.
tensorHom (𝟙 F) − is functorial. Every layer of tensorHom is a functor, so
this is Functor.map_comp on top of tensorHom_comp_tensorHom; no linearity
is involved anywhere.
That distinction is the point. A scalar cannot be moved across tensorHom:
neither X.Modules nor X.PresheafOfModules carries the monoidal-linear
structure that would need, and supplying it would mean a Γ-linear structure on
presheaves, linearity of toPresheafOfModules and of associatedSheaf, and a
MonoidalLinear instance — none of which exist. A morphism can be moved
across it, by this lemma. So an argument that would multiply by a section should
compose with multiplication-by-that-section instead.
It has to live here rather than with its consumer: the monoidal structure on
X.PresheafOfModules is a local instance in this namespace, so
MonoidalCategoryStruct X.PresheafOfModules does not synthesize outside it and
the presheaf-level identity below is not even statable elsewhere.
Tensoring with a fixed sheaf on the left preserves composition.
tensorHom (𝟙 F) − is functorial. Every layer of tensorHom is a functor, so
this is Functor.map_comp on top of tensorHom_comp_tensorHom; no linearity
is involved anywhere.
That distinction is the point. A scalar cannot be moved across tensorHom:
neither X.Modules nor X.PresheafOfModules carries the monoidal-linear
structure that would need, and supplying it would mean a Γ-linear structure on
presheaves, linearity of toPresheafOfModules and of associatedSheaf, and a
MonoidalLinear instance — none of which exist. A morphism can be moved
across it, by this lemma. So an argument that would multiply by a section should
compose with multiplication-by-that-section instead.
It has to live here rather than with its consumer: the monoidal structure on
X.PresheafOfModules is a local instance in this namespace, so
MonoidalCategoryStruct X.PresheafOfModules does not synthesize outside it and
the presheaf-level identity below is not even statable elsewhere.
Sheafification identifies tensoring with the structure sheaf on the left.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sheafification identifies tensoring with the structure sheaf on the right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conjugating an endomorphism of the unit by the right unitor.
M ≅ M ⊗ 𝟙 --(𝟙 ⊗ φ)--> M ⊗ 𝟙 ≅ M. This is how a map out of the structure sheaf acts on an
arbitrary module sheaf without any linearity of the tensor being available.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same conjugation, one level down: a morphism of presheaves of modules.
This is where the computation happens. Mathlib's PresheafOfModules/Monoidal.lean gives the
unitors and ⊗ₘ openwise by rfl, reducing to ModuleCat's own monoidal structure, so at this
level t ↦ t ⊗ₜ 1 ↦ t ⊗ₜ φ(1) ↦ φ(1) • t is definitional. No such API exists a level up, on the
sheafified tensor — unitorConj_eq is what carries the computation across.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conjugate is the sheaf morphism whose presheaf image is unitorConjPre.
The point of the whole file's approach to this: sheafification is never computed on sections.
unitorConjPre is a presheaf endomorphism of M's underlying presheaf; toPresheafOfModules is
fully faithful, so it is the image of a unique sheaf endomorphism, and naturality of the
sheafification adjunction's counit collapses counit.inv ≫ associatedSheaf.map _ ≫ counit.hom to
exactly that endomorphism.
Two steps are congrArg/exact rather than rw: goals here mention associatedSheaf, and are
not type-correct under the instances transparency level, which stops rw matching patterns that
are syntactically present.
What conjugation does to a section: it multiplies by φ's value on 1.
The element-level rule for the sheafified tensor that the twist API needed and did not have.
Before this, no lemma anywhere in the tree said what any of tensorObj, tensorHom or
tensorUnitRightIso does to a section — every consumer used them at the morphism level only.
Given unitorConj_eq it is rfl: the sheaf morphism is unitorConjPre, and that computes
openwise by Mathlib's presheaf-monoidal API.
The scalar is ascribed at Γ(X, U.unop). Written bare it elaborates at the unit sheaf's own
section type, where the action on Γ(M, U) does not synthesize.
A pure tensor of sections, as a section of the sheafified tensor.
The exportable handle on the sheafified tensor at section level. tensorObj is built from
toPresheafOfModules and the monoidal structure on X.PresheafOfModules, neither of which is
nameable outside this file — the first is used through a private abbrev, the second is a
local instance. So a consumer cannot write t ⊗ₜ y at all, and any section-level statement about
the tensor has to be phrased through a named constructor. This is it.
It is the image of the honest pure tensor under the sheafification adjunction's unit. Sections of a sheafification are not in general sums of pure tensors, so this is a map into the sections, not a description of them — which is all the twist API needs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A scalar moves across the pure tensor.
Tensor bilinearity plus linearity of the unit's component. What makes it usable downstream is the direction: a scalar sitting outside, where a chart extension leaves it, can be pushed onto the second factor, where the twist's own section lives.
The pure tensor restricts termwise.
The sheafification unit is a morphism of presheaves of modules, so it commutes with restriction,
and the presheaf tensor restricts a pure tensor termwise by definition
(PresheafOfModules.Monoidal.tensorObj_map_tmul). Without this a section built by tmulSection
cannot be followed to a smaller open, which every chart-by-chart argument has to do.
The pure tensor is additive in its first factor.
A scalar moves onto the first factor -- the companion of smul_tmulSection, which moves
it onto the second. A chart-local generation argument leaves the scalar on the F side, where
the generators live.
The pure tensor of a finite sum is the finite sum of pure tensors.
The sheafification unit of a presheaf of modules is locally surjective.
Its underlying map of abelian presheaves is toSheafify
(toPresheaf_map_sheafificationAdjunction_unit_app, by rfl), and that carries Mathlib's
instance. Stated because instance search does not find it on its own: all three of
HasWeakSheafify, HasSheafCompose and PreservesSheafification synthesize here, but the
composite goal does not, and explicit application is what closes it.
Locally, a section of the sheafified tensor product is a finite sum of pure tensors.
tmulSection's docstring warns that it is "a map into the sections, not a description of them",
and globally that is right: sheafification does not preserve surjectivity of
M(U) ⊗ N(U) → Γ(M ⊗ N, U) on the nose. Locally it does, and this is that statement — the
missing converse, and the reason it can only live in this file.
Nothing outside can state it. The monoidal structure on X.PresheafOfModules is a local instance
here and associatedSheaf is a private abbrev, so a consumer cannot write t ⊗ₜ y, cannot name
M' ⊗ N', and therefore cannot say "a section of the sheafification comes from the presheaf
tensor" at all. Anything needing to take a section of M ⊗ N apart has to be given this from
inside.
The proof is the three facts that were unavailable to a consumer: the sheafification unit is
locally surjective, so t has a preimage z in the presheaf tensor near x;
TensorProduct.exists_finset writes z as a finite sum of pure tensors; and the unit's component
is additive, which turns that sum into a sum of tmulSections by definition of tmulSection.
The neighbourhood is genuinely needed: V is where the preimage exists, and no smaller claim about
U itself is available.
The twistBy shape, applied to a section: it is the pure tensor with ψ's value on 1.
(ρ.inv ≫ tensorHom (𝟙 F) ψ) is exactly the shape of Proj.twistBy and of
Proj.chartTwistBy. This says what it does to a section, which nothing in the tree did before.
Proved the same way as unitorConj_eq, and sheafification is again never computed on sections.
The counit's inverse is the adjunction unit — hinv, from the right triangle identity, assembled
mono-free because Mono does not synthesize on a .val; then naturality of that unit carries a
presheaf-level computation across, and the presheaf-level part (t ↦ t ⊗ₜ 1 ↦ t ⊗ₜ ψ(1)) is rfl.
Every step is congrArg/exact: goals here mention associatedSheaf and are not type-correct
under the instances transparency level, so rw will not match patterns that are syntactically
present. The naturality step additionally needs DFunLike.congr_fun rather than congrFun — the
components are bundled LinearMaps, not functions.
Associativity before iterated sheafification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The object property of being an invertible sheaf.
Equations
- AlgebraicGeometry.Scheme.Modules.isInvertible X M = (have this := M; this).IsInvertible
Instances For
The category of invertible sheaves on a scheme.
Equations
Instances For
Isomorphism classes of invertible sheaves.
Equations
Instances For
The isomorphism class of an invertible sheaf.
Instances For
The distinguished class of the structure sheaf.