In this file we construct the functor Sheaf J A ⥤ Sheaf J B between sheaf categories
obtained by composition with a functor F : A ⥤ B.
In order for the sheaf condition to be preserved, F must preserve the correct limits.
The lemma Presheaf.IsSheaf.comp says that composition with such an F indeed preserves the
sheaf condition.
The functor between sheaf categories is called sheafCompose J F.
Given a natural transformation η : F ⟶ G, we obtain a natural transformation
sheafCompose J F ⟶ sheafCompose J G, which we call sheafCompose_map J η.
class
CategoryTheory.GrothendieckTopology.HasSheafCompose
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
:
Describes the property of a functor to "preserve sheaves".
- isSheaf : ∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)
For every sheaf
P,P ⋙ Fis a sheaf.
Instances
theorem
CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
{J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Functor A B}
[self : J.HasSheafCompose F]
(P : CategoryTheory.Functor Cᵒᵖ A)
(hP : CategoryTheory.Presheaf.IsSheaf J P)
:
CategoryTheory.Presheaf.IsSheaf J (P.comp F)
For every sheaf P, P ⋙ F is a sheaf.
@[simp]
theorem
CategoryTheory.sheafCompose_map_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
:
∀ {X Y : CategoryTheory.Sheaf J A} (η : X ⟶ Y),
((CategoryTheory.sheafCompose J F).map η).val = CategoryTheory.whiskerRight η.val F
@[simp]
theorem
CategoryTheory.sheafCompose_obj_val
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
(G : CategoryTheory.Sheaf J A)
:
((CategoryTheory.sheafCompose J F).obj G).val = G.val.comp F
def
CategoryTheory.sheafCompose
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
:
Composing a functor which HasSheafCompose, yields a functor between sheaf categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
:
((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
[F.Full]
:
((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.instFaithfulSheafSheafCompose
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
:
(CategoryTheory.sheafCompose J F).Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.instFullSheafSheafComposeOfFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
[F.Full]
[F.Faithful]
:
(CategoryTheory.sheafCompose J F).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.instReflectsIsomorphismsSheafSheafCompose
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[J.HasSheafCompose F]
[F.ReflectsIsomorphisms]
:
(CategoryTheory.sheafCompose J F).ReflectsIsomorphisms
Equations
- ⋯ = ⋯
def
CategoryTheory.sheafCompose_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor A B}
{G : CategoryTheory.Functor A B}
(η : F ⟶ G)
[J.HasSheafCompose F]
[J.HasSheafCompose G]
:
If η : F ⟶ G is a natural transformation then we obtain a morphism of functors
sheafCompose J F ⟶ sheafCompose J G by whiskering with η on the level of presheaves.
Equations
- CategoryTheory.sheafCompose_map J η = { app := fun (X : CategoryTheory.Sheaf J A) => { val := CategoryTheory.whiskerLeft X.val η }, naturality := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.sheafCompose_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor A B}
[J.HasSheafCompose F]
:
@[simp]
theorem
CategoryTheory.sheafCompose_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor A B}
{G : CategoryTheory.Functor A B}
(H : CategoryTheory.Functor A B)
(η : F ⟶ G)
(γ : G ⟶ H)
[J.HasSheafCompose F]
[J.HasSheafCompose G]
[J.HasSheafCompose H]
:
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
{J : CategoryTheory.GrothendieckTopology C}
(F : CategoryTheory.Functor A B)
(P : CategoryTheory.Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X✝)
(X : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app X = (match X with
| CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
| CategoryTheory.Limits.WalkingMulticospan.right b =>
CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).inv
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
{J : CategoryTheory.GrothendieckTopology C}
(F : CategoryTheory.Functor A B)
(P : CategoryTheory.Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X✝)
(X : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app X = (match X with
| CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
| CategoryTheory.Limits.WalkingMulticospan.right b =>
CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).hom
def
CategoryTheory.GrothendieckTopology.Cover.multicospanComp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
{J : CategoryTheory.GrothendieckTopology C}
(F : CategoryTheory.Functor A B)
(P : CategoryTheory.Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
:
(S.index (P.comp F)).multicospan ≅ (S.index P).multicospan.comp F
The multicospan associated to a cover S : J.Cover X and a presheaf of the form P ⋙ F
is isomorphic to the composition of the multicospan associated to S and P,
composed with F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.GrothendieckTopology.Cover.mapMultifork
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
{J : CategoryTheory.GrothendieckTopology C}
(F : CategoryTheory.Functor A B)
(P : CategoryTheory.Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
:
F.mapCone (S.multifork P) ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom).obj
(S.multifork (P.comp F))
Mapping the multifork associated to a cover S : J.Cover X and a presheaf P with
respect to a functor F is isomorphic (upto a natural isomorphism of the underlying functors)
to the multifork associated to S and P ⋙ F.
Equations
- CategoryTheory.GrothendieckTopology.Cover.mapMultifork F P S = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (F.mapCone (S.multifork P)).pt) ⋯
Instances For
instance
CategoryTheory.hasSheafCompose_of_preservesMulticospan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
(F : CategoryTheory.Functor A B)
[(X : C) →
(S : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ A) → CategoryTheory.Limits.PreservesLimit (S.index P).multicospan F]
:
J.HasSheafCompose F
Composing a sheaf with a functor preserving the limit of (S.index P).multicospan yields a functor
between sheaf categories.
Equations
- ⋯ = ⋯
instance
CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{B : Type u₃}
[CategoryTheory.Category.{v₃, u₃} B]
(J : CategoryTheory.GrothendieckTopology C)
{F : CategoryTheory.Functor A B}
[CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} F]
:
J.HasSheafCompose F
Composing a sheaf with a functor preserving limits of the same size as the hom sets in C yields a
functor between sheaf categories.
Note: the size of the limit that F is required to preserve in
hasSheafCompose_of_preservesMulticospan is in general larger than this.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Sheaf.isSeparated
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{J : CategoryTheory.GrothendieckTopology C}
[CategoryTheory.ConcreteCategory A]
[J.HasSheafCompose (CategoryTheory.forget A)]
(F : CategoryTheory.Sheaf J A)
:
theorem
CategoryTheory.Presheaf.IsSheaf.isSeparated
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : Type u₂}
[CategoryTheory.Category.{v₂, u₂} A]
{J : CategoryTheory.GrothendieckTopology C}
{F : CategoryTheory.Functor Cᵒᵖ A}
[CategoryTheory.ConcreteCategory A]
[J.HasSheafCompose (CategoryTheory.forget A)]
(hF : CategoryTheory.Presheaf.IsSheaf J F)
: