[Merged by Bors] - feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic by jessealama · Pull Request #31121 · leanprover-community/mathlib4

jessealama · 2025-10-31T11:16:38Z

Add ComplexShape.EulerCharSigns typeclass providing the alternating signs χ : ι → ℤˣ for Euler characteristic computations. Instances are provided for up ℕ, down ℕ, up ℤ, and down ℤ.

The Euler characteristic definition (eulerChar) uses finsum to sum over all indices, with the ComplexShape as an explicit parameter. This allows working with arbitrary index types without requiring a Fintype instance, defaulting to 0 when the support is infinite.

The GradedObject version is the primary definition, with HomologicalComplex.eulerChar and HomologicalComplex.homologyEulerChar as abbreviations that apply the graded object version to C.X and C.homology respectively.

Split from #29713 as suggested by @joelriou.

github-actions · 2025-10-31T11:17:44Z

PR summary 088175664f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Homology.EulerCharacteristic` (new file)	1320

Declarations diff

+ EulerCharSigns
+ eulerCharSignsDownInt
+ eulerCharSignsDownNat
+ eulerCharSignsUpInt
+ eulerCharSignsUpNat
+ finrankSupport
+ finrankSupport_subset_iff
+ homologyEulerChar
+ homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset
+ mulSupport_eq_univ
+ support_eulerChar_summand
+ support_mul_of_ne_zero_left
+ support_mul_of_ne_zero_right
+ χ
+ χ_next
+ χ_prev
++ eulerChar
++ eulerChar_eq_sum_finSet_of_finrankSupport_subset

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 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).

Mathlib/Algebra/Homology/EulerCharacteristic.lean

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

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

jessealama · 2025-11-20T14:02:26Z

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

resolved!

jessealama · 2025-12-08T13:56:33Z

ping @joelriou I took a look at your comment and changed things as suggested. It's ready for another look!

jessealama · 2025-12-23T19:49:15Z

-awaiting-author

Mathlib/Algebra/Homology/EulerCharacteristic.lean

jessealama · 2026-02-04T08:23:04Z

-awaiting-author

…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 N and up/down Z. Introduces GradedObject.eulerChar and GradedObject.eulerCharTsum with ComplexShape as an explicit parameter, with HomologicalComplex versions as abbreviations.

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

…o lemmas Add `mulSupport_eq_univ`/`support_eq_univ` for functions that are everywhere non-one/nonzero, and `support_mul_of_ne_zero_left/right` for products where one factor is everywhere nonzero. Simplify `support_eulerChar_summand` using the new lemmas.

@robin-carlier

Make finsum-based eulerChar the primary definition, remove separate finite-sum versions. Make support_eulerChar_summand private. Thanks @robin-carlier for the review feedback.

Add a "Junk values" section to document that `eulerChar` and related definitions may produce junk values from `finsum` (0 for infinite support) and `Module.finrank` (0 for modules not free of finite rank).

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

robin-carlier

Thanks!

maintainer merge

github-actions · 2026-02-06T09:05:05Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

joelriou · 2026-02-06T11:56:20Z

Thanks!

bors merge

jessealama · 2026-02-06T12:49:25Z

Thanks!

Thanks for the help!

@joelriou

…istic (#31121) Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`. The Euler characteristic definition (`eulerChar`) uses `finsum` to sum over all indices, with the `ComplexShape` as an explicit parameter. This allows working with arbitrary index types without requiring a `Fintype` instance, defaulting to 0 when the support is infinite. The `GradedObject` version is the primary definition, with `HomologicalComplex.eulerChar` and `HomologicalComplex.homologyEulerChar` as abbreviations that apply the graded object version to `C.X` and `C.homology` respectively. Split from #29713 as suggested by @joelriou.

mathlib-bors · 2026-02-06T13:35:51Z

Pull request successfully merged into master.

Build succeeded:

@joelriou

…istic (leanprover-community#31121) Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`. The Euler characteristic definition (`eulerChar`) uses `finsum` to sum over all indices, with the `ComplexShape` as an explicit parameter. This allows working with arbitrary index types without requiring a `Fintype` instance, defaulting to 0 when the support is infinite. The `GradedObject` version is the primary definition, with `HomologicalComplex.eulerChar` and `HomologicalComplex.homologyEulerChar` as abbreviations that apply the graded object version to `C.X` and `C.homology` respectively. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic (leanprover-community#31121) Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`. The Euler characteristic definition (`eulerChar`) uses `finsum` to sum over all indices, with the `ComplexShape` as an explicit parameter. This allows working with arbitrary index types without requiring a `Fintype` instance, defaulting to 0 when the support is infinite. The `GradedObject` version is the primary definition, with `HomologicalComplex.eulerChar` and `HomologicalComplex.homologyEulerChar` as abbreviations that apply the graded object version to `C.X` and `C.homology` respectively. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic (leanprover-community#31121) Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`. The Euler characteristic definition (`eulerChar`) uses `finsum` to sum over all indices, with the `ComplexShape` as an explicit parameter. This allows working with arbitrary index types without requiring a `Fintype` instance, defaulting to 0 when the support is infinite. The `GradedObject` version is the primary definition, with `HomologicalComplex.eulerChar` and `HomologicalComplex.homologyEulerChar` as abbreviations that apply the graded object version to `C.X` and `C.homology` respectively. Split from leanprover-community#29713 as suggested by @joelriou.

@joelriou

…istic (leanprover-community#31121) Add `ComplexShape.EulerCharSigns` typeclass providing the alternating signs `χ : ι → ℤˣ` for Euler characteristic computations. Instances are provided for `up ℕ`, `down ℕ`, `up ℤ`, and `down ℤ`. The Euler characteristic definition (`eulerChar`) uses `finsum` to sum over all indices, with the `ComplexShape` as an explicit parameter. This allows working with arbitrary index types without requiring a `Fintype` instance, defaulting to 0 when the support is infinite. The `GradedObject` version is the primary definition, with `HomologicalComplex.eulerChar` and `HomologicalComplex.homologyEulerChar` as abbreviations that apply the graded object version to `C.X` and `C.homology` respectively. Split from leanprover-community#29713 as suggested by @joelriou.

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 31, 2025

jessealama changed the title ~~feat: generalize Euler characteristic using ComplexShape.EulerCharSigns~~ feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic Oct 31, 2025

jessealama mentioned this pull request Oct 31, 2025

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

Draft

jessealama force-pushed the feat/euler-char-generalized branch 3 times, most recently from 0e6cabb to 9f13faa Compare November 5, 2025 15:10

leanprover-community-bot-assistant assigned ocfnash Nov 8, 2025

jessealama force-pushed the feat/euler-char-generalized branch from 9f13faa to 3db3084 Compare November 10, 2025 08:09

joelriou added the t-category-theory Category theory label Nov 10, 2025

jessealama force-pushed the feat/euler-char-generalized branch from 012aa24 to 8d67eca Compare November 12, 2025 10:28

ocfnash removed their assignment Nov 12, 2025

joelriou reviewed Nov 12, 2025

View reviewed changes

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

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 12, 2025

jessealama force-pushed the feat/euler-char-generalized branch 2 times, most recently from a7f8bb5 to 31ed875 Compare November 12, 2025 21:36

jessealama requested a review from joelriou November 12, 2025 21:47

jessealama force-pushed the feat/euler-char-generalized branch from a27c882 to 9d20009 Compare November 14, 2025 09:12

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 feat/euler-char-generalized branch from 9d20009 to 7930a93 Compare November 20, 2025 14:01

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 feat/euler-char-generalized branch 2 times, most recently from e34b02c to 08d8d31 Compare November 22, 2025 09:26

jessealama force-pushed the feat/euler-char-generalized branch 3 times, most recently from 7fabf67 to 6e07cf2 Compare December 5, 2025 12:24

robin-carlier reviewed Jan 30, 2026

View reviewed changes

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

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

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2026

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 4, 2026

jessealama force-pushed the feat/euler-char-generalized branch from 6a290f6 to 6f58056 Compare February 4, 2026 08:23

jessealama and others added 8 commits February 5, 2026 22:14

Update Mathlib/Algebra/Homology/EulerCharacteristic.lean

dea778a

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

feat(Homology): use finsum for eulerCharTsum, remove Fintype requirement

813e184

refactor(Homology): simplify Euler characteristic API

932969f

Make finsum-based eulerChar the primary definition, remove separate finite-sum versions. Make support_eulerChar_summand private. Thanks @robin-carlier for the review feedback.

docs(Homology): clarify junk value behavior in EulerCharacteristic

76a01fb

Add a "Junk values" section to document that `eulerChar` and related definitions may produce junk values from `finsum` (0 for infinite support) and `Module.finrank` (0 for modules not free of finite rank).

Update Mathlib/Algebra/Homology/EulerCharacteristic.lean

594fe98

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

Update Mathlib/Algebra/Homology/EulerCharacteristic.lean

f77962c

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

jessealama force-pushed the feat/euler-char-generalized branch from 6f58056 to f77962c Compare February 5, 2026 21:14

jessealama requested a review from robin-carlier February 5, 2026 21:14

robin-carlier reviewed Feb 6, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 6, 2026

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 6, 2026

mathlib-bors bot changed the title ~~feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic~~ [Merged by Bors] - feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic Feb 6, 2026

mathlib-bors bot closed this Feb 6, 2026

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 088175664f

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

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

Uh oh!

jessealama commented Nov 20, 2025

Uh oh!

jessealama commented Dec 8, 2025

Uh oh!

jessealama commented Dec 23, 2025

Uh oh!

Uh oh!

Uh oh!

jessealama commented Feb 4, 2026

Uh oh!

robin-carlier left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 6, 2026

Uh oh!

joelriou commented Feb 6, 2026

Uh oh!

jessealama commented Feb 6, 2026

Uh oh!

mathlib-bors bot commented Feb 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

jessealama commented Oct 31, 2025 •

edited

Loading

github-actions bot commented Oct 31, 2025 •

edited

Loading