Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(algebra/homology): chain complexes #2174

Merged
merged 48 commits into from Mar 26, 2020
Merged

feat(algebra/homology): chain complexes #2174

merged 48 commits into from Mar 26, 2020

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Mar 18, 2020 •
edited

I don't think this is ready yet, but given others, e.g. @TwoFX, @kbuzzard, @b-mehta, are all doing things in the vicinity, I thought I'd put this out for people to look at.

This introduces graded_object, differential_object, and then defines chain_complex V as differential_object (graded_object int V). Perhaps surprisingly, this seems to work out okay in practice.

I don't do a whole lot with it: basic properties like being concrete when V is concrete, having zero morphisms and zero objects, and (non-functorial) homology groups.

(There need to be some more assumptions added before homology groups become functorial, but we're getting close now.)

Really, I want to use this as a test for my design for enriched categories. but this PR is still at the "pre-enriched" stage.

@TwoFX TwoFX added this to In progress in Homological algebra Mar 18, 2020
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 22, 2020
jcommelin
jcommelin reviewed Mar 23, 2020
View reviewed changes
src/category_theory/equivalence.lean Show resolved Hide resolved
src/category_theory/shift.lean Outdated Show resolved Hide resolved
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 24, 2020
jcommelin
jcommelin reviewed Mar 24, 2020
View reviewed changes
src/category_theory/equivalence.lean
| (int.neg_succ_of_nat 0) := e.symm
| (int.neg_succ_of_nat (n+1)) := e.symm.trans (pow (int.neg_succ_of_nat n))

instance : has_pow (C ≌ C) ℤ := ⟨pow⟩
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this come with simp-lemmas or canonical-isom-defs for the cases n in {-1, 0, 1}, and similarly for (n+1) etc?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added the simp lemmas for -1, 0, 1. I don't think we're ready yet to express the power laws like (e^a).trans (e^b) \iso e^(a+b), as we haven't even specified the category structure on equivalences, let alone the monoidal category structure on autoequivalences!

src/category_theory/graded_object.lean
def graded_object (β : Type w) (C : Type u) : Type (max w u) := β → C

-- Satisfying the inhabited linter...
instance inhabited_graded_object (β : Type w) (C : Type u) [inhabited C] :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Won't the linter complain that the instances don't have docstrings?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, the linter isn't concerned about instances, for better or worse. @fpvandoorn, have you considered adding this requirement?

@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 24, 2020
jcommelin
jcommelin approved these changes Mar 24, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm fine with merging this. I'll give others a bit of time to look over the final version.

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 24, 2020
@jcommelin jcommelin added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 25, 2020
@mergify mergify bot merged commit 6e6c81a into master Mar 26, 2020
@robertylewis robertylewis deleted the chain_complex branch March 27, 2020 13:30
@bryangingechen bryangingechen moved this from In progress to Done in Homological algebra Mar 30, 2020
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@semorrison @jcommelin
@kbuzzard @TwoFX @mergify @anrddh
feat(algebra/homology): chain complexes (leanprover-community#2174)
b7ed826 
* thoughts on chain complexes

* minor

* feat(category_theory): split epis and monos, and a result about (co)projections

* total functor faithful

* homology!

* remove lint

* something something homology

* comment out broken stuff

* adding comments

* various

* rewrite

* fixes

* Update src/category_theory/epi_mono.lean

* Update src/category_theory/epi_mono.lean

* Update src/category_theory/epi_mono.lean

* better use of ext

* feat(category_theory): subsingleton (has_zero_morphisms)

* revert some independent changes moved to leanprover-community#2180

* revert some independent changes moved to leanprover-community#2181

* revert independent changes moved to leanprover-community#2182

* fix

* Apply suggestions from code review

Co-Authored-By: Johan Commelin <johan@commelin.net>

* changes from review

* module docs

* various

* Update src/category_theory/shift.lean

Co-Authored-By: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* various

* various fixes

* fix

* all the minor suggestions

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* ugh... fix reverting stuff from leanprover-community#2180

* off by one

* various

* use abbreviation

* chain as well as cochain

* satisfy the linter

* some simp lemmas

* simp lemmas

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020
@semorrison @jcommelin
@kbuzzard @TwoFX @mergify @anrddh
feat(algebra/homology): chain complexes (leanprover-community#2174)
dfdec7c 
* thoughts on chain complexes

* minor

* feat(category_theory): split epis and monos, and a result about (co)projections

* total functor faithful

* homology!

* remove lint

* something something homology

* comment out broken stuff

* adding comments

* various

* rewrite

* fixes

* Update src/category_theory/epi_mono.lean

* Update src/category_theory/epi_mono.lean

* Update src/category_theory/epi_mono.lean

* better use of ext

* feat(category_theory): subsingleton (has_zero_morphisms)

* revert some independent changes moved to leanprover-community#2180

* revert some independent changes moved to leanprover-community#2181

* revert independent changes moved to leanprover-community#2182

* fix

* Apply suggestions from code review

Co-Authored-By: Johan Commelin <johan@commelin.net>

* changes from review

* module docs

* various

* Update src/category_theory/shift.lean

Co-Authored-By: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* various

* various fixes

* fix

* all the minor suggestions

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* ugh... fix reverting stuff from leanprover-community#2180

* off by one

* various

* use abbreviation

* chain as well as cochain

* satisfy the linter

* some simp lemmas

* simp lemmas

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

@kbuzzard kbuzzard kbuzzard left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees

@rwbarton rwbarton

@jcommelin jcommelin

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
Homological algebra
  
Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@semorrison @TwoFX @jcommelin @kbuzzard @rwbarton @robertylewis