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
tofunctor.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
toopen_nhds
- fix introduced typo
- typo
- compactify a proof
- rename
presheaf
topresheaf_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