Commit 2019-05-13 15:42 70cd00bc
View on Github →feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings (#976)
- 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
- 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
- update notation
- fix
- 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
- Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com
- fixes in response to review