mathlib3 documentation

category_theory.sites.pushforward

Pushforward of sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

The pushforward functor is left adjoint to the pullback functor.

Equations