Skip to content

feat(AlgebraicTopology): Eilenberg Steenrod axioms#38369

Open
quantumsnow wants to merge 64 commits into
leanprover-community:masterfrom
quantumsnow:eilenberg-steenrod-axioms
Open

feat(AlgebraicTopology): Eilenberg Steenrod axioms#38369
quantumsnow wants to merge 64 commits into
leanprover-community:masterfrom
quantumsnow:eilenberg-steenrod-axioms

Conversation

@quantumsnow
Copy link
Copy Markdown
Contributor

@quantumsnow quantumsnow commented Apr 22, 2026 •
edited
Loading

Jacob Scharmberg and others added 30 commits March 13, 2026 16:04
add: TopPair
362e036
fix simp quirk in inclAdjProj₁
26849b5
streamline TopPair preamble
4532d92
optimizations and style improvements
8037bfa
add TopPair.lean to Mathlib.lean
efda772
implement style improvement suggestions
29fa930
add isomorphism of TopPair with MorphismProperty.Comma
2bf6bb6
replace iso between TopPair and MorphismProperty.Comma by equivalence…
9c67f5a 
… of categories
add more simps and ext annotations
febb357
add more API for Homotopy and Homotopic
49b6a98
implement style suggestions in equivComma
c539636
fix indentation in equivComma
5dbafb3
style improvements
4bdc137
simplify proofs using attributes
c283edb
remove superfluous compMap
5d70970
@quantumsnow @dagurtomas
minor docstring fix
0514eeb 
Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
change definition of TopPair to use MorphismProperty.Arrow
72126df
@quantumsnow
Merge branch 'leanprover-community:master' into eilenberg-steenrod
0065ebb
first version of Eilenberg-Steenrod axioms
e28a1d0
use TopCat and MonoidalCategory API for TopPair.Homotopy
bf2fd7c
require embeddings in TopPair instead of inducing maps
436617a
@quantumsnow
Merge branch 'leanprover-community:master' into eilenberg-steenrod-ax…
669015c 
…ioms
@quantumsnow
Merge branch 'master' into eilenberg-steenrod
acbb2e1
remove redundant simp lemma
a5d7fb7
@quantumsnow
change naming and docstrings from inducing to embedding
839475b
Merge branch 'eilenberg-steenrod' into eilenberg-steenrod-axioms
dda09b7
add Eilenberg-Steenrod axioms
f198e6a
remove erroneous file
251287c
@quantumsnow
Merge branch 'leanprover-community:master' into eilenberg-steenrod
9532431
@quantumsnow
Merge branch 'leanprover-community:master' into eilenberg-steenrod-ax…
1b27a91 
…ioms
@quantumsnow
Copy link
Copy Markdown
Contributor Author

quantumsnow commented May 9, 2026

For some reason, I can't add any more inline comments at the moment. Maybe it is a github issue, I'll try again later or when you have incorporated the first set of changes (Some of the further comments, we have already discussed in person).

I have incorporated all current feedback so if you have more, let me know.

@quantumsnow
Copy link
Copy Markdown
Contributor Author

quantumsnow commented May 9, 2026

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 9, 2026
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
joelriou
joelriou reviewed May 10, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 10, 2026
quantumsnow and others added 7 commits May 11, 2026 08:03
@quantumsnow @joelriou
style improvements
18bfc29 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@quantumsnow @joelriou
add reassoc to Hom.iso_comm
028a3ef 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@quantumsnow @joelriou
remove unnecessary change of transparency mode
3910381 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
add default value for Hom.hom
f8880a7
remove redundant simp attribute
d7bf832
fix HasPairSequence for ComplexShapes with 'extremities'
6198121
fing too long lines
5f2fa6b
@quantumsnow
Copy link
Copy Markdown
Contributor Author

quantumsnow commented May 11, 2026

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2026
joelriou
joelriou reviewed May 11, 2026
View reviewed changes
Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 11, 2026
@quantumsnow quantumsnow mentioned this pull request May 12, 2026
Open
@quantumsnow
Copy link
Copy Markdown
Contributor Author

quantumsnow commented May 12, 2026

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 12, 2026
@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

@chrisflav chrisflav chrisflav left review comments

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebraic-topology Algebraic topology

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@quantumsnow @joelriou @chrisflav @grunweg