Commit 2023-05-18 16:02 c0be162f

View on Github →

feat: port Topology.Sheaves.Presheaf (#3828)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/Init.lean

Created Mathlib/Topology/Sheaves/Presheaf.lean

added def TopCat.Presheaf.Pullback.id

added theorem TopCat.Presheaf.Pullback.id_inv_app

added def TopCat.Presheaf.Pushforward.comp

added theorem TopCat.Presheaf.Pushforward.comp_eq

added theorem TopCat.Presheaf.Pushforward.comp_hom_app

added theorem TopCat.Presheaf.Pushforward.comp_inv_app

added def TopCat.Presheaf.Pushforward.id

added theorem TopCat.Presheaf.Pushforward.id_eq

added theorem TopCat.Presheaf.Pushforward.id_hom_app'

added theorem TopCat.Presheaf.Pushforward.id_hom_app

added theorem TopCat.Presheaf.Pushforward.id_inv_app'

added theorem TopCat.Presheaf.id_pushforward

added theorem TopCat.Presheaf.map_restrict

added def TopCat.Presheaf.presheafEquivOfIso

added def TopCat.Presheaf.pullback

added def TopCat.Presheaf.pullbackHomIsoPushforwardInv

added def TopCat.Presheaf.pullbackInvIsoPushforwardHom

added def TopCat.Presheaf.pullbackMap

added def TopCat.Presheaf.pullbackObj

added def TopCat.Presheaf.pullbackObjObjOfImageOpen

added theorem TopCat.Presheaf.pullbackObj_eq_pullbackObj

added def TopCat.Presheaf.pushforward

added def TopCat.Presheaf.pushforwardEq

added theorem TopCat.Presheaf.pushforwardEq_eq

added theorem TopCat.Presheaf.pushforwardEq_hom_app

added theorem TopCat.Presheaf.pushforwardEq_rfl

added def TopCat.Presheaf.pushforwardMap

added def TopCat.Presheaf.pushforwardObj

added theorem TopCat.Presheaf.pushforwardObj_map

added theorem TopCat.Presheaf.pushforwardObj_obj

added def TopCat.Presheaf.pushforwardPullbackAdjunction

added def TopCat.Presheaf.pushforwardToOfIso

added theorem TopCat.Presheaf.pushforwardToOfIso_app

added theorem TopCat.Presheaf.pushforward_eq'

added theorem TopCat.Presheaf.pushforward_eq'_hom_app

added theorem TopCat.Presheaf.pushforward_map_app'

added def TopCat.Presheaf.restrict

added theorem TopCat.Presheaf.restrict_restrict

added def TopCat.Presheaf.toPushforwardOfIso

added theorem TopCat.Presheaf.toPushforwardOfIso_app

added def TopCat.Presheaf