The sheaf of linear morphisms #
For a presheaf of modules and a sheaf of modules over a sheaf of rings, local linear morphisms from the first to the second form a sheaf of sets; only the target has to be a sheaf. This is the gluing input for the dual sheaf: take the target to be the structure sheaf. The construction works over any site and does not require commutativity of the rings.
Over an object U, a section is an additive morphism between the restrictions of the source
and the target to the slice over U, whose components are linear over the restricted structure
sheaf. Restriction pulls such morphisms back along arrows. Linearity is local because
equality of target sections can be checked on a covering sieve, so compatible local linear
morphisms glue uniquely.
The resulting sheaf PresheafOfModules.linearHom has local sections over U equivalent to
morphisms between the restricted presheaves of modules (PresheafOfModules.linearHomObjEquiv).
When the source is a sheaf as well, they are equivalent to morphisms between the restricted
module sheaves, and global sections are equivalent to morphisms of the original module sheaves.
The declarations SheafOfModules.linearHomObjEquiv, SheafOfModules.linearHomSectionsEquiv,
and SheafOfModules.linearHomObjEquiv_map_app expose these identifications and their behavior
under restriction. They support dot notation directly, for example M.val.linearHom N and
M.linearHomObjEquiv N U.
Sources #
The construction builds on Mathlib's presheafHom. Its gluing proof uses the sheaf result
Presheaf.IsSheaf.hom together with the subfunctor criterion Subfunctor.isSheaf_iff.
This file constructs the underlying sheaf of sets; it does not equip it with a module structure or identify it with a categorical internal Hom.
The sheaf of sets of local linear morphisms from a presheaf of modules to a sheaf of modules. Only the target has to be a sheaf.
Equations
Instances For
Sections over U of the sheaf of local linear morphisms from a presheaf of modules are
precisely the morphisms between the restrictions to the slice over U.
Equations
- M.linearHomObjEquiv N U = { toFun := PresheafOfModules.linearHomObjToFun✝ M N U, invFun := PresheafOfModules.linearHomObjInvFun✝ M N U, left_inv := ⋯, right_inv := ⋯ }
Instances For
Evaluate a local linear Hom section at a slice object and a source section.
Equations
- M.linearHomApp N U φ V m = (CategoryTheory.ConcreteCategory.hom ((↑φ).app (Opposite.op V))) m
Instances For
The morphism associated to a local linear Hom section evaluates to the section's component.
The local linear Hom section associated to a morphism evaluates to the morphism's component.
Restriction of a local linear morphism restricts its component linear maps.
Sections of the linear Hom sheaf over an object are precisely morphisms between the restricted sheaves of modules.
The lemmas linearHomObjEquiv_app and linearHomObjEquiv_symm_app give the componentwise
evaluation formulas in both directions.
Equations
- M.linearHomObjEquiv N U = (M.val.linearHomObjEquiv N U).trans (SheafOfModules.fullyFaithfulForget (R.over U)).homEquiv.symm
Instances For
The morphism associated to a local linear Hom section evaluates to the section's component.
The local linear Hom section associated to a morphism evaluates to the morphism's component.
Restriction of a Hom section restricts its component linear maps.
Global sections of the linear Hom sheaf are morphisms of sheaves of modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism associated to a global Hom section is read at the identity of each slice.
The global Hom section associated to a morphism restricts to that morphism on each slice.