The determinant of a vector bundle of fixed rank

If E is a finite locally free sheaf on a scheme X of constant rank r, its top exterior power det E = ⋀ʳ E has rank r.choose r = 1 at every point, so it is an invertible sheaf. This file packages the top exterior power as the determinant functor FiniteLocallyFreeSheaf.determinant X r : FixedRank X r ⥤ InvertibleSheaf X, and computes it in the basic cases: the determinant of the free sheaf of rank r is the trivial line bundle, the determinant of a sheaf of constant rank one is the sheaf itself, and every sheaf of rank zero has trivial determinant.

Main declarations

• FiniteLocallyFreeSheaf.determinant X r: the determinant E ↦ ⋀ʳ E of finite locally free sheaves of constant rank r, with values in invertible sheaves;
• FiniteLocallyFreeSheaf.determinantFreeIso: the determinant of the free sheaf of rank r is the trivial invertible sheaf;
• FiniteLocallyFreeSheaf.determinantOneIso: on sheaves of constant rank one, the determinant is naturally the sheaf itself, as a finite locally free sheaf;
• FiniteLocallyFreeSheaf.determinantZeroIso: in rank zero, the determinant is naturally the trivial invertible sheaf.

References

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

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinant (X : AlgebraicGeometry.Scheme) (r : ℕ) : CategoryTheory.Functor (FixedRank X r) (InvertibleSheaf X)

The determinant of finite locally free sheaves of constant rank r on X: the top exterior power E ↦ ⋀ʳ E of the underlying 𝒪_X-modules, which has rank r.choose r = 1 everywhere and so is an invertible sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinant_obj_obj {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) : ((determinant X r).obj E).obj = (SheafOfModules.exteriorPower X.sheaf r).obj E.obj.obj

The underlying sheaf of the determinant of a sheaf E of constant rank r is the r-th exterior power of the underlying 𝒪_X-module of E.

@[simp]

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

The determinant acts on a morphism of sheaves of constant rank r by the r-th exterior power of the underlying morphism of 𝒪_X-modules.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantFreeIso (X : AlgebraicGeometry.Scheme) (r : ℕ) : (determinant X r).obj (FixedRank.free X r) ≅ InvertibleSheaf.trivial X

The determinant of the free sheaf of rank r is the trivial invertible sheaf: the top exterior power of the free sheaf on Fin r is free on its single r-element subset.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantFreeIso_hom_hom {X : AlgebraicGeometry.Scheme} (r : ℕ) : (determinantFreeIso X r).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SheafOfModules.exteriorPowerFreeIso (ULift.{u, 0} (Fin r)) r).hom (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap fun (x : ↑(Set.powersetCard (ULift.{u, 0} (Fin r)) r)) => PUnit.unit) (CategoryTheory.eqToHom ⋯)))

On underlying sheaves, determinantFreeIso is the identification ⋀ʳ (free (Fin r)) ≅ free (Set.powersetCard (Fin r) r) of exteriorPowerFreeIso, followed by the map of free sheaves collapsing the single r-element subset of Fin r to a point.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantOneIso (X : AlgebraicGeometry.Scheme) : (determinant X 1).comp (InvertibleSheaf.toFiniteLocallyFree X) ≅ FixedRank.toFiniteLocallyFree X 1

The determinant of a finite locally free sheaf of constant rank one is naturally the sheaf itself: ⋀¹ E ≅ E.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantOneIso_hom_app_hom {X : AlgebraicGeometry.Scheme} (E : FixedRank X 1) : ((determinantOneIso X).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((SheafOfModules.exteriorPowerOneIso X.sheaf).hom.app E.obj.obj)

On underlying sheaves, the components of determinantOneIso are those of SheafOfModules.exteriorPowerOneIso.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantZeroIso (X : AlgebraicGeometry.Scheme) : determinant X 0 ≅ (CategoryTheory.Functor.const (FixedRank X 0)).obj (InvertibleSheaf.trivial X)

In rank zero the determinant is naturally the trivial invertible sheaf: ⋀⁰ E ≅ 𝒪_X.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantZeroIso_hom_app_hom {X : AlgebraicGeometry.Scheme} (E : FixedRank X 0) : ((determinantZeroIso X).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.exteriorPowerZeroIso X.sheaf).hom.app E.obj.obj) (CategoryTheory.CategoryStruct.comp (SheafOfModules.freePUnitIsoUnit X.ringCatSheaf).inv (CategoryTheory.eqToHom ⋯)))

On underlying sheaves, the components of determinantZeroIso are those of SheafOfModules.exteriorPowerZeroIso, followed by the identification of the structure sheaf with the free sheaf on one generator.