The symmetric-power pullback comparison for module presheaves #
Pushforward, including restriction of scalars, has a canonical comparison from the symmetric
power of a pushforward to the pushforward of the symmetric power. On sections it sends a product
m₁ ⋯ mₙ over the source coefficient ring to the same product over the target coefficient ring.
Taking its mate under the pullback--pushforward adjunction constructs a natural map
α* (Symⁿ M) ⟶ Symⁿ (α* M) for pullback of module presheaves. Only the adjunction is needed
for this construction. This supplies the sectionwise input to symmetric-power pullback
comparisons for sheaves. Restriction of scalars does not generally give an isomorphism of
symmetric powers; the comparison is invertible when the coefficient presheaf map is an
isomorphism.
The construction follows the exterior-power comparison
TauCeti.PresheafOfModules.pullbackExteriorPowerComparison: it uses the module-level
restriction-of-scalars comparison TauCeti.ModuleCat.restrictScalarsSymmetricPowerComparison and
Mathlib's CategoryTheory.mateEquiv for the pullback--pushforward adjunction. The section formula
specifies the pushforward comparison, and the unit equation specifies the pullback comparison.
References #
- R. Hartshorne, Algebraic Geometry, Exercise II.5.16.
Pushforward of module presheaves carries the canonical symmetric-power comparison. It changes the coefficient ring of a product of sections, without changing its factors.
Instances For
On sections over U, the pushforward comparison is computed in the symmetric algebra by the
ring homomorphism induced by the identity of M(F U), viewed as a semilinear map over
α.app U; it sends a product of sections over S(U) to the same product over R(F U).
In degree one, the pushforward comparison is the identity of α_* M, read through the
identifications of first symmetric powers with the presheaves themselves.
In degree one, the pushforward comparison is the identity of α_* M, read through the
identifications of first symmetric powers with the presheaves themselves.
Pushforward along an isomorphism of coefficient presheaves preserves symmetric powers sectionwise.
The canonical map from the pullback of a symmetric power to the symmetric power of a pullback, characterized by compatibility with the pullback unit.
Instances For
The adjunction equation characterizes the canonical pullback comparison.
The adjunction equation characterizes the canonical pullback comparison.
On sections in the image of the pullback unit, the pullback comparison is computed in the
symmetric algebra by the ring homomorphism induced by the unit, viewed as a semilinear map over
α.app U; it sends a product of sections to the product of their images under the unit.