Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-22 05:08 64335dec

View on Github →

chore(topology/category/): switch to bundled morphisms in Top (#3506) This is a natural follow-up to @Nicknamen's recent PRs splitting bundled continuous maps out of compact_open. There is a slight regression in algebraic_geometry.presheafed_space and algebraic_geometry.stalks, requiring a more explicit coercion. I'd encourage reviewers to ignore this, as I'll make a separate PR simplifying this (basically: having a coercion from morphisms of PresheafedSpaces to morphisms of Tops is unrealistically ambitious, and moreover harder to read, than just using the projection notation, and removing it makes everything easier).

Estimated changes