Exterior powers of finite locally free sheaves in a locally constant degree

For a locally constant function r : X → ℕ, the exterior power ⋀^r of 𝒪_X-modules (TauCeti.AlgebraicGeometry.locallyConstantExteriorPower r) restricts over each open set r⁻¹{n} to the n-th exterior power. Since ⋀ⁿ preserves finite local freeness, so does ⋀^r, and it restricts to an endofunctor of the category of finite locally free sheaves on X. The rank of ⋀^r E at x is (rank E x).choose (r x).

Main declarations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.locallyConstantExteriorPower X r: the exterior power ⋀^r of finite locally free sheaves;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_locallyConstantExteriorPower_apply: the rank of ⋀^r E at x is (rank E x).choose (r x).

References

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

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isFiniteLocallyFree_locallyConstantExteriorPower {X : AlgebraicGeometry.Scheme} (r : LocallyConstant ↥X ℕ) (E : FiniteLocallyFreeSheaf X) : AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X ((AlgebraicGeometry.locallyConstantExteriorPower r).obj E.obj)

The exterior power ⋀^r E of a finite locally free sheaf in a locally constant degree r is finite locally free: over each open set r⁻¹{n} it is the finite locally free sheaf ⋀ⁿ E.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.locallyConstantExteriorPower (X : AlgebraicGeometry.Scheme) (r : LocallyConstant ↥X ℕ) : CategoryTheory.Functor (FiniteLocallyFreeSheaf X) (FiniteLocallyFreeSheaf X)

The exterior power E ↦ ⋀^r E of finite locally free sheaves in a locally constant degree r : X → ℕ: over each open set r⁻¹{n} it is the n-th exterior power.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.locallyConstantExteriorPower_obj_obj {X : AlgebraicGeometry.Scheme} (r : LocallyConstant ↥X ℕ) (E : FiniteLocallyFreeSheaf X) : ((locallyConstantExteriorPower X r).obj E).obj = (AlgebraicGeometry.locallyConstantExteriorPower r).obj E.obj

The underlying sheaf of ⋀^r E is ⋀^r of the underlying 𝒪_X-module of E.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.locallyConstantExteriorPower_map_hom {X : AlgebraicGeometry.Scheme} (r : LocallyConstant ↥X ℕ) {E F : FiniteLocallyFreeSheaf X} (φ : E ⟶ F) : ((locallyConstantExteriorPower X r).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.locallyConstantExteriorPower r).map φ.hom) (CategoryTheory.eqToHom ⋯))

The exterior power ⋀^r acts on morphisms of finite locally free sheaves through the underlying morphisms of 𝒪_X-modules.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_locallyConstantExteriorPower_apply {X : AlgebraicGeometry.Scheme} (r : LocallyConstant ↥X ℕ) (E : FiniteLocallyFreeSheaf X) (x : ↥X) : ((locallyConstantExteriorPower X r).obj E).rank x = (E.rank x).choose (r x)

The rank of ⋀^r E at x is (E.rank x).choose (r x).