feat(Algebra/Homology): add Euler–Poincaré formula by jessealama · Pull Request #29713 · leanprover-community/mathlib4

jessealama · 2025-09-16T11:26:30Z

This PR builds on the generalized Euler characteristic framework from #31121 to prove the Euler-Poincaré formula for chain complexes.

PR #31121 defines the Euler characteristic for general homological complexes. This PR specializes those definitions to ℤ-indexed chain complexes and proves the main Euler-Poincaré theorem.

Main result (in `EulerPoincare.lean`)

ChainComplex.eulerChar_eq_homologyEulerChar: For ℤ-indexed bounded chain complexes of finite-dimensional modules over a division ring, the alternating sum of chain dimensions equals the alternating sum of homology dimensions.

Supporting lemmas

The file also provides dimension lemmas generalized to arbitrary HomologicalComplex (ModuleCat k) c (not just ℤ-indexed chain complexes):

HomologicalComplex.dFrom_zero_range / dTo_zero_range: zero range when the target/source object is zero
HomologicalComplex.dFrom_range_finrank_eq_d / dTo_range_finrank_eq_d: range of dFrom/dTo has the same dimension as the underlying differential
HomologicalComplex.range_dTo_le_ker_dFrom: range of dTo is contained in the kernel of dFrom

Builds on: #31121
Related to: #29639, #29643, #29646

github-actions · 2025-09-16T11:27:44Z

PR summary 9ea9209725

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Homology.EulerPoincare` (new file)	1666

Declarations diff

+ chain_dimension_decomposition
+ dFrom_range_finrank_eq_d
+ dFrom_succ_range_finrank_eq_dTo
+ dFrom_zero_range
+ dTo_range_finrank_eq_d
+ dTo_zero_range
+ eulerChar_eq_homologyEulerChar
+ finrank_eq_zero_of_isZero
+ homology_finrank_formula
+ isZero_outside_Ico
+ moduleCatToCycles_range_finrank_eq
+ range_dTo_le_ker_dFrom
+ sum_Ico_add_sum_Ico_shift_neg_cancel

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

kim-em · 2025-09-16T23:43:43Z

(btw --- don't mark things as "draft" unless you specifically do not want review yet.)

Mathlib/Algebra/Homology/EulerCharacteristic.lean

Mathlib/Algebra/Homology/EulerPoincare.lean

kim-em · 2025-09-16T23:52:35Z

(My suggestions are not necessary conditions for merging this. We can generalize later.)

jessealama · 2025-09-17T08:55:53Z

(My suggestions are not necessary conditions for merging this. We can generalize later.)

Thanks for taking a look! I think working with Grothendieck groups might be a bit of a stretch, at this point. I think this is a decent result as it stands, though I definitely agree that an integer generalization is even better and should be possible.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

mathlib4-merge-conflict-bot · 2025-11-19T08:10:15Z

This pull request has conflicts, please merge master and resolve them.

jessealama · 2025-11-20T13:58:05Z

This pull request has conflicts, please merge master and resolve them.

resolved!

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic Add Euler characteristic for homological complexes with arbitrary index types and shapes. The typeclass ComplexShape.EulerCharSigns provides alternating signs for Euler characteristic computations, with instances for up/down ℕ and up/down ℤ. New file EulerCharacteristic.lean defines eulerChar and homologyEulerChar for HomologicalComplex (ModuleCat R) c where c has an EulerCharSigns instance. Both finite and infinite sum versions are provided. Split from leanprover-community#29713 as suggested by @joelriou.

mathlib-merge-conflicts · 2026-02-06T15:27:55Z

This pull request has conflicts, please merge master and resolve them.

…complexes Prove `ChainComplex.eulerChar_eq_homologyEulerChar`: for ℤ-indexed bounded chain complexes of finite-dimensional modules over a division ring, the Euler characteristic (alternating sum of dimensions) equals the homological Euler characteristic (alternating sum of homology dimensions). The proof uses a telescoping sum argument: the dimension of each chain module decomposes via rank-nullity as kernel + image, and the kernel further decomposes as homology + boundaries. The boundary terms telescope and cancel at adjacent degrees, leaving only the homology terms. This builds on the `finsum`-based Euler characteristic infrastructure from `Mathlib.Algebra.Homology.EulerCharacteristic`.

…roof

…duplication - Replace hand-rolled Subsingleton proof with ModuleCat.subsingleton_of_isZero - Delete cycles_dimension_decomposition wrapper, inline as ← homology_finrank_formula - Golf chain_dimension_decomposition proof using omega - Simplify Finset interval helpers to one-liners (ext; simp; omega) - Extract isZero_outside_Ico helper to deduplicate IsZero logic in main theorem - Generalize dimension lemmas from ChainComplex to HomologicalComplex

Reduce EulerPoincare.lean from 368 to 302 lines: - Remove/shorten docstrings on trivial and private lemmas - Inline temporary `have` bindings in `sum_Ico_alternating_shift_decomp` - Replace 36-line `calc` in `homology_finrank_formula` with direct proof - Eliminate `let`/`change` pattern in main theorem via inline lambdas - Use `rcases`/`<;>` and `exact_mod_cast` for shorter tactic blocks - Merge consecutive `rw` calls

…se existing Ico splits Remove 4 custom utility lemmas from EulerPoincare.lean and replace with: - `Finset.sum_Ico_add_sum_Ico_shift_neg_cancel` (new, in Intervals.lean) - Existing `insert_Ico_add_one_left_eq_Ico` / `insert_Ico_right_eq_Ico_add_one` - `Int.negOnePow_succ` + `Int.coe_negOnePow` for sign alternation

…r-Poincaré Replace `simp [xNext]` and `simp [xPrev]` with `simp only` followed by explicit `rw` using `next_eq'`/`prev_eq'` to satisfy the `linter.style.flexible` check.

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch from 0679a12 to c9ece47 Compare September 16, 2025 11:44

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch 2 times, most recently from 4d1e774 to 36439f8 Compare September 16, 2025 13:31

github-actions bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch 3 times, most recently from b48d5c1 to d402fb9 Compare September 16, 2025 15:06

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch from d402fb9 to e42702d Compare September 16, 2025 15:10

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch from e42702d to 48a1b5b Compare September 16, 2025 15:25

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 16, 2025

jessealama changed the title ~~feat: add Euler characteristic for chain complexes~~ feat (Algebra/Homology): add Euler-Poincaré formula Sep 16, 2025

jessealama force-pushed the euler-poincare-formula branch 4 times, most recently from fb43799 to e04637c Compare September 16, 2025 16:50

kim-em reviewed Sep 16, 2025

View reviewed changes

Mathlib/Algebra/Homology/EulerCharacteristic.lean Outdated Show resolved Hide resolved

kim-em reviewed Sep 16, 2025

View reviewed changes

Mathlib/Algebra/Homology/EulerCharacteristic.lean Outdated Show resolved Hide resolved

kim-em reviewed Sep 16, 2025

View reviewed changes

Mathlib/Algebra/Homology/EulerCharacteristic.lean Outdated Show resolved Hide resolved

kim-em reviewed Sep 16, 2025

View reviewed changes

Mathlib/Algebra/Homology/EulerPoincare.lean Outdated Show resolved Hide resolved

jessealama force-pushed the euler-poincare-formula branch from e04637c to 4ae31ae Compare September 17, 2025 08:58

jessealama mentioned this pull request Oct 31, 2025

[Merged by Bors] - feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic #31121

Closed

jessealama force-pushed the euler-poincare-formula branch from 9e4e7b7 to 413feba Compare November 5, 2025 15:24

jessealama marked this pull request as draft November 5, 2025 15:50

jessealama force-pushed the euler-poincare-formula branch from 413feba to 8d4bcbb Compare November 5, 2025 15:54

jessealama force-pushed the euler-poincare-formula branch from 8d4bcbb to e9f8473 Compare November 7, 2025 13:14

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

jessealama force-pushed the euler-poincare-formula branch from e9f8473 to 9eb54eb Compare November 20, 2025 13:57

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 20, 2025

jessealama force-pushed the euler-poincare-formula branch from 9eb54eb to 53503de Compare November 22, 2025 08:59

jessealama mentioned this pull request Mar 2, 2026

feat(Algebra/Homology): add dimension lemmas for homological complex differentials #35977

Closed

jessealama added 7 commits March 18, 2026 23:00

refactor(Algebra/Homology): use Int.coe_negOnePow in Euler-Poincaré p…

f08a5a6

…roof

style: trim docstrings, flatten nested haves, rename section

1b98fb4

style(Algebra/Homology): replace flexible simp with simp only in Eule…

79d93d6

…r-Poincaré Replace `simp [xNext]` and `simp [xPrev]` with `simp only` followed by explicit `rw` using `next_eq'`/`prev_eq'` to satisfy the `linter.style.flexible` check.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Algebra/Homology): add Euler–Poincaré formula#29713

feat(Algebra/Homology): add Euler–Poincaré formula#29713
jessealama wants to merge 7 commits intoleanprover-community:masterfrom
jessealama:euler-poincare-formula

jessealama commented Sep 16, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Sep 16, 2025 •

edited

Loading

Declarations diff

Uh oh!

kim-em commented Sep 16, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Sep 16, 2025

Uh oh!

jessealama commented Sep 17, 2025 •

edited

Loading

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

jessealama commented Nov 20, 2025

Uh oh!

mathlib-merge-conflicts bot commented Feb 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

jessealama commented Sep 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Main result (in EulerPoincare.lean)

Supporting lemmas

Uh oh!

github-actions bot commented Sep 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 9ea9209725

Import changes for modified files

Declarations diff

Uh oh!

kim-em commented Sep 16, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Sep 16, 2025

Uh oh!

jessealama commented Sep 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

jessealama commented Nov 20, 2025

Uh oh!

mathlib-merge-conflicts bot commented Feb 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jessealama commented Sep 16, 2025 •

edited

Loading

Main result (in `EulerPoincare.lean`)

github-actions bot commented Sep 16, 2025 •

edited

Loading

jessealama commented Sep 17, 2025 •

edited

Loading