Several complex variables and analytic spaces
The Lean Pool projects whose card's first MSC2020 code is in class 32, Several complex variables and analytic spaces: 3 articles, one per card.
TheoremA complex structure on the six-sphere#
Formalizes Levent Alpöge's construction of a complex-analytic atlas on the standard six-sphere. The development builds a compact complex threefold from torus fibrations with cusp and elliptic fibres, computes its homology and fundamental group, proves that its underlying topological space is homeomorphic to the six-sphere, and transports the complex atlas across that homeomorphism. It adapts Lean developments by Yury G. Kudryashov and Sebastian Kumar, together with the statement from the Formal Conjectures Authors.
Quoted from the card LeanPool/projects/hopf-problem.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.
Mathoverflow1973.SixSphereComplexAtlas.exists_complex_analytic_atlas(theorem), declared in LeanPool/HopfProblem/Threefold/SixSphereComplexAtlas.lean, line 68: “The standard unit six-sphere admits a complex three-dimensional charted-space structure making it a complex-analytic manifold.”Mathoverflow1973.SixSphereComplexAtlas.exists_complex_atlas(theorem), declared in LeanPool/HopfProblem/Threefold/SixSphereComplexAtlas.lean, line 83: “The standard unit six-sphere admits a complex three-dimensional charted-space structure making it a continuously differentiable complex manifold.”Mathoverflow1973.mathoverflow_1973(theorem; a main declaration), declared in LeanPool/HopfProblem/MainTheorem/Core3.lean, line 37: “The formalized statement of MathOverflow question 1973: the standard six-sphere carries a complex three-dimensional manifold atlas.”
Project
- Authors: Boris Alexeev, Yury G. Kudryashov, Sebastian Kumar, The Formal Conjectures Authors.
- Source: HopfProblem: formalization of Alpöge's six-sphere construction by Boris Alexeev.
- Project repository: plby/HopfProblem, at commit 9ac8a456.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 32Q55, 57R15.
- In Lean Pool: LeanPool/HopfProblem, from the card LeanPool/projects/hopf-problem.yaml.
Sources
TheoremClassical several complex variables#
Formalizes Cauchy and Taylor theory, Hartogs phenomena, removable singularities, analytic sets and germs, Weierstrass theory, holomorphic convexity, Cartan–Thullen and Bochner tube theorems, plurisubharmonic functions, Levi convexity, and elementary Runge-domain theory. Weierstrass preparation and coordinate-origin germ Noetherianity overlap LocalComplexGeometry; this development also supplies germ unique factorization and global extension and convexity results.
Quoted from the card LeanPool/projects/lean-scv.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.
SCV.cauchy_formula_polydisc(theorem), declared in LeanPool/SeveralComplexVariables/Solution.lean, line 99: “Holomorphic functions on a polydisc satisfy the iterated Cauchy integral formula.”SeveralComplexVariables.analyticOnNhd_of_separately_analytic_locally_bounded(theorem; a main declaration), declared in LeanPool/SeveralComplexVariables/SeveralComplexVariables/LocallyBounded.lean, line 146: “On an open subset of a finite complex coordinate space, a Banach-valued separately analytic map that is locally bounded is jointly analytic.” Its source, as the card gives it: “Boas (2013), Section 2.7, Theorem 7 (the classical two-variable scalar case).”SCV.identity_theorem(theorem), declared in LeanPool/SeveralComplexVariables/Solution.lean, line 130: “Holomorphic functions on a connected domain that agree on a nonempty open subset agree throughout the domain.”
Project
- Authors: Bastiaan J Braams.
- Project repository: bjbraams/lean-scv, at commit caef1ae7.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 32A10, 32D05, 32E10.
- In Lean Pool: LeanPool/SeveralComplexVariables, from the card LeanPool/projects/lean-scv.yaml.
Sources
TheoremFoundational local complex-analytic geometry#
Develops a common Lean foundation for several classical local theorems in several complex variables: complex-analytic Weierstrass preparation with full germ uniqueness, Noetherianity of holomorphic-germ rings, finite projection for hypersurface germs, the holomorphic constant-rank normal form, and the finite-family local analytic Nullstellensatz. The imported development also exposes the arbitrary-ideal Nullstellensatz and regular level-set, submersion, and immersion consequences.
Quoted from the card LeanPool/projects/local-complex-geometry.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.
LocalComplexGeometry.localAnalyticNullstellensatz(theorem; a main declaration), declared in LeanPool/LocalComplexGeometry/Palomar.lean, line 458: “If a finite family of functions analytic at the origin has common zero set locally contained in the zero set of another analytic function, then a positive power of the latter is locally an analytic linear combination of the family.”LocalComplexGeometry.holomorphicGerm_isNoetherian(theorem), declared in LeanPool/LocalComplexGeometry/Palomar.lean, line 37: “For every finite complex dimension, including dimension zero, the local ring of holomorphic germs at the origin is Noetherian.”LocalComplexGeometry.hypersurface_finiteProjection(theorem), declared in LeanPool/LocalComplexGeometry/Palomar.lean, line 315: “A nonzero hypersurface germ vanishing at the origin admits a linear coordinate change whose local quotient is finite free over the base germ ring, together with an explicit prepared equation and a proper, surjective finite-fiber projection of the local zero set.”LocalComplexGeometry.holomorphic_constantRank_normalForm(theorem), declared in LeanPool/LocalComplexGeometry/Palomar.lean, line 410: “An analytic map of locally constant complex rank is locally equivalent, through analytic source and target coordinates, to the standard rank projection.”ClassicalComplexWPT.classicalComplexWeierstrassPreparation(theorem), declared in LeanPool/LocalComplexGeometry/ClassicalComplexWPT/Main.lean, line 32: “A complex-analytic germ of exact order in one distinguished variable factors uniquely into a nonvanishing analytic unit and a monic Weierstrass polynomial whose analytic coefficient germs vanish at the origin.” Its source, as the card gives it: “BochaoKong/classical-complex-wpt, commit b4a7273fe5c9752753c52e10494097569089642d (2026-08-28).”LocalComplexGeometry.analyticNullstellensatz_ideal(theorem), declared in LeanPool/LocalComplexGeometry/Nullstellensatz/Main.lean, line 35: “For every ideal of the local holomorphic-germ ring, the ideal of germs vanishing on its local zero set equals its radical.”LocalComplexGeometry.holomorphic_regularLevelSet_parametrization(theorem), declared in LeanPool/LocalComplexGeometry/Analytic/LevelSet.lean, line 112: “Near a regular point, the level set of a holomorphic map admits an analytic parametrization with an analytic local inverse on the level set.”
Project
- Authors: BochaoKong.
- Source: Foundational theorems in local complex-analytic geometry by BochaoKong.
- Project repository: BochaoKong/nullstellensatz, at commit 02969724.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 32A05, 32A10, 32B05, 32C25, 13E05.
- In Lean Pool: LeanPool/LocalComplexGeometry, from the card LeanPool/projects/local-complex-geometry.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.