Commit 2019-05-29 11:10 d935bc31

View on Github →

feat(presheaves/stalks): stalks of presheafs, and presheafed spaces with extra structure on stalks (#1018)

feat(category_theory/colimits): missing simp lemmas
feat(category_theory): functor.map_nat_iso
define functor.map_nat_iso, and relate to whiskering
rename functor.on_iso to functor.map_iso
add some missing lemmas about whiskering
fix(category_theory): presheaves, unbundled and bundled, and pushforwards
restoring (opens X)ᵒᵖ
various changes from working on stalks
rename nbhds to open_nhds
fix introduced typo
typo
compactify a proof
rename presheaf to presheaf_on_space
fix(category_theory): turn has_limits classes into structures
naming instances to avoid collisions
breaking up instances.topological_spaces
fixing all the other pi-type typclasses
fix import
oops
fix import
feat(category_theory): stalks of sheaves
renaming
fixes after rebase
nothing
yay, got rid of the @s
attempting a very general version of structured stalks
missed one
typo
WIP
oops
the presheaf of continuous functions to ℂ
restoring eq_to_hom simp lemmas
removing unnecessary simp lemma
remove another superfluous lemma
removing the nat_trans and vcomp notations; use \hom and \gg
a simpler proposal
getting rid of vcomp
fix
splitting files
renaming
probably working again?
update notation
remove old lemma
fix
comment out unfinished stuff
cleanup
use iso_whisker_right instead of map_nat_iso
proofs magically got easier?
improve some proofs
moving instances
remove crap
tidy
minimise imports
chore(travis): disable the check for minimal imports
Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison scott@tqft.net
writing op_induction tactic, and improving proofs
squeeze_simping
cleanup
rearranging
cleanup
cleaning up
cleaning up
move
cleaning up
structured stalks
comment
structured stalks
more simp lemmas
formatting
Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com
fixes in response to review
tidy regressions... :-(
oops
Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/category_theory/instances/TopCommRing/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
def to lemma
remove useless lemma
explicit associator
broken
can't get proofs to work...
remove superfluous imports
missing headers
change example
reverting changes to tidy
remove presheaf_Z, as it doesn't work at the moment
fixes
fixes
fix
postponing stuff on structured stalks for a later PR
coercions
getting rid of all the erw
omitting some proofs
deleting more proofs
convert begin ... end to by
local