[Merged by Bors] - feat: Algebra.Homology.ShortComplex.Basic#4203
[Merged by Bors] - feat: Algebra.Homology.ShortComplex.Basic#4203
Conversation
joelriou
changed the title
kbuzzard
left a comment
kbuzzard
left a comment
There was a problem hiding this comment.
This all looks very uncontroversial :-) I left some minor comments.
| of two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` such that | ||
| `f ≫ g = 0`. -/ | ||
| structure ShortComplex [HasZeroMorphisms C] where | ||
| /-- the three objects of a `ShortComplex` -/ |
There was a problem hiding this comment.
heh heh, nice try :-) This gives that docstring to all three of the fields X1, X2, X3. Is that what you wanted?
| This file defines the category `ShortComplex C` of diagrams | ||
| `X₁ ⟶ X₂ ⟶ X₃` such that the composition is zero. | ||
|
|
||
| TODO: An homology API for these objects shall be developped |
There was a problem hiding this comment.
| TODO: An homology API for these objects shall be developped | |
| TODO: A homology API for these objects shall be developed |
| hom := ⟨e₁.hom, e₂.hom, e₃.hom, comm₁₂, comm₂₃⟩ | ||
| inv := homMk e₁.inv e₂.inv e₃.inv | ||
| (by rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id, | ||
| ← comm₁₂, e₁.inv_hom_id_assoc]) |
There was a problem hiding this comment.
I don't know if the spacing is correct here. Should this be under the rw rather than under the by? Not sure.
| lemma isIso_of_isIso (f : S₁ ⟶ S₂) [IsIso f.τ₁] [IsIso f.τ₂] [IsIso f.τ₃] : IsIso f := | ||
| IsIso.of_iso (isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃) (by aesop_cat) (by aesop_cat)) | ||
|
|
||
| /-- The opposite short_complex in `Cᵒᵖ` associated to a short complex in `C`. -/ |
There was a problem hiding this comment.
| /-- The opposite short_complex in `Cᵒᵖ` associated to a short complex in `C`. -/ | |
| /-- The opposite `ShortComplex` in `Cᵒᵖ` associated to a short complex in `C`. -/ |
| @[simp] | ||
| lemma opMap_id : opMap (𝟙 S) = 𝟙 S.op := rfl | ||
|
|
||
| /-- The short_complex in `C` associated to a short complex in `Cᵒᵖ`. -/ |
There was a problem hiding this comment.
| /-- The short_complex in `C` associated to a short complex in `Cᵒᵖ`. -/ | |
| /-- The `ShortComplex` in `C` associated to a short complex in `Cᵒᵖ`. -/ |
|
Looks great, just the remaining minor comments. bors d+ |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Thanks very much @kbuzzard & @semorrison for these reviews! bors r+ |
This PR introduces the category of short complexes `X₁ ⟶ X₂ ⟶ X₃` in a category with zero morphisms.
|
Build failed (retrying...): |
This PR introduces the category of short complexes `X₁ ⟶ X₂ ⟶ X₃` in a category with zero morphisms.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
3 participants
This PR introduces the category of short complexes
X₁ ⟶ X₂ ⟶ X₃in a category with zero morphisms.This is the first PR in a series which intends to develop the homology of these short complexes, and redefining the homology in
mathlib4. The whole code (which also includes the construction of derived categories) appear at #4197