mathlib

1e8f438c - feat(presheaves) (#886)

feat(presheaves) (#886) * 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 * missed one * typo * 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 * update notation * fix * cleanup * use iso_whisker_right instead of map_nat_iso * proofs magically got easier? * improve some proofs * remove crap * 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 * Update src/category_theory/instances/Top/presheaf.lean Co-Authored-By: semorrison <scott@tqft.net> * fix `open` statements, and use `op_induction` * rename terms of PresheafedSpace to X Y Z. rename field from .X to .to_Top * forgetful functor * update comments about unfortunate proofs * add coercion from morphisms of PresheafedSpaces to morphisms in Top