[Merged by Bors] - feat(algebra/homology): redesign of homological complexes #7473
Conversation
This file contains 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
|
Deprecates #7375. This only has part of the content from that PR, but extensively updated. The remainder of that content, and much more, is coming in subsequent PRs! |
This was referenced May 4, 2021
[Merged by Bors] - feat(algebra/homology/single): chain complexes supported in a single degree
#7477
Closed
Co-authored-by: Johan Commelin <johan@commelin.net>
github-actions
bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
jcommelin
reviewed
May 7, 2021
adamtopaz
reviewed
May 7, 2021
|
|
||
| variables (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : d₁ ≫ d₀ = 0) | ||
| (succ : Π (t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁), d₁ ≫ d₀ = 0), | ||
| Σ' (X₃ : V) (d₂ : X₃ ⟶ t.2.2.1), d₂ ≫ t.2.2.2.2.1 = 0) |
There was a problem hiding this comment.
This t.2.2.2.2.1 makes me think it might be better to just use mk_struct instead of the flat version. Is there any benefit to using a sigma type?
There was a problem hiding this comment.
@adamtopaz I don't have sufficient overview, but I feel like Scott need sigma types heavily for construction projective resolutions etc...
There was a problem hiding this comment.
I didn't want mk_struct to become part of the public API, but rather to stay hidden as an implementation detail of chain_complex.mk.
bryangingechen
added
the
awaiting-review
adamtopaz
approved these changes
May 10, 2021
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
May 11, 2021
This is a complete redesign of our library on homological complexes and homology. This PR replaces the current definition of `chain_complex` which had proved cumbersome to work with. The fundamental change is that chain complexes are now indexed by a type equipped with a `complex_shape`, rather than by a monoid. A `complex_shape ι` contains a relation `r`, with the intent that we will only allow a differential `X i ⟶ X j` when `r i j`. This allows, for example, complexes indexed either by `nat` or `int`, with differentials going either up or down. We set up the initial theory without referring to "successors" and "predecessors" in the type `ι`, to ensure we can avoid dependent type theory hell issues involving arithmetic in the index of a chain group. We achieve this by having a chain complex consist of morphisms `d i j : X i ⟶ X j` for all `i j`, but with an additional axiom saying this map is zero unless `r i j`. This means we can easily talk about, e.g., morphisms from `X (i - 1 + 1)` to `X (i + 1)` when we need to. However after not too long we also set up `option` valued `next` and `prev` functions which make an arbitrary choice of such successors and predecessors if they exist. Using these, we define morphisms `d_to j`, which lands in `X j`, and has source either `X i` for some `r i j`, or the zero object if these isn't such an `i`. These morphisms are very convenient when working "at the edge of a complex", e.g. when indexing by `nat`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This is a complete redesign of our library on homological complexes and homology.
This PR replaces the current definition of
chain_complexwhich had proved cumbersome to work with.The fundamental change is that chain complexes are now indexed by a type equipped with a
complex_shape, rather than by a monoid. Acomplex_shape ιcontains a relationr, with the intent that we will only allow a differentialX i ⟶ X jwhenr i j. This allows, for example, complexes indexed either bynatorint, with differentials going either up or down.We set up the initial theory without referring to "successors" and "predecessors" in the type
ι, to ensure we can avoid dependent type theory hell issues involving arithmetic in the index of a chain group. We achieve this by having a chain complex consist of morphismsd i j : X i ⟶ X jfor alli j, but with an additional axiom saying this map is zero unlessr i j. This means we can easily talk about, e.g., morphisms fromX (i - 1 + 1)toX (i + 1)when we need to.However after not too long we also set up
optionvaluednextandprevfunctions which make an arbitrary choice of such successors and predecessors if they exist. Using these, we define morphismsd_to j, which lands inX j, and has source eitherX ifor somer i j, or the zero object if these isn't such ani. These morphisms are very convenient when working "at the edge of a complex", e.g. when indexing bynat.