mathlib3
feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings
#976
Merged
Merged
feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings #976
mergify
merged
76 commits into
master
from
presheaf-2
feat(category_theory/colimits): missing simp lemmas
25014052
feat(category_theory): functor.map_nat_iso
9d3f315a
Merge branch 'map_nat_iso' into temp
2e677bbe
fix(category_theory): presheaves, unbundled and bundled, and pushforw…
deb92bf7
restoring `(opens X)ᵒᵖ`
57936830
various changes from working on stalks
7557c2b3
rename `nbhds` to `open_nhds`
999bea62
fix introduced typo
163f0343
typo
cf32bbc1
compactify a proof
4c6db44e
rename `presheaf` to `presheaf_on_space`
377193c7
fix(category_theory): turn `has_limits` classes into structures
67331712
naming instances to avoid collisions
acb35a8c
breaking up instances.topological_spaces
dc40368a
fixing all the other pi-type typclasses
abaf382f
fix import
87cb66ba
oops
09c6d5bd
merge
19c873e0
fix import
ac39ffe7
missed one
cc77474d
typo
0e9bb4ef
WIP
b2f0262b
oops
b8654931
the presheaf of continuous functions to ℂ
1e009658
restoring eq_to_hom simp lemmas
20c7e2e8
removing unnecessary simp lemma
8f1d3e83
merge
654f8079
remove another superfluous lemma
0ba70412
removing the nat_trans and vcomp notations; use \hom and \gg
40fa3d6d
a simpler proposal
d83c45b6
getting rid of vcomp
49d299d8
fix
8e46bac8
splitting files
c9601c7d
merge
662b4aeb
renaming
299965f8
entirely remove the nat_trans double arrow
330869d1
merge
198dc96b
update notation
bfa28837
Merge branch 'presheaf' into presheaf-2
3d92ce28
fix
50ce6b26
Merge branch 'presheaf' into presheaf-2
b4d86479
merge
c313e8de
cleanup
c481adff
use iso_whisker_right instead of map_nat_iso
e436fb96
proofs magically got easier?
d002d25f
Merge branch 'presheaf' into presheaf-2
19f511ce
improve some proofs
957a004f
moving instances
36cefbc9
remove crap
3c6c352f
Merge branch 'presheaf' of github.com:leanprover-community/mathlib in…
f439c413
tidy
c07c62cc
merge master
b2fea816
merge
e9e2a346
minimise imports
99f51c84
chore(travis): disable the check for minimal imports
f550ea6a
Merge branch 'jcommelin-patch-1' of github.com:leanprover-community/m…
4708d904
Update src/algebraic_geometry/presheafed_space.lean
44eb5e43
writing `op_induction` tactic, and improving proofs
1d99d8b5
squeeze_simping
a037c53d
cleanup
3fff00e9
rearranging
dd50c250
Merge branch 'master' into presheaf
3ca5ff6f
merge
65cf6005
cleanup
15dd7243
cleaning up
5ca637d8
cleaning up
bbb97842
move
5c96415a
kim-em
changed the title
merge
dceb2761
jcommelin
commented
on 2019-05-06
Update src/category_theory/instances/Top/presheaf_of_functions.lean
f430dbf9
fixes in response to review
cda5885c
merge
157eea53
Merge branch 'master' into presheaf-2
43f1f1c3
fpvandoorn
approved these changes
on 2019-05-13
jcommelin
approved these changes
on 2019-05-13
Merge branch 'master' into 'presheaf-2'
89a43ca6
Merge branch 'master' into 'presheaf-2'
e6f076eb
Merge branch 'master' into 'presheaf-2'
585bc269
Merge branch 'master' into 'presheaf-2'
ea728965
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub