Algebraic geometry
The Lean Pool projects whose card's first MSC2020 code is in class 14, Algebraic geometry: 5 articles, one per card.
TheoremBrill–Noether theory and gonality of finite graphs#
Formalizes Brill–Noether existence through genus five, chains of marked banana graphs and loops, the treewidth lower bound for gonality, and a tricycle example whose gonality drops under regular subdivision. Includes divisor and transmission infrastructure and the Demazure-product support used by vertex gluing.
Quoted from the card LeanPool/projects/brill-noether-graphs.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Highlights.brill_noether_existence_through_five(theorem; a main declaration), declared in LeanPool/BrillNoetherGraphs/Highlights.lean, line 1242: “Every finite connected loopless multigraph of genus g at most five has, for integers r and d, a divisor of degree d and rank at least r whenever (r + 1) * (g - d + r) ≤ g.”Highlights.treewidth_le_gonality(theorem), declared in LeanPool/BrillNoetherGraphs/Highlights.lean, line 2052: “On a finite connected loopless multigraph, for every natural number k, any degree-k divisor of rank at least one bounds the treewidth by k; this is the witness formulation of the treewidth lower bound for divisorial gonality.”Highlights.gonality_drops_under_regular_subdivision(theorem), declared in LeanPool/BrillNoetherGraphs/Highlights.lean, line 2003: “There is a graph whose divisorial gonality strictly decreases under a regular subdivision.”
Project
- Authors: Nathan Pflueger.
- Project repository: npflueger/brill-noether-graphs, at commit ce62dd82.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 14T15, 05C50.
- In Lean Pool: LeanPool/BrillNoetherGraphs, from the card LeanPool/projects/brill-noether-graphs.yaml.
Sources
TheoremFinEqs - reducing equations defining a subset of n-space over a finite field#
Formalizes the finite-field equation-reduction theorem and sharpness examples.
Quoted from the card LeanPool/projects/fineqs.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.Fineqs.theorem_1(theorem; a main declaration), declared in LeanPool/Fineqs/Main.lean, line 259: “Reduces equations on a small finite set to at most n equations in the same span.”LeanPool.Fineqs.prop_1(theorem; a main declaration), declared in LeanPool/Fineqs/Main.lean, line 454: “Shows the cardinality bound in the reduction theorem is sharp.”LeanPool.Fineqs.corollary_2(theorem), declared in LeanPool/Fineqs/Main.lean, line 356: “Applies the reduction theorem to affine space over a finite field.”LeanPool.Fineqs.corollary_3(theorem), declared in LeanPool/Fineqs/Main.lean, line 383: “Applies the reduction theorem to nonempty projective zero loci.”LeanPool.Fineqs.remark_example(theorem), declared in LeanPool/Fineqs/Main.lean, line 507: “Shows n - 1 coordinate-function combinations have at least q common zeros.”
Project
- Authors: Stefan Barańczuk, Aristotle.
- Source: doi:10.5802/afst.1766, arXiv:1906.11174.
- Project repository: nasqret/fineqs.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 14G15, 11T06.
- In Lean Pool: LeanPool/Fineqs, from the card LeanPool/projects/fineqs.yaml.
Sources
TheoremGrothendieck's Vanishing Theorem#
Formalizes Grothendieck's vanishing theorem for sheaf cohomology on Noetherian topological spaces.
Quoted from the card LeanPool/projects/grothendieck-vanishing.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
GrothendieckVanishing(theorem; a main declaration), declared in LeanPool/GrothendieckVanishing/GrothendieckVanishing.lean, line 135: “Proves vanishing of sheaf cohomology above the topological Krull dimension.”
Project
- Authors: Vasily Ilin, Brian Nugent.
- Source: doi:10.1007/978-1-4757-3849-0, https://github.com/Vilin97/Clawristotle/tree/grothendieck-vanishing.
- Project repository: Vilin97/Clawristotle.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 14F06, 18F20.
- In Lean Pool: LeanPool/GrothendieckVanishing, from the card LeanPool/projects/grothendieck-vanishing.yaml.
Sources
TheoremThe Jacobian of a Compact Riemann Surface#
Constructs the Jacobian of a compact Riemann surface as the period-lattice quotient of the dual of holomorphic 1-forms, and proves the surrounding theory it needs: the genus as the dimension of the space of holomorphic 1-forms, discreteness and full rank 2g of the period lattice, the Abel-Jacobi map and its injectivity in positive genus, functoriality (pushforward, pullback, degree, and the projection formula), Riemann-Roch, Serre duality via Laurent tails, the residue theorem, the Dolbeault-Cech comparison, and finite dimensionality of the first cohomology by a Schwartz/Montel argument. The headline no-hack guard is that the genus vanishes exactly when the surface is homeomorphic to the sphere.
Quoted from the card LeanPool/projects/jacobian-diffgeo.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
genus_eq_zero_iff_homeo(theorem; a main declaration), declared in LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean, line 128: “A compact connected Riemann surface has genus zero if and only if it is homeomorphic to the 2-sphere.”Jacobian.ofCurve_inj(theorem; a main declaration), declared in LeanPool/JacobianDiffgeo/CechCount/Final.lean, line 120: “The Abel-Jacobi map of a compact Riemann surface of positive genus is injective: two points with the same image coincide.”Jacobian.pushforward_pullback(lemma), declared in LeanPool/JacobianDiffgeo/Challenge.lean, line 147: “For a non-constant holomorphic map between compact Riemann surfaces, the pushforward composed with the pullback on Jacobians is multiplication by the degree of the map.”
Project
- Authors: Rado Kirov.
- Source: Jacobians of compact Riemann surfaces (AI challenge) by Kevin Buzzard, https://gist.github.com/kbuzzard/778bc714030b3e974ab5f4038783d1a9.
- Project repository: rkirov/jacobian-fable.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 14H40, 30F30, 32G20.
- In Lean Pool: LeanPool/JacobianDiffgeo, from the card LeanPool/projects/jacobian-diffgeo.yaml.
Sources
TheoremRiemann–Roch for algebraic function fields#
Formalizes the Riemann–Roch theorem for algebraic function fields of one variable through the adelic route. Divisors are indexed by intrinsic places (discrete rank-one valuation subrings containing the constants), with an equivalence to a two-chart coordinate model via Ostrowski's theorem. The development builds Riemann–Roch spaces, the genus, an intrinsic adele space, Weil differentials and the canonical class, and proves Riemann's inequality, the duality theorem, Riemann–Roch, Clifford's inequality, and the standard corollaries. As an application it shows that a Weierstrass elliptic curve has genus one and identifies its degree-one places with the class group of the coordinate ring compatibly with the group law.
Quoted from the card LeanPool/projects/riemann-roch-function-fields.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
FunctionField.riemann_roch(theorem; a main declaration), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/RiemannRoch.lean, line 286: “For a function field K over its full constant field k, a canonical divisor W, and any divisor D indexed by intrinsic places, ℓ(D) = deg D + 1 − g + ℓ(W − D).”FunctionField.duality(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/RiemannRoch.lean, line 272: “For a canonical divisor W and any divisor D, ℓ(W − D) equals the index of specialty i(D), the codimension of L(D) plus K inside the adele space.”FunctionField.riemann_ineq(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/RiemannRoch.lean, line 279: “Riemann's inequality ℓ(D) ≥ deg D + 1 − g holds for every divisor D.”FunctionField.clifford(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/RiemannRoch.lean, line 341: “Clifford's inequality 2(ℓ(D) − 1) ≤ deg D holds for every divisor D with 0 ≤ deg D ≤ 2g − 2, ℓ(D) > 0, and ℓ(W − D) > 0 for a canonical divisor W. The degree bounds are not needed for the inequality and are dropped in FunctionField.clifford_of_ell_pos.”FunctionField.exists_isCanonical(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/RiemannRoch.lean, line 265: “Every function field admits a canonical divisor, namely the divisor of a nonzero Weil differential.”WeierstrassCurve.Affine.genus_eq_one(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/EllipticCurve.lean, line 91: “The function field of a Weierstrass elliptic curve over a field k that is its full constant field (for example any algebraically closed k, in any characteristic) has genus one.”WeierstrassCurve.Affine.picTorsor_compat_groupLaw(theorem), declared in LeanPool/RiemannRochFunctionFields/CoordinateFree/EllipticCurve.lean, line 100: “The bijection between degree-one places of an elliptic function field and the class group of the coordinate ring is compatible with the elliptic group law.”
Project
- Authors: Guanghao Li.
- Source: Riemann–Roch for function fields, in Lean 4 by Guanghao Li.
- Project repository: vaca22/riemann-roch-function-fields, at commit dbca5bee.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 14H05, 11R58, 14H52.
- In Lean Pool: LeanPool/RiemannRochFunctionFields, from the card LeanPool/projects/riemann-roch-function-fields.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.