Skip to content

Commit ed56d0f

Browse files
Paul-LezPaul-Lez
committed
Add formalisation of Hartshorne's conjecture for vector bundles
1 parent 76b7804 commit ed56d0f

File tree

4 files changed

+182
-0
lines changed

4 files changed

+182
-0
lines changed

‎FormalConjectures/ForMathlib/AlgebraicGeometry/ProjectiveSpace.lean

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import Mathlib.AlgebraicGeometry.Limits
2+
import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
3+
import Mathlib.RingTheory.MvPolynomial.Homogeneous
4+
5+
universe u v u' v' w
6+
7+
8+
open CategoryTheory Limits MvPolynomial AlgebraicGeometry
9+
10+
variable (n : Type v) (S : Scheme.{max u v})
11+
12+
local notation3 "ℤ[" n "]" => homogeneousSubmodule n ℤ
13+
local notation3 "ℤ[" n "].{" u "," v "}" => homogeneousSubmodule n (ULift.{max u v} ℤ)
14+
15+
attribute [local instance] MvPolynomial.gradedAlgebra
16+
17+
/--
18+
The projective space over a scheme `S`, with homogeneous coordinates indexed by `n`
19+
-/
20+
noncomputable def ProjectiveSpace : Scheme.{max u v} :=
21+
pullback (terminal.from S) (terminal.from (Proj ℤ[n].{u, v}))
22+
23+
/-- `ℙ(n; S)` is the affine `S` indexed by `n` -/
24+
scoped [AlgebraicGeometry] notation "ℙ("n"; "S")" => ProjectiveSpace n S

‎FormalConjectures/ForMathlib/AlgebraicGeometry/VectorBundle.lean

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
import Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
2+
import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
3+
import Mathlib.CategoryTheory.Sites.CoversTop
4+
5+
universe u v u' v'
6+
7+
namespace SheafOfModules
8+
9+
open CategoryTheory Limits
10+
11+
variable {C : Type u} [CategoryTheory.Category.{v, u} C]
12+
variable {J : CategoryTheory.GrothendieckTopology C}
13+
variable {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R)
14+
variable [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)]
15+
variable [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp]
16+
variable [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp]
17+
18+
/-- A vector bundle is a sheaf of modules that is locally isomorphic to
19+
a free sheaf. -/
20+
structure VectorBundleData (M : SheafOfModules R) where
21+
I : Type u
22+
X : I → C
23+
--TODO(lezeau) : we probably need to be more careful with
24+
--universes here.
25+
I' : I → Type _
26+
coversTop : J.CoversTop X
27+
locallyFree : ∀ i, (M.over <| X i) ≅ SheafOfModules.free (I' i)
28+
29+
structure FiniteRankVectorBundleData (M : SheafOfModules R) extends VectorBundleData M where
30+
finite : ∀ i, Finite (I' i)
31+
32+
/-- A class for vector bundles of constant finite rank. -/
33+
class IsVectorBundleWithRank (M : SheafOfModules R) (n : ℕ) where
34+
exists_vector_bundle_data : ∃ (D : M.FiniteRankVectorBundleData),
35+
∀ i, Nat.card (D.I' i) = n
36+
37+
end SheafOfModules

‎FormalConjectures/Paper/HartshorneConjecture.lean

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/-
2+
Copyright 2025 Google LLC
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
import FormalConjectures.Util.ProblemImports
17+
18+
/-! # Hartshorne's conjecture on Vector Bundles
19+
20+
*Reference*: [Varieties of small codimension in projective space](https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-80/issue-6/Varieties-of-small-codimension-in-projective-space/bams/1183535999.full)
21+
by *R. Hartshorne*
22+
-/
23+
24+
universe u v u' v' w
25+
26+
open CategoryTheory Limits MvPolynomial AlgebraicGeometry
27+
28+
variable (n : Type v) (S : Scheme.{max u v})
29+
30+
31+
namespace AlgebraicGeometry.Scheme
32+
33+
section AlgebraicVectorBundles
34+
35+
variable (S : Scheme.{u})
36+
37+
@[category API, AMS 18]
38+
theorem WEqualsLocallyBijective_addCommGrp {T : Type u}
39+
[TopologicalSpace T] :
40+
(Opens.grothendieckTopology T).WEqualsLocallyBijective (AddCommGrp : Type (u + 1)) := by
41+
sorry
42+
43+
@[category API, AMS 18]
44+
theorem WEqualsLocallyBijectiveOver {C : Type v} [Category C]
45+
(J : GrothendieckTopology C) (A : Type u') [Category A]
46+
{FA : A → A → Type*} {CA : A → Type*} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
47+
[ConcreteCategory A FA] (X : C) [J.WEqualsLocallyBijective A] :
48+
(J.over X).WEqualsLocallyBijective A := by
49+
sorry
50+
51+
instance instWEqualsLocallyBijectiveOpensAddCommGrp {T : Type*} [TopologicalSpace T] :
52+
(Opens.grothendieckTopology T).WEqualsLocallyBijective AddCommGrp :=
53+
sorry
54+
55+
instance instWEqualsLocallyBijectiveOver {C : Type v} [Category C]
56+
(J : GrothendieckTopology C) (A : Type u') [Category A]
57+
{FA : A → A → Type*} {CA : A → Type*} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
58+
[ConcreteCategory A FA] (X : C) [J.WEqualsLocallyBijective A] :
59+
(J.over X).WEqualsLocallyBijective A :=
60+
WEqualsLocallyBijectiveOver J A X
61+
62+
/--
63+
A vector bundle over a scheme `S` is a locally free `𝓞_S`-module of finite rank.
64+
-/
65+
structure VectorBundles where
66+
carrier : AlgebraicGeometry.Scheme.Modules S
67+
rank : ℕ
68+
isLocallyFreeFiniteConstantRank : SheafOfModules.IsVectorBundleWithRank
69+
(J := Opens.grothendieckTopology S) carrier rank
70+
71+
instance (S : Scheme) : Coe S.VectorBundles S.Modules where
72+
coe := fun 𝓕 => 𝓕.carrier
73+
74+
/--
75+
Vector bundles form a category.
76+
-/
77+
instance (S : Scheme) : Category (VectorBundles S) :=
78+
InducedCategory.category VectorBundles.carrier
79+
80+
def VectorBundles.toModule (S : Scheme) : S.VectorBundles ⥤ S.Modules where
81+
obj 𝓕 := 𝓕.carrier
82+
map f := f
83+
84+
@[category API, AMS 14]
85+
theorem hasFiniteCoproductsVectorBundles (S : Scheme) :
86+
HasFiniteCoproducts S.VectorBundles :=
87+
sorry
88+
89+
instance (S : Scheme) : HasFiniteCoproducts S.VectorBundles :=
90+
hasFiniteCoproductsVectorBundles S
91+
92+
/--
93+
A splitting of a vector bundle `𝓕` is a non-trivial direct sum decomposition of `𝓕`
94+
-/
95+
structure VectorBundles.Splitting
96+
{S : Scheme} (𝓕 : VectorBundles S) (ι : Type) [Fintype ι] [Nonempty ι] where
97+
(toFun : ι → S.VectorBundles)
98+
(iso : 𝓕 ≅ ∐ fun (i : ι) => toFun i)
99+
(non_trivial : ∀ i, IsEmpty (toFun i ≅ 𝓕))
100+
101+
instance {S : Scheme} (𝓕 : S.VectorBundles) (ι : Type) [Fintype ι] [Nonempty ι] :
102+
CoeOut (𝓕.Splitting ι) (ι → S.VectorBundles) where
103+
coe := fun s => s.toFun
104+
105+
--TODO(lezeau): here we would really need some sanity checks and
106+
--easier results.
107+
108+
end AlgebraicVectorBundles
109+
110+
/--
111+
There are no indecomposable vector bundles of rank 2 on `ℙⁿ` for `n ≥ 7`.
112+
This is conjecture 6.3 in _VARIETIES OF SMALL CODIMENSION IN PROJECTIVE SPACE_, R. Hartshorne
113+
-/
114+
@[category research open, AMS 14]
115+
theorem harthshorne_conjecture (n : ℕ) (hn : 7 ≤ n)
116+
(𝓕 : VectorBundles ℙ(Fin (n + 1); Spec (.of ℂ)))
117+
(h𝓕 : VectorBundles.rank 𝓕 = 2) :
118+
Nonempty (VectorBundles.Splitting 𝓕 (Fin 2)) :=
119+
sorry

‎FormalConjectures/Util/ForMathlib.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ limitations under the License.
1515
-/
1616

1717
import FormalConjectures.ForMathlib.Algebra.Order.Group.Pointwise.Interval
18+
import FormalConjectures.ForMathlib.AlgebraicGeometry.ProjectiveSpace
19+
import FormalConjectures.ForMathlib.AlgebraicGeometry.VectorBundle
1820
import FormalConjectures.ForMathlib.Analysis.SpecialFunctions.Log.Basic
1921
import FormalConjectures.ForMathlib.Combinatorics.Basic
2022
import FormalConjectures.ForMathlib.Data.Nat.MaxPrimeFac

0 commit comments

Comments
 (0)