The constant sheaf #
We define the constant sheaf functor (the sheafification of the constant presheaf)
constantSheaf : D ⥤ Sheaf J D
and prove that it is left adjoint to evaluation at a terminal
object (see constantSheafAdj
).
We also define a predicate on sheaves, Sheaf.IsConstant
, saying that a sheaf is in the
essential image of the constant sheaf functor.
Main results #
Sheaf.isConstant_iff_isIso_counit_app
: Provided that the constant sheaf functor is fully faithful, a sheaf is constant if and only if the counit of the constant sheaf adjunction applied to it is an isomorphism.Sheaf.isConstant_iff_of_equivalence
: The property of a sheaf of being constant is invariant under equivalence of sheaf categories.Sheaf.isConstant_iff_forget
: Given a "forgetful" functorU : D ⥤ B
a sheafF : Sheaf J D
is constant if and only if the sheaf given by postcomposition withU
is constant.
The constant presheaf functor is left adjoint to evaluation at a terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor which maps an object of D
to the constant sheaf at that object, i.e. the
sheafification of the constant presheaf.
Equations
Instances For
The constant sheaf functor is left adjoint to evaluation at a terminal object.
Equations
- CategoryTheory.constantSheafAdj J D hT = (CategoryTheory.constantPresheafAdj D hT).comp (CategoryTheory.sheafificationAdjunction J D)
Instances For
A sheaf is constant if it is in the essential image of the constant sheaf functor.
- mem_essImage : F ∈ (CategoryTheory.constantSheaf J D).essImage
Instances
Equations
- ⋯ = ⋯
If the constant sheaf functor is fully faithful, then a sheaf is constant if and only if the counit of the constant sheaf adjunction applied to it is an isomorphism.
A variant of isConstant_iff_isIso_counit_app
for a general left adjoint to evaluation at a
terminal object.
The constant sheaf functor commutes up to isomorphism the equivalence of sheaf categories induced by a dense subsite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constant sheaf functor commutes up to isomorphism the inverse equivalence of sheaf categories induced by a dense subsite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The property of a sheaf of being constant is invariant under equivalence of sheaf categories.
The constant sheaf functor commutes with sheafCompose J U
up to isomorphism, provided that U
preserves sheafification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The counit of constantSheafAdj
factors through the isomorphism constantCommuteCompose
.
Equations
- ⋯ = ⋯