mathlib3
feat(topology/sheaves/*): sheaves have enough injectives under some condition
#15742
Open
Overview
Commits
95
Changes
View On GitHub

feat(topology/sheaves/*): sheaves have enough injectives under some condition #15742

jjaassoonn wants to merge 95 commits into master from jjaassoonn/sky
jjaassoonn
jjaassoonn initial
5eb1c0ba
jjaassoonn finished epi
df250671
jjaassoonn add to_additive
99553bda
jjaassoonn add doc_string
793b87b1
jjaassoonn generalize
d80df7fc
jjaassoonn add to_addtive
9a7d5c9f
jjaassoonn remove noncomputable
5170d987
jjaassoonn minor golf
370c5f32
jjaassoonn minimize import
29808f5e
jjaassoonn golf
4640408f
jjaassoonn golf
697ddd95
jjaassoonn golf
c605b390
jjaassoonn golf
e1d1cf84
jjaassoonn golf a little bit more
bf97e8bb
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/group_ep…
1f73f520
jjaassoonn apply suggestion and fix
4b3cc16e
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
f21bd67e
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
7b39fcd0
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
c039b7d9
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
ef6a749b
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
677d5425
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
02c7601f
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
99d29450
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
5fd75291
jjaassoonn add `noncomputable`
0d8ea158
jjaassoonn Merge branch 'jjaassoonn/group_epi_mono' of https://github.com/leanpr…
e6d47417
jjaassoonn reformat
c199b075
jjaassoonn initial
f82ff81f
jjaassoonn Merge remote-tracking branch 'origin/jjaassoonn/group_epi_mono' into …
5cdf35f1
jjaassoonn add missing
dab193b9
jjaassoonn add docs
38ba5c9d
jjaassoonn fix linter error
68b35237
jjaassoonn fix doc_blame error
c2f9119d
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/equiv_Gr…
0ce5f68a
jjaassoonn fix after merge master
ff66715e
jjaassoonn need cache
8af22a99
jjaassoonn calculating stalk
3f98b721
jjaassoonn add doc
5d79d135
jjaassoonn add doc
eb70d55c
erdOne
erdOne commented on 2022-07-29
hrmacbeth hrmacbeth added t-algebraic-geometry
jjaassoonn add an alternative formualtion
b3fd04e1
jjaassoonn fix
987b81f3
jjaassoonn use specializes notation
942d9e90
add documentation
0a3f9d07
adjoint: stalk functor and skyscraper functor
b16682a6
save for now
01d6a97a
skyscraper sheaf in Ab is injective when S is inj
6e6a0770
jjaassoonn Apply suggestions from code review
117fe37e
jjaassoonn apply suggestion
92d917fc
jjaassoonn fix
5630ac82
jjaassoonn fix
aa6b2d46
jjaassoonn apply change
40e544e8
jjaassoonn Update src/algebra/category/Group/epi_mono.lean
31d54dec
jjaassoonn reorder import
e305717a
jjaassoonn Merge branch 'jjaassoonn/equiv_Group_AddGroup' of https://github.com/…
f195f1b0
jjaassoonn initial
319101da
jjaassoonn fix loop
8f981a6d
jjaassoonn Merge remote-tracking branch 'origin/jjaassoonn/epi_mono_sheaves' int…
f1aefb72
jjaassoonn Merge branch 'jjaassoonn/sky' of https://github.com/leanprover-commun…
ab9b3428
jjaassoonn minimize diff
47bfa232
jjaassoonn Merge remote-tracking branch 'origin/jjaassoonn/equiv_Group_AddGroup'…
0360df75
jjaassoonn sorry free
c83f8733
jjaassoonn delete long lines
a3b397be
jjaassoonn
jjaassoonn initial
64b245e5
jjaassoonn move file
95a36634
jjaassoonn jjaassoonn changed the title feat(algebraic_geometry/skyscraper): define skyscraper (pre)sheaves and calculating their stalks feat(topology/sheves/skyscraper): skyscraper sheaves are injective if the targets are injective 3 years ago
jjaassoonn need cache
93f4f219
jjaassoonn need cache
3c964fd0
jjaassoonn make it better
085be8fd
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
c73eaa24
jjaassoonn jjaassoonn added WIP
jjaassoonn jjaassoonn added awaiting-CI
jjaassoonn fix linter error
adfff44c
jjaassoonn fix
fb707bc7
jjaassoonn move fiel
aa6a325b
jjaassoonn move file
c7c9f5f4
jjaassoonn delete unnecessary
8c38e63c
jjaassoonn Merge remote-tracking branch 'origin/jjaassoonn/sky_def' into jjaasso…
749f8fcc
jjaassoonn need cache
dc5b5d0d
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
2fdae17f
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/sky
8b13323d
jjaassoonn fix
cf4bbe8d
jjaassoonn generalize
081ff840
jjaassoonn minimize import
1cf1bbb5
jjaassoonn fix
67ad6347
jjaassoonn need cache
54292536
jjaassoonn fix and add lemma about mono in sheaves
0dbcde21
jjaassoonn fixx
729c6496
jjaassoonn commit
ffe5571f
jjaassoonn defined some auxilary isomorphism
6cfe30f7
jjaassoonn save for now
036fc2f8
jjaassoonn commit
55d4046a
jjaassoonn save
84c015d5
jjaassoonn more api
e941031e
jjaassoonn finish godement resolution
98575524
jjaassoonn jjaassoonn changed the title feat(topology/sheves/skyscraper): skyscraper sheaves are injective if the targets are injective feat(topology/sheves/skyscraper): sheaves have enough injectives under some condition 3 years ago
jjaassoonn jjaassoonn changed the title feat(topology/sheves/skyscraper): sheaves have enough injectives under some condition feat(topology/sheves/*): sheaves have enough injectives under some condition 3 years ago
jjaassoonn cache
ef039e9d
alreadydone alreadydone changed the title feat(topology/sheves/*): sheaves have enough injectives under some condition feat(topology/sheaves/*): sheaves have enough injectives under some condition 3 years ago
jjaassoonn finish
06689d18
jjaassoonn jjaassoonn removed WIP
jjaassoonn jjaassoonn removed awaiting-CI
jjaassoonn add some more lemma
02957538
jjaassoonn add some docs
28dc545d
alreadydone
alreadydone commented on 2022-08-22
jjaassoonn jjaassoonn added WIP
jjaassoonn jjaassoonn marked this pull request as draft 2 years ago
kim-em kim-em added too-late
alreadydone

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
WIP t-algebraic-geometry too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum