Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes