mathlib

47efcf3c - chore(algebraic_geometry/presheafed_space): use projection rather than fancy coercion (#3507)

chore(algebraic_geometry/presheafed_space): use projection rather than fancy coercion (#3507) We'd gone to great effort when writing `PresheafedSpace` to create a coercion from morphisms of `PresheafedSpace`s to morphisms in `Top`. It's hard to read, it's fragile. So this PR rips out that coercion, and renames the "continuous map between base spaces" field from `f` to `base`, and uses that throughout. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>