Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-29 11:10 d935bc31

View on Github →

feat(presheaves/stalks): stalks of presheafs, and presheafed spaces with extra structure on stalks (#1018)

  • 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
  • feat(category_theory): stalks of sheaves
  • renaming
  • fixes after rebase
  • nothing
  • yay, got rid of the @s
  • attempting a very general version of structured stalks
  • 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
  • probably working again?
  • update notation
  • remove old lemma
  • fix
  • comment out unfinished stuff
  • 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
  • cleaning up
  • structured stalks
  • comment
  • structured stalks
  • more simp lemmas
  • formatting
  • Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com
  • fixes in response to review
  • tidy regressions... :-(
  • oops
  • Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/category_theory/instances/TopCommRing/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • def to lemma
  • remove useless lemma
  • explicit associator
  • broken
  • can't get proofs to work...
  • remove superfluous imports
  • missing headers
  • change example
  • reverting changes to tidy
  • remove presheaf_Z, as it doesn't work at the moment
  • fixes
  • fixes
  • fix
  • postponing stuff on structured stalks for a later PR
  • coercions
  • getting rid of all the erw
  • omitting some proofs
  • deleting more proofs
  • convert begin ... end to by
  • local

Estimated changes