Exterior powers of 𝒪_X-modules in a locally constant degree #
For a locally constant function r : X → ℕ on a scheme X, the exterior power ⋀^r M of an
𝒪_X-module M is the 𝒪_X-module which over each open set r⁻¹{n} is the n-th exterior
power ⋀ⁿ M. The sets r⁻¹{n} form a cover of X by pairwise disjoint open sets, and ⋀^r M is
the product over n of the pushforwards of the restrictions of ⋀ⁿ M to r⁻¹{n}: its sections
over an open V are the families of sections of the ⋀ⁿ M over the sets V ∩ r⁻¹{n}. Over an
open set on which r is constantly n, the other factors have no nonzero sections, so ⋀^r M
restricts there to ⋀ⁿ M (restrictLocallyConstantExteriorPowerIso), and if r is constantly
n then ⋀^r M ≅ ⋀ⁿ M (locallyConstantExteriorPowerIso). Both isomorphisms are the projection
onto the n-th factor, read through the unit of the restriction--pushforward adjunction.
Main declarations #
TauCeti.AlgebraicGeometry.locallyConstantExteriorPower r: the exterior power⋀^rof𝒪_X-modules in a locally constant degreer;TauCeti.AlgebraicGeometry.locallyConstantExteriorPowerπ r n: the projection of⋀^ronto itsn-th factor;TauCeti.AlgebraicGeometry.restrictLocallyConstantExteriorPowerIsoandTauCeti.AlgebraicGeometry.locallyConstantExteriorPowerIso: over an open set whereris constantlyn, and ifris constantlyn,⋀^ris then-th exterior power.
References #
- [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16
The n-th factor of locallyConstantExteriorPower r: the n-th exterior power, restricted
to the fiber r⁻¹{n} and pushed forward to X.
Instances For
The exterior power ⋀^r M of an 𝒪_X-module M in a locally constant degree
r : X → ℕ: the 𝒪_X-module whose restriction to each open set r⁻¹{n} is the n-th exterior
power of M there (restrictLocallyConstantExteriorPowerIso). It is the product over n of
the pushforwards of these restrictions, whose sections over an open V are the families of
sections of ⋀ⁿ M over the sets V ∩ r⁻¹{n}.
Instances For
⋀^r M is the product over n of the factors locallyConstantExteriorPowerFactor r n.
⋀^r φ is the product over n of the maps (locallyConstantExteriorPowerFactor r n).map φ,
compared through the projections onto the n-th factor.
⋀^r φ is the product over n of the maps (locallyConstantExteriorPowerFactor r n).map φ,
compared through the projections onto the n-th factor.
The projection of ⋀^r M onto its n-th factor, the pushforward of the restriction of
⋀ⁿ M to r⁻¹{n}.
Instances For
The projection locallyConstantExteriorPowerπ r n is the product projection.
Over an open V on which r is constantly n, the projection of ⋀^r M onto its n-th
factor is an isomorphism on sections.
Restriction of ⋀^r M to an open where r is constant. Over an open U on which the
locally constant function r takes the value n, the restriction of ⋀^r M is the restriction
of the n-th exterior power ⋀ⁿ M, naturally in M.
Instances For
restrictLocallyConstantExteriorPowerIso is the restricted projection onto the n-th
factor, read through the restricted unit ⋀ⁿ M ⟶ (r⁻¹{n}).ι_* (⋀ⁿ M|_{r⁻¹{n}}).
restrictLocallyConstantExteriorPowerIso is the restricted projection onto the n-th
factor, read through the restricted unit ⋀ⁿ M ⟶ (r⁻¹{n}).ι_* (⋀ⁿ M|_{r⁻¹{n}}).
⋀^r M in constant degree. If the locally constant function r is constantly n,
then ⋀^r M is the n-th exterior power ⋀ⁿ M, naturally in M.
Instances For
locallyConstantExteriorPowerIso is the projection onto the n-th factor, read through the
unit ⋀ⁿ M ⟶ (r⁻¹{n}).ι_* (⋀ⁿ M|_{r⁻¹{n}}).
locallyConstantExteriorPowerIso is the projection onto the n-th factor, read through the
unit ⋀ⁿ M ⟶ (r⁻¹{n}).ι_* (⋀ⁿ M|_{r⁻¹{n}}).