Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.
Draft
Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
95 commits
Select commit Hold shift + click to select a range
5eb1c0b
initial
jjaassoonn Jun 13, 2022
df25067
finished epi
jjaassoonn Jun 13, 2022
99553bd
add to_additive
jjaassoonn Jun 13, 2022
793b87b
add doc_string
jjaassoonn Jun 13, 2022
d80df7f
generalize
jjaassoonn Jun 15, 2022
9a7d5c9
add to_addtive
jjaassoonn Jun 15, 2022
5170d98
remove noncomputable
jjaassoonn Jun 15, 2022
370c5f3
minor golf
jjaassoonn Jun 15, 2022
29808f5
minimize import
jjaassoonn Jun 15, 2022
4640408
golf
jjaassoonn Jun 17, 2022
697ddd9
golf
jjaassoonn Jun 17, 2022
c605b39
golf
jjaassoonn Jun 17, 2022
e1d1cf8
golf
jjaassoonn Jun 17, 2022
bf97e8b
golf a little bit more
jjaassoonn Jun 17, 2022
1f73f52
Merge remote-tracking branch 'origin/master' into jjaassoonn/group_ep…
jjaassoonn Jul 17, 2022
4b3cc16
apply suggestion and fix
jjaassoonn Jul 17, 2022
f21bd67
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
7b39fcd
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
c039b7d
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
ef6a749
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
677d542
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
02c7601
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
99d2945
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
5fd7529
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Jul 18, 2022
0d8ea15
add `noncomputable`
jjaassoonn Jul 18, 2022
e6d4741
Merge branch 'jjaassoonn/group_epi_mono' of https://github.com/leanpr…
jjaassoonn Jul 18, 2022
c199b07
reformat
jjaassoonn Jul 18, 2022
f82ff81
initial
jjaassoonn Jul 18, 2022
5cdf35f
Merge remote-tracking branch 'origin/jjaassoonn/group_epi_mono' into …
jjaassoonn Jul 18, 2022
dab193b
add missing
jjaassoonn Jul 18, 2022
38ba5c9
add docs
jjaassoonn Jul 18, 2022
68b3523
fix linter error
jjaassoonn Jul 18, 2022
c2f9119
fix doc_blame error
jjaassoonn Jul 18, 2022
0ce5f68
Merge remote-tracking branch 'origin/master' into jjaassoonn/equiv_Gr…
jjaassoonn Jul 19, 2022
ff66715
fix after merge master
jjaassoonn Jul 19, 2022
8af22a9
need cache
jjaassoonn Jul 27, 2022
3f98b72
calculating stalk
jjaassoonn Jul 28, 2022
5d79d13
add doc
jjaassoonn Jul 28, 2022
eb70d55
add doc
jjaassoonn Jul 28, 2022
b3fd04e
add an alternative formualtion
jjaassoonn Jul 31, 2022
987b81f
fix
jjaassoonn Jul 31, 2022
942d9e9
use specializes notation
jjaassoonn Jul 31, 2022
0a3f9d0
add documentation
Aug 1, 2022
b16682a
adjoint: stalk functor and skyscraper functor
Aug 2, 2022
01d6a97
save for now
Aug 2, 2022
6e6a077
skyscraper sheaf in Ab is injective when S is inj
Aug 2, 2022
117fe37
Apply suggestions from code review
jjaassoonn Aug 4, 2022
92d917f
apply suggestion
jjaassoonn Aug 4, 2022
5630ac8
fix
jjaassoonn Aug 4, 2022
aa6b2d4
fix
jjaassoonn Aug 4, 2022
40e544e
apply change
jjaassoonn Aug 7, 2022
31d54de
Update src/algebra/category/Group/epi_mono.lean
jjaassoonn Aug 7, 2022
e305717
reorder import
jjaassoonn Aug 7, 2022
f195f1b
Merge branch 'jjaassoonn/equiv_Group_AddGroup' of https://github.com/…
jjaassoonn Aug 7, 2022
319101d
initial
jjaassoonn Aug 8, 2022
8f981a6
fix loop
jjaassoonn Aug 8, 2022
f1aefb7
Merge remote-tracking branch 'origin/jjaassoonn/epi_mono_sheaves' int…
jjaassoonn Aug 8, 2022
ab9b342
Merge branch 'jjaassoonn/sky' of https://github.com/leanprover-commun…
jjaassoonn Aug 8, 2022
47bfa23
minimize diff
jjaassoonn Aug 8, 2022
0360df7
Merge remote-tracking branch 'origin/jjaassoonn/equiv_Group_AddGroup'…
jjaassoonn Aug 8, 2022
c83f873
sorry free
jjaassoonn Aug 8, 2022
a3b397b
delete long lines
jjaassoonn Aug 8, 2022
64b245e
initial
jjaassoonn Aug 8, 2022
95a3663
move file
jjaassoonn Aug 8, 2022
93f4f21
need cache
jjaassoonn Aug 8, 2022
3c964fd
need cache
jjaassoonn Aug 10, 2022
085be8f
make it better
jjaassoonn Aug 10, 2022
c73eaa2
Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
jjaassoonn Aug 15, 2022
adfff44
fix linter error
jjaassoonn Aug 15, 2022
fb707bc
fix
jjaassoonn Aug 15, 2022
aa6a325
move fiel
jjaassoonn Aug 16, 2022
c7c9f5f
move file
jjaassoonn Aug 16, 2022
8c38e63
delete unnecessary
jjaassoonn Aug 16, 2022
749f8fc
Merge remote-tracking branch 'origin/jjaassoonn/sky_def' into jjaasso…
jjaassoonn Aug 16, 2022
dc5b5d0
need cache
jjaassoonn Aug 16, 2022
2fdae17
Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
jjaassoonn Aug 16, 2022
8b13323
Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
jjaassoonn Aug 16, 2022
cf4bbe8
fix
jjaassoonn Aug 16, 2022
081ff84
generalize
jjaassoonn Aug 16, 2022
1cf1bbb
minimize import
jjaassoonn Aug 16, 2022
67ad634
fix
jjaassoonn Aug 16, 2022
5429253
need cache
jjaassoonn Aug 17, 2022
0dbcde2
fix and add lemma about mono in sheaves
jjaassoonn Aug 17, 2022
729c649
fixx
jjaassoonn Aug 17, 2022
ffe5571
commit
jjaassoonn Aug 17, 2022
6cfe30f
defined some auxilary isomorphism
jjaassoonn Aug 19, 2022
036fc2f
save for now
jjaassoonn Aug 19, 2022
55d4046
commit
jjaassoonn Aug 19, 2022
84c015d
save
jjaassoonn Aug 19, 2022
e941031
more api
jjaassoonn Aug 19, 2022
9857552
finish godement resolution
jjaassoonn Aug 20, 2022
ef039e9
cache
jjaassoonn Aug 21, 2022
06689d1
finish
jjaassoonn Aug 21, 2022
0295753
add some more lemma
jjaassoonn Aug 21, 2022
28dc545
add some docs
jjaassoonn Aug 21, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading