Commit 2023-06-29 20:50 04c1c091

View on Github →

feat: port Topology.Sheaves.Skyscraper (#4751)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Skyscraper.lean

added def SkyscraperPresheafFunctor.map'

added theorem SkyscraperPresheafFunctor.map'_comp

added theorem SkyscraperPresheafFunctor.map'_id

added def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk

added theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper

added def StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf

added theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk

added def skyscraperPresheaf

added def skyscraperPresheafCocone

added def skyscraperPresheafCoconeOfSpecializes

added def skyscraperPresheafFunctor

added def skyscraperPresheafStalkAdjunction

added def skyscraperPresheafStalkOfNotSpecializesIsTerminal

added theorem skyscraperPresheaf_eq_pushforward

added theorem skyscraperPresheaf_isSheaf

added def skyscraperSheaf

added def skyscraperSheafFunctor

added def stalkSkyscraperSheafAdjunction