PR #2174 feat(algebra/homology): chain complexes

feat(algebra/homology): chain complexes #2174

mergify merged 48 commits into master from chain_complex

thoughts on chain complexes

64c23b40

Merge remote-tracking branch 'origin/master' into chain_complex

5034cc2c

minor

a322404e

feat(category_theory): split epis and monos, and a result about (co)p…

fe8e3a4a

Merge branch 'split_mono' into chain_complex

c9837614

total functor faithful

17cfe8ae

homology!

84e6f1ac

remove lint

44153fce

something something homology

7da3a8a1

comment out broken stuff

cbee3ea5

adding comments

c36be73b

various

d78e1027

rewrite

b1621f12

merge

3921c6c0

fixes

25f56b2f

kim-em commented on 2020-03-18

Update src/category_theory/epi_mono.lean

eb8a389a

kim-em commented on 2020-03-18

Update src/category_theory/epi_mono.lean

c4cf9559

kim-em commented on 2020-03-18

Update src/category_theory/epi_mono.lean

babe6c67

cipher1024 assigned

jcommelin 6 years ago

cipher1024 assigned

rwbarton 6 years ago

better use of ext

e3442faf

Merge remote-tracking branch 'origin/master' into chain_complex

b21cd0c7

feat(category_theory): subsingleton (has_zero_morphisms)

e547914d

revert some independent changes moved to #2180

d3dcf67c

revert some independent changes moved to #2181

0b257ca6

revert independent changes moved to #2182

f1d142cd

fix

da69994b

Merge branch 'subsingleton_has_zero_morphisms' into chain_complex

7e4ae761

kim-em added blocked-by-other-PR

jcommelin commented on 2020-03-19

Apply suggestions from code review

ea7d3857

changes from review

d3e92fea

kim-em changed the title ~~feat(algebra/homology): chain complexes~~ feat(algebra/homology): chain complexes (blocked by #2180) 6 years ago

module docs

4613e0dd

kim-em changed the title ~~feat(algebra/homology): chain complexes (blocked by #2180)~~ feat(algebra/homology): chain complexes 6 years ago

kim-em removed blocked-by-other-PR

kim-em added awaiting-review

merge

f3c802c1

kim-em requested a review from

TwoFX 6 years ago

Merge remote-tracking branch 'origin/master' into chain_complex

c4260dd9

kbuzzard commented on 2020-03-21

various

7ed3b3c5

Update src/category_theory/shift.lean

c6b085a9

various

0352bc1c

Merge branch 'chain_complex' of github.com:leanprover-community/mathl…

195fcc9c

various fixes

17e4f6d8

fix

92a0bf4f

TwoFX commented on 2020-03-22

kim-em removed awaiting-review

kim-em added awaiting-author

kim-em commented on 2020-03-22

all the minor suggestions

dca405fc

Merge remote-tracking branch 'origin/master' into chain_complex

8be3226e

ugh... fix reverting stuff from #2180

e3f4c273

off by one

39d0cb11

various

5db4cb73

jcommelin commented on 2020-03-23

use abbreviation

10d94339

chain as well as cochain

34958ba8

kim-em removed awaiting-author

kim-em added awaiting-review

jcommelin commented on 2020-03-24

robertylewis removed awaiting-review

robertylewis added awaiting-author

satisfy the linter

1a024edc

some simp lemmas

74c235bc

jcommelin approved these changes on 2020-03-24

kim-em removed awaiting-author

kim-em added awaiting-review

simp lemmas

c611d763

jcommelin added ready-to-merge

jcommelin removed awaiting-review

Merge branch 'master' into chain_complex

452c0bb2

mergify merged 6e6c81a4 into master 6 years ago

robertylewis deleted the chain_complex branch 6 years ago

Reviewers

jcommelin

TwoFX

kbuzzard

Assignees

rwbarton

jcommelin

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(algebra/homology): chain complexes #2174 Merged

feat(algebra/homology): chain complexes #2174

mathlib3
feat(algebra/homology): chain complexes
#2174

Merged