Pullback of sheaves #
Main definitions #
CategoryTheory.Functor.sheafPullback
: the functorSheaf J A ⥤ Sheaf K A
obtained as an extension of a functorG : C ⥤ D
between the underlying categories.CategoryTheory.Functor.sheafAdjunctionContinuous
: the adjunctionG.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K
when the functorG
is continuous. In caseG
is representably flat, the pullback functor on sheaves commutes with finite limits: this is a morphism of sites in the sense of SGA 4 IV 4.9.
instance
CategoryTheory.instIsCofilteredCover
{C : Type v₁}
[CategoryTheory.SmallCategory C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
:
CategoryTheory.IsCofiltered (J.Cover X)
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.sheafPullback_map
{C : Type v₁}
[CategoryTheory.SmallCategory C]
{D : Type v₁}
[CategoryTheory.SmallCategory D]
(G : CategoryTheory.Functor C D)
(A : Type u₁)
[CategoryTheory.Category.{v₁, u₁} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
:
∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y),
(G.sheafPullback A J K).map f = (CategoryTheory.presheafToSheaf K A).map (G.op.lan.map f.val)
@[simp]
theorem
CategoryTheory.Functor.sheafPullback_obj
{C : Type v₁}
[CategoryTheory.SmallCategory C]
{D : Type v₁}
[CategoryTheory.SmallCategory D]
(G : CategoryTheory.Functor C D)
(A : Type u₁)
[CategoryTheory.Category.{v₁, u₁} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
(X : CategoryTheory.Sheaf J A)
:
(G.sheafPullback A J K).obj X = (CategoryTheory.presheafToSheaf K A).obj (G.op.lan.obj X.val)
def
CategoryTheory.Functor.sheafPullback
{C : Type v₁}
[CategoryTheory.SmallCategory C]
{D : Type v₁}
[CategoryTheory.SmallCategory D]
(G : CategoryTheory.Functor C D)
(A : Type u₁)
[CategoryTheory.Category.{v₁, u₁} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
:
The pullback functor Sheaf J A ⥤ Sheaf K A
associated to a functor G : C ⥤ D
in the
same direction as G
.
Equations
- G.sheafPullback A J K = (CategoryTheory.sheafToPresheaf J A).comp (G.op.lan.comp (CategoryTheory.presheafToSheaf K A))
Instances For
instance
CategoryTheory.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat
{C : Type v₁}
[CategoryTheory.SmallCategory C]
{D : Type v₁}
[CategoryTheory.SmallCategory D]
(G : CategoryTheory.Functor C D)
(A : Type u₁)
[CategoryTheory.Category.{v₁, u₁} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
[CategoryTheory.RepresentablyFlat G]
:
CategoryTheory.Limits.PreservesFiniteLimits (G.sheafPullback A J K)
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Functor.sheafAdjunctionContinuous
{C : Type v₁}
[CategoryTheory.SmallCategory C]
{D : Type v₁}
[CategoryTheory.SmallCategory D]
(G : CategoryTheory.Functor C D)
(A : Type u₁)
[CategoryTheory.Category.{v₁, u₁} A]
(J : CategoryTheory.GrothendieckTopology C)
(K : CategoryTheory.GrothendieckTopology D)
[CategoryTheory.ConcreteCategory A]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
[CategoryTheory.Limits.HasColimits A]
[CategoryTheory.Limits.HasLimits A]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
[(CategoryTheory.forget A).ReflectsIsomorphisms]
[G.IsContinuous J K]
:
G.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K
The pullback functor is left adjoint to the pushforward functor.
Equations
- One or more equations did not get rendered due to their size.