feat(category_theory/limits): kernels #1988
mergify
merged
45 commits into
leanprover-community:master
from
kernel
chore(category_theory): require morphisms live in Type
3a394670
move back to Type
647b9ece
Merge remote-tracking branch 'origin/master' into category_no_sorts
d9700b92
fixes
ec618c1a
feat(category_theory/limits): kernels
3fe06fa6
finishing basic API for kernels
eee51dbe
merge
697d86db
update post #1412
d9e38f16
Merge remote-tracking branch 'origin/master' into kernel
a88bbede
merge
81a025e8
fix
cfa15400
documentation
db14d76b
documentation
f1d036cf
more docs
f088de88
Merge branch 'master' into kernel
23c039a9
replacing dumb code
58bb08ef
forall -> Pi
191134fc
removing all instances
dd8ef659
working on Reid's suggested lemmas
0b5f3cc5
experiments
a4c2a54a
lots to do
e468f4f0
merge
f8605067
Merge branch 'master' into kernel
5da6a52d
Show that equalizers are monomorphisms
77700cd0
Show that equalizer of (f, f) is always an iso
21487269
Show that an equalizer that is an epimorphism is an isomorphism
7e6bf143
Clean up
3e3b072a
Show that the kernel of a monomorphism is zero
d6d325d4
Fix
6aad61f0
Show that the kernel of a linear map is a kernel in the categorical s…
7fa24c9a
Merge remote-tracking branch 'upstream/master' into kernel
8712dec7
Modify proof
c83d4a5f
Compactify proof
faf91ec2
Various cleanup
6eaa950c
Some more cleanup
7cd89be7
Fix bibtex
6f2f2bb6
Address some issues raised during discussion of the PR
f5f4e09e
Fix some more incorrect indentation
15ae9663
Some more minor fixes
354cfcc7
jcommelin
commented
on 2020-02-17
Unify capitalization in Bibtex entries
3cbe6956
Replace equalizer.lift.uniq with equalizer.hom_ext
9e3f032f
Some more slight refactors
8cebbeb2
jcommelin
commented
on 2020-02-19
jcommelin
commented
on 2020-02-21
kim-em
approved these changes
on 2020-02-21
kim-em
commented
on 2020-02-21
Typo
5ebb3418
jcommelin
approved these changes
on 2020-02-22
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into kernel
b36ed6be
Merge branch 'master' into kernel
3e81161a
Login to write a write a comment.
Login via GitHub