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