Commit 2021-11-04 20:30 74c27b25View on Github →
feat(topology/sheaves): Pullback of presheaf (#9961) Defined the pullback of a presheaf along a continuous map, and proved that it is adjoint to pushforwards and it preserves stalks.
modified theorem Top.presheaf.id_pushforward
added def Top.presheaf.pullback.id
added theorem Top.presheaf.pullback.id_inv_app
added def Top.presheaf.pullback
added def Top.presheaf.pullback_map
added def Top.presheaf.pullback_obj