The determinant of a vector bundle of locally constant rank

The rank of a finite locally free sheaf E on a scheme X is only locally constant: on a disconnected scheme it may differ between components. Its determinant det E is the invertible sheaf which over each open set X_n = {x | rank E x = n} is the top exterior power ⋀ⁿ E.

It is the exterior power of E in the locally constant degree rank E (FiniteLocallyFreeSheaf.locallyConstantExteriorPower), which has rank (rank E).choose (rank E) = 1 everywhere, so it is an invertible sheaf FiniteLocallyFreeSheaf.det E. An isomorphism E ≅ F preserves the rank, so the determinant is a functor FiniteLocallyFreeSheaf.determinantCore X on the core of the category of finite locally free sheaves. On sheaves of constant rank r it agrees with the fixed-rank determinant FiniteLocallyFreeSheaf.determinant X r (FiniteLocallyFreeSheaf.detIsoDeterminant).

Main declarations

• FiniteLocallyFreeSheaf.det: the determinant ⋀^{rank E} E of a finite locally free sheaf, an invertible sheaf;
• FiniteLocallyFreeSheaf.determinantCore X: the determinant as a functor on the core of the category of finite locally free sheaves;
• FiniteLocallyFreeSheaf.detIsoDeterminant: in constant rank r, det E is the fixed-rank determinant ⋀ʳ E.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16
• F. Knudsen and D. Mumford, The projectivity of the moduli space of stable curves I: Preliminaries on det and Div, Math. Scand. 39 (1976), Chapter I

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.det {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : InvertibleSheaf X

The determinant det E = ⋀^{rank E} E of a finite locally free sheaf E: over each open set where E has rank n it is the top exterior power ⋀ⁿ E. It has rank (rank E).choose (rank E) = 1 everywhere, so it is an invertible sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.det_obj {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : E.det.obj = (AlgebraicGeometry.locallyConstantExteriorPower E.rank).obj E.obj

The underlying sheaf of det E is ⋀^{rank E} of the underlying 𝒪_X-module of E.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantCore (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (CategoryTheory.Core (FiniteLocallyFreeSheaf X)) (InvertibleSheaf X)

The determinant is functorial on the core of the category of finite locally free sheaves: an isomorphism E ≅ F preserves the rank and induces the isomorphism ⋀^{rank E} E ≅ ⋀^{rank E} F = ⋀^{rank F} F of determinants.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantCore_obj {X : AlgebraicGeometry.Scheme} (E : CategoryTheory.Core (FiniteLocallyFreeSheaf X)) : (determinantCore X).obj E = E.of.det

The determinant of an object of the core is det of the underlying finite locally free sheaf.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.determinantCore_map_hom {X : AlgebraicGeometry.Scheme} {E F : CategoryTheory.Core (FiniteLocallyFreeSheaf X)} (e : E ⟶ F) : ((determinantCore X).map e).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.locallyConstantExteriorPower E.of.rank).map e.iso.hom.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)))

The determinant acts on an isomorphism E ≅ F through ⋀^{rank E}, followed by the identification ⋀^{rank E} F = ⋀^{rank F} F given by rank E = rank F.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.detIsoDeterminant {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) : E.obj.det ≅ (determinant X r).obj E

On a sheaf E of constant rank r, the determinant det E is the fixed-rank determinant ⋀ʳ E.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.detIsoDeterminant_hom_hom {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) : (detIsoDeterminant E).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((locallyConstantExteriorPowerIso E.obj.rank ⋯).hom.app E.obj.obj) (CategoryTheory.eqToHom ⋯))

On underlying sheaves, detIsoDeterminant is locallyConstantExteriorPowerIso.