Theorems · Definition · category theory

TopCat.Sheaf.pushforward

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

The pushforward functor.

Defined in: Mathlib.Topology.Sheaves.Functors
Cited by: 11 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functorstatement · cited by 16,252
TopCat.carrierproof · cited by 3,184
TopCatstatement and proof · cited by 1,889
TopologicalSpace.Opens.mapproof · cited by 645
Opens.grothendieckTopologyproof · cited by 206
CategoryTheory.Functor.sheafPushforwardContinuousproof · cited by 102
TopCat.Sheafstatement · cited by 73

Cited by19

Results whose statement or proof uses this declaration.

AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpaceproof · cited by 8
ContMDiff.smoothSheafHomstatement · cited by 3
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpensstatement · cited by 3
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_isoproof · cited by 2
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eqproof · cited by 2
AlgebraicGeometry.pushforwardCompModulesSpecToSheafIsostatement and proof · cited by 1
AlgebraicGeometry.Spec.basicOpen_hom_extproof · cited by 1
ContMDiff.smoothSheafCommRingHomstatement · cited by 1
ContMDiff.smoothSheafHom_hom_app_homstatement · cited by 1
AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardCompstatement · cited by 0
TopCat.Sheaf.pullbackPushforwardAdjunctionstatement · cited by 0
TopCat.Sheaf.pushforwardForgetIsostatement and proof · cited by 0