Hartshorne's conjecture on Vector Bundles

Reference: Varieties of small codimension in projective space by R. Hartshorne

theorem HartshorneConjecture.AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveOverOpensCarrierCarrierCommRingCatOverGrothendieckTopologyTypeHomObjForget_formalConjectures (S : AlgebraicGeometry.Scheme) (X : TopologicalSpace.Opens ↥S) : ((Opens.grothendieckTopology ↥S).over X).WEqualsLocallyBijective (Type u)

theorem HartshorneConjecture.AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveOverOpensCarrierCarrierCommRingCatOverGrothendieckTopologyAddCommGrpAddMonoidHomCarrier_formalConjectures (S : AlgebraicGeometry.Scheme) (X : TopologicalSpace.Opens ↥S) : ((Opens.grothendieckTopology ↥S).over X).WEqualsLocallyBijective AddCommGrp

structure HartshorneConjecture.AlgebraicGeometry.Scheme.VectorBundles (S : AlgebraicGeometry.Scheme) : Type (u + 1)

A vector bundle over a scheme S is a locally free $\mathcal{O}_S$-module of finite rank.

• carrier : S.Modules
• rank : ℕ
• isLocallyFreeFiniteConstantRank : SheafOfModules.IsVectorBundleWithRank self.carrier self.rank

instance HartshorneConjecture.AlgebraicGeometry.Scheme.instCoeVectorBundlesModules (S : AlgebraicGeometry.Scheme) : Coe (VectorBundles S) S.Modules

Equations

• HartshorneConjecture.AlgebraicGeometry.Scheme.instCoeVectorBundlesModules S = { coe := fun (𝓕 : HartshorneConjecture.AlgebraicGeometry.Scheme.VectorBundles S) => 𝓕.carrier }

instance HartshorneConjecture.AlgebraicGeometry.Scheme.instCategoryVectorBundles (S : AlgebraicGeometry.Scheme) : CategoryTheory.Category.{u, u + 1} (VectorBundles S)

Vector bundles form a category.

Equations

• HartshorneConjecture.AlgebraicGeometry.Scheme.instCategoryVectorBundles S = CategoryTheory.InducedCategory.category HartshorneConjecture.AlgebraicGeometry.Scheme.VectorBundles.carrier

def HartshorneConjecture.AlgebraicGeometry.Scheme.VectorBundles.toModule (S : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (VectorBundles S) S.Modules

Equations

• One or more equations did not get rendered due to their size.

theorem HartshorneConjecture.AlgebraicGeometry.Scheme.hasFiniteCoproductsVectorBundles (S : AlgebraicGeometry.Scheme) : CategoryTheory.Limits.HasFiniteCoproducts (VectorBundles S)

instance HartshorneConjecture.AlgebraicGeometry.Scheme.instHasFiniteCoproductsVectorBundles (S : AlgebraicGeometry.Scheme) : CategoryTheory.Limits.HasFiniteCoproducts (VectorBundles S)

structure HartshorneConjecture.AlgebraicGeometry.Scheme.VectorBundles.Splitting {S : AlgebraicGeometry.Scheme} (𝓕 : VectorBundles S) (ι : Type) [Fintype ι] [Nonempty ι] : Type (u + 1)

A splitting of a vector bundle 𝓕 is a non-trivial direct sum decomposition of 𝓕

• components : ι → VectorBundles S
• iso : 𝓕 ≅ ∐ self.components
• non_trivial (i : ι) : IsEmpty (self.components i ≅ 𝓕)

instance HartshorneConjecture.AlgebraicGeometry.Scheme.instCoeOutSplittingForallVectorBundles {S : AlgebraicGeometry.Scheme} (𝓕 : VectorBundles S) (ι : Type) [Fintype ι] [Nonempty ι] : CoeOut (𝓕.Splitting ι) (ι → VectorBundles S)

Equations

• HartshorneConjecture.AlgebraicGeometry.Scheme.instCoeOutSplittingForallVectorBundles 𝓕 ι = { coe := fun (s : 𝓕.Splitting ι) => s.components }

theorem HartshorneConjecture.harthshorne_conjecture (n : ℕ) (hn : 7 ≤ n) (𝓕 : AlgebraicGeometry.Scheme.VectorBundles (ProjectiveSpace (Fin (n + 1)) (AlgebraicGeometry.Spec (CommRingCat.of ℂ)))) (h𝓕 : 𝓕.rank = 2) : Nonempty (𝓕.Splitting (Fin 2))

There are no indecomposable vector bundles of rank 2 on $\mathbb{P}^n$ for $n \ge 7$. This is conjecture 6.3 in VARIETIES OF SMALL CODIMENSION IN PROJECTIVE SPACE, R. Hartshorne