Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-05 07:02 1e8f438c

View on Github →

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

Estimated changes