mathlib

70cd00bc - feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings (#976)

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` 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 * 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