Mathlib Map

Theorems · Definition · category theory

TopCat.Presheaf.pushforward

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} → (X ⟶ Y) → CategoryTheory.Functor (TopCat.Presheaf C X) (TopCat.Presheaf C Y)

The pushforward functor.

Defined in
Mathlib.Topology.Sheaves.Presheaf
Cited by
174 results in Mathlib
Foundations
Depth 75 from the axioms, rests on 871 definitions · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Category
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.PresheafedSpace.Hom.c · cited by 142Hom.cTopCat.Presheaf.stalkPushforward · cited by 12Presheaf.stalkPushforwardTopCat.Presheaf.pullbackPushforwardAdjunction · cited by 9Presheaf.pullbackPushforw…AlgebraicGeometry.PresheafedSpace.congr_app · cited by 9PresheafedSpace.congr_appAlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit · cited by 8PresheafedSpace.pushforwa…AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp · cited by 8IsOpenImmersion.app_invAppTopCat.Presheaf.pushforwardEq · cited by 6Presheaf.pushforwardEqTopCat.Presheaf.stalkPushforward_germ · cited by 6Presheaf.stalkPushforward…AlgebraicGeometry.PresheafedSpace.Hom.ext · cited by 6Hom.extAlgebraicGeometry.PresheafedSpace.stalkMap_germ · cited by 5PresheafedSpace.stalkMap_…AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app · cited by 5IsOpenImmersion.invApp_appAlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp · cited by 5IsOpenImmersion.inv_invAppTopCat.Presheaf.Pushforward.id · cited by 5Pushforward.idAlgebraicGeometry.PresheafedSpace.comp_c_app · cited by 5PresheafedSpace.comp_c_appAlgebraicGeometry.PresheafedSpace.id_c_app · cited by 5PresheafedSpace.id_c_appCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor.obj · cited by 19642Functor.objCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorOpposite · cited by 8081OppositeTopCat.carrier · cited by 3184TopCat.carrierTopologicalSpace.Opens · cited by 2040TopologicalSpace.OpensTopCat · cited by 1889TopCatCategoryTheory.Functor.op · cited by 997Functor.opTopologicalSpace.Opens.map · cited by 645Opens.mapCategoryTheory.Functor.whiskeringLeft · cited by 395Functor.whiskeringLeftTopCat.Presheaf · cited by 371TopCat.PresheafPresheaf.pushforwardCITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by200

Results whose statement or proof uses this declaration.