The sheaf condition along a homeomorphism #
Mathlib's TopCat.Sheaf.pushforward_sheaf_of_sheaf says that the pushforward of a sheaf along a
continuous map is a sheaf. Along a homeomorphism the converse holds as well, since pushing forward
along the inverse undoes the pushforward. This file records the resulting criterion: a presheaf
isomorphic to the pushforward of another along a homeomorphism is a sheaf exactly when the other
is.
Main results #
TopCat.Presheaf.isSheaf_iff_of_iso_pushforward: the sheaf condition transfers along an isomorphism with a pushforward along a homeomorphism, in both directions.
theorem
TopCat.Presheaf.isSheaf_iff_of_iso_pushforward
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : TopCat}
(h : Y ≅ X)
{F : Presheaf C X}
{G : Presheaf C Y}
(α : F ≅ (pushforward C h.hom).obj G)
:
The sheaf condition transfers along a homeomorphism. If F is isomorphic to the pushforward
of G along a homeomorphism h, then F is a sheaf exactly when G is.