Exterior powers of finite locally free sheaves on a scheme

The n-th exterior power of 𝒪_X-modules (SheafOfModules.exteriorPower X.sheaf n) preserves finite local freeness (SheafOfModules.isFiniteLocallyFree_exteriorPower), so it restricts to an endofunctor FiniteLocallyFreeSheaf.exteriorPower X n of the category of finite locally free sheaves on X. A basis of E with r elements over an open U induces a basis of ⋀ⁿ E over U indexed by the n-element subsets of the basis, so the rank of ⋀ⁿ E at x is (E.rank x).choose n. In particular, if E has constant rank r, then ⋀ʳ E has rank one at every point.

Main declarations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPower X n: the n-th exterior power of finite locally free sheaves on X;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPowerFreeIso: the exterior power of a finite free sheaf as the free sheaf on subsets of its basis;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_exteriorPower_apply: the rank of ⋀ⁿ E at x is (E.rank x).choose n.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPower (X : AlgebraicGeometry.Scheme) (n : ℕ) : CategoryTheory.Functor (FiniteLocallyFreeSheaf X) (FiniteLocallyFreeSheaf X)

The n-th exterior power of finite locally free sheaves on a scheme X, computed as the exterior power of the underlying 𝒪_X-modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPower_obj_obj {X : AlgebraicGeometry.Scheme} (n : ℕ) (E : FiniteLocallyFreeSheaf X) : ((exteriorPower X n).obj E).obj = (SheafOfModules.exteriorPower X.sheaf n).obj E.obj

The underlying sheaf of the n-th exterior power of a finite locally free sheaf is the n-th exterior power of its underlying 𝒪_X-module.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPowerFreeIso (X : AlgebraicGeometry.Scheme) (I : Type u) [LinearOrder I] [Finite I] (n : ℕ) : (exteriorPower X n).obj (free X I) ≅ free X ↑(Set.powersetCard I n)

The exterior power of a free sheaf, expressed in the finite locally free category.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exteriorPower_map_hom {X : AlgebraicGeometry.Scheme} (n : ℕ) {E F : FiniteLocallyFreeSheaf X} (φ : E ⟶ F) : ((exteriorPower X n).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPower X.sheaf n).map φ.hom) (CategoryTheory.eqToHom ⋯))

The n-th exterior power acts on morphisms of finite locally free sheaves through the n-th exterior power of the underlying morphisms of 𝒪_X-modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_exteriorPower_apply {X : AlgebraicGeometry.Scheme} (n : ℕ) (E : FiniteLocallyFreeSheaf X) (x : ↥X) : ((exteriorPower X n).obj E).rank x = (E.rank x).choose n

The rank of the n-th exterior power of a finite locally free sheaf E at x is (E.rank x).choose n.