feat: Euler's polyhedron formula via homological algebra#29639
Closed
jessealama wants to merge 6 commits intoleanprover-community:masterfrom
Closed
feat: Euler's polyhedron formula via homological algebra#29639jessealama wants to merge 6 commits intoleanprover-community:masterfrom
jessealama wants to merge 6 commits intoleanprover-community:masterfrom
Conversation
PR summary 82ba83d8bcImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Homology.HomologicalComplex | 747 | 1238 | +491 (+65.73%) |
Import changes for all files
| Files | Import difference |
|---|---|
15 filesMathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree |
3 |
7 filesMathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution |
17 |
Mathlib.Algebra.Category.ContinuousCohomology.Basic |
28 |
Mathlib.Algebra.Homology.LocalCohomology |
36 |
Mathlib.Algebra.Homology.ConcreteCategory Mathlib.CategoryTheory.Abelian.Ext |
51 |
16 filesMathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.DerivedCategory.TStructure Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.Triangulated |
90 |
Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.MappingCone |
100 |
7 filesMathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.TotalComplexShift |
109 |
Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.Monoidal |
121 |
Mathlib.AlgebraicTopology.SingularHomology.Basic |
144 |
4 filesMathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex |
147 |
Mathlib.Algebra.Homology.AlternatingConst |
251 |
16 filesMathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject |
266 |
Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.ExtraDegeneracy |
269 |
Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Notations |
275 |
4 filesMathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.AlgebraicTopology.MooreComplex |
338 |
21 filesMathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution |
339 |
Mathlib.Algebra.Homology.HomologySequence |
345 |
5 filesMathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.SingleHomology |
346 |
Mathlib.Algebra.Homology.Linear |
412 |
Mathlib.Algebra.Homology.GrothendieckAbelian |
421 |
Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.HomologicalComplexAbelian |
435 |
Mathlib.CategoryTheory.Idempotents.HomologicalComplex |
455 |
3 filesMathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.HomologicalComplexBiprod |
462 |
Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.CategoryTheory.Generator.HomologicalComplex |
490 |
8 filesMathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.Single |
491 |
Mathlib.Algebra.Homology.EulerPoincare (new file) |
1525 |
Mathlib.Algebra.Homology.EulerPolyhedronFormula.Basic (new file) |
1590 |
Mathlib.Algebra.Homology.EulerPolyhedronFormula (new file) |
1591 |
Declarations diff
+ GeometricPolyhedron
+ HasChainComplexProperty
+ Polyhedron
+ acyclic_augmented_euler_char
+ acyclic_euler_char
+ acyclic_euler_poincare
+ alternating_telescoping_sum
+ augmentationMap
+ augmented_boundary_from_top_image
+ augmented_chain_shift
+ augmented_dFrom_zero_ker_finrank
+ augmented_dTo_at_dim_plus_one_image_finrank
+ augmented_d_shift
+ augmented_dim_zero
+ augmented_euler_characteristic_relation
+ boundariesSubmodule
+ boundary
+ boundary_from_top_dim_image
+ boundary_from_top_dim_ker_zero
+ boundary_from_top_dim_nonzero
+ chainComplexSc
+ chain_complex_rank_nullity
+ chain_module_rank_eq_face_count
+ cyclesSubmodule
+ edge_vertex_count_subtype
+ eulerChar
+ eulerChar'
+ eulerCharacteristic
+ euler_char_of_acyclic_augmentation
+ euler_formula_1d
+ euler_poincare_formula
+ euler_poincare_telescoping
+ euler_polyhedron_formula
+ exist_faces_at_all_dimensions
+ faceCount
+ handshaking_lemma
+ homology_eulerChar
+ homology_finrank_formula
+ instance (C : ChainComplex (ModuleCat (ZMod 2)) ℕ) (i : ℕ) : AddCommGroup (C.X i)
+ instance (C : ChainComplex (ModuleCat (ZMod 2)) ℕ) (i : ℕ) : Module (ZMod 2) (C.X i)
+ instance (P : Polyhedron α) (k : ℕ) : AddCommGroup (kChains P k)
+ instance (P : Polyhedron α) (k : ℕ) : AddCommMonoid (kChains P k) := by
+ instance (P : Polyhedron α) (k : ℕ) : FiniteDimensional (ZMod 2) (kChains P k) := by
+ instance (P : Polyhedron α) (k : ℕ) : Module (ZMod 2) (kChains P k)
+ instance (P : Polyhedron α) (k : ℕ) : Module.Finite (ZMod 2) (kChains P k) := by
+ instance : HasZeroMorphisms (ModuleCat (ZMod 2)) := inferInstance
+ isAcyclic
+ kChains
+ kChains_finrank
+ kChains_smul_sum
+ polyhedron_euler_as_special_case
+ polyhedron_homology_euler_char
+ sc_morphisms
+ sum_range_succ_eq_head
+ toAugmentedComplex
+ toChainComplex
+ unique_faces_at_top_dim
++ euler_formula_2d
++ instance (GP : GeometricPolyhedron α) (i : ℕ) :
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Member
|
This is great, thanks! Can you try to split the PR in smaller pieces? |
Contributor
Author
Sure! I can imagine splitting this up into four or five, PRs, depending on where they ought to go in Mathlib:
How does that sound? |
Member
Sounds perfect! |
joelriou
reviewed
Sep 14, 2025
joelriou
reviewed
Sep 14, 2025
joelriou
reviewed
Sep 14, 2025
Comment on lines
+9
to
+13
| # Freek № 13: Euler's Polyhedron Formula | ||
|
|
||
| This file proves Theorem 13 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/), | ||
| Euler's polyhedron formula, which states that for a convex polyhedron with V vertices, | ||
| E edges, and F faces, we have V - E + F = 2. |
Contributor
There was a problem hiding this comment.
I would argue that this is not a formalization of the statement or the proof of Theorem 13. The content of this PR does not connect the convexity of a certain subset of a real vector space and the vanishing of the homology.
We would surely welcome a PR which would show that the alternate sum of dimensions of a bounded complex of vector spaces equals the alternate sum of the dimensions of the homology spaces.
Contributor
Author
There was a problem hiding this comment.
I was intending to define a notion of combinatorial polyhedron with suitable axioms that permit us to make a chain complex out of (some of) these combinatorial polyhedra (I called those "geometric polyhedra" -- they are assumed to satisfy the property "boundary of boundary is zero"). I thereby avoid real numbers, not as a trick or to exclude such polyhedra as invalid, but because I thought a chain complex-based approach would be the right way to go.
Contributor
Author
|
Converting to draft while I split off various smaller PRs. |
Contributor
Author
|
See further discussion on Zulip. |
723480b to
b0736e0
Compare
This PR formalizes Euler's polyhedron formula (V - E + F = 2) using homological algebra, specifically through chain complexes and their Euler characteristics. Main contributions: - Define geometric polyhedra with chain complex structure - Prove that acyclic augmented chain complexes have Euler characteristic 1 - Apply to 2D case to obtain classical V - E + F = 2 formula - Add to Wiedijk's Formalizing 100 Theorems list (leanprover-community#13) The proof follows a modern algebraic topology approach, constructing a chain complex from the polyhedron's face structure and using the vanishing of homology groups to establish the formula. Co-authored-by: Jesse Michael Han <jesse@pqr.ai>
b0736e0 to
2f7d059
Compare
Following reviewer feedback, this refactors the proof to better leverage Mathlib's ShortComplex infrastructure: - Add import for ShortComplex.Exact to access exactness API - Add helper lemmas connecting chain complexes to short complexes - Remove redundant lemmas that were reimplementing existing API: - acyclic_implies_exact_at (was just hC k) - exact_implies_image_eq_kernel (was just hexact.moduleCat_range_eq_ker) - Directly use C_acyclic k instead of intermediate lemmas - Clarify relationship between (C.sc k).f/g and C.dTo k/C.dFrom k This makes the code more idiomatic and better aligned with Mathlib patterns while maintaining correctness of all proofs. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
- Add new file Mathlib/Algebra/Homology/EulerPoincare.lean - Define eulerChar' as alternating sum of chain group dimensions - Define homology_eulerChar as alternating sum of homology dimensions - State main theorem euler_poincare_formula (with sorry for proof) - Prove acyclic_euler_char showing homology characteristic is 0 for acyclic complexes - Show how polyhedron formula is a special case of general theorem This addresses reviewer feedback requesting the general Euler-Poincaré formula showing that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded complexes of vector spaces. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
Break up lines longer than 100 characters to comply with style guide 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
- Add polyhedron_homology_euler_char showing that for a spherical polyhedron with H_0 = Z, H_1 = 0, H_2 = Z, the homological Euler char is 2 - Add euler_char_of_acyclic_augmentation theorem framework - Fix type issues by using IsZero instead of equality to 0 - This clarifies the connection between the general Euler-Poincaré formula and the classical V - E + F = 2 for polyhedra The key insight: a spherical polyhedron has homology (1, 0, 1) giving homological Euler char = 1 - 0 + 1 = 2, which by Euler-Poincaré equals the alternating sum of face counts V - E + F. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
jessealama
added a commit
to jessealama/mathlib4
that referenced
this pull request
Sep 16, 2025
This PR adds the Euler-Poincaré formula for bounded chain complexes of finite-dimensional vector spaces over a field, following feedback from @joelriou in leanprover-community#29639. The main result states that for a bounded complex C that vanishes after position n: ∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i) This builds upon the Euler characteristic definitions from leanprover-community#29646. Key additions: - Basic lemmas about chain complex differentials at boundaries (dFrom 0, dTo n) - Relationship between dTo/dFrom and the underlying differentials - General telescoping lemma for alternating sums - The rank-nullity decomposition for chain complexes - The main Euler-Poincaré theorem Thanks to @joelriou for the valuable feedback that guided this implementation. Co-authored-by: joelriou <joelriou@users.noreply.github.com>
jessealama
added a commit
to jessealama/mathlib4
that referenced
this pull request
Sep 16, 2025
This PR contributes the Euler-Poincaré formula for bounded chain complexes of finite-dimensional vector spaces over a field. ## Main Contributions ### Core Theorem * `ChainComplex.euler_poincare_formula`: The Euler-Poincaré formula showing that the alternating sum of chain space dimensions equals the alternating sum of homology dimensions for bounded complexes ### Supporting Infrastructure * Euler characteristic definitions in `EulerCharacteristic.lean`: - `ChainComplex.boundedEulerChar`: Bounded Euler characteristic - `ChainComplex.homologyBoundedEulerChar`: Homological Euler characteristic * General chain complex lemmas added to `HomologicalComplex.lean` * Private telescoping sum lemma for the main proof ## Related Work This is part of a multi-PR contribution towards formalizing Euler's polyhedron formula (Wiedijk leanprover-community#13). Related to: - PR leanprover-community#29643 (telescoping sum infrastructure) - PR leanprover-community#29639 (original combined PR) ## Acknowledgments Thanks to @joelriou for valuable feedback on the original PR. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>
Contributor
Author
|
I'm going to close this PR for now. I'll keep working in the same branch, without a PR, building on top of the work done in #29713 . |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR adds the Euler-Poincaré formula for chain complexes, proving that the alternating sum of dimensions equals the alternating sum of homology dimensions for bounded complexes of finite-dimensional vector spaces.
Main Contributions
New files:
Mathlib/Algebra/Homology/EulerCharacteristic.lean- Euler characteristic definitionsMathlib/Algebra/Homology/EulerPoincare.lean- The Euler-Poincaré formulaKey definitions:
ChainComplex.boundedEulerChar: Euler characteristic over a finite setChainComplex.homologyBoundedEulerChar: Homology Euler characteristic over a finite setChainComplex.eulerChar: Euler characteristic as an infinite sumChainComplex.homologyEulerChar: Homology Euler characteristic as an infinite sumMain theorem:
ChainComplex.eulerChar_eq_homology_eulerChar: For bounded complexes of finite-dimensional vector spaces, the Euler characteristic equals the homology Euler characteristicThe proof uses a telescoping sum approach where chain spaces decompose into kernels and images.