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₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
:
Describes the property of a functor to "preserve sheaves".
For every sheaf
P,P ⋙ Fis a sheaf.
Instances
def
CategoryTheory.sheafCompose
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : 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
@[simp]
theorem
CategoryTheory.sheafCompose_map_val
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
{X✝ Y✝ : Sheaf J A}
(η : X✝ ⟶ Y✝)
:
((sheafCompose J F).map η).val = whiskerRight η.val F
@[simp]
theorem
CategoryTheory.sheafCompose_obj_val
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
(G : Sheaf J A)
:
((sheafCompose J F).obj G).val = G.val.comp F
instance
CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
:
((sheafCompose J F).comp (sheafToPresheaf J B)).Faithful
instance
CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
[F.Full]
:
((sheafCompose J F).comp (sheafToPresheaf J B)).Full
instance
CategoryTheory.instFaithfulSheafSheafCompose
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
[F.Faithful]
:
(sheafCompose J F).Faithful
instance
CategoryTheory.instFullSheafSheafComposeOfFaithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
[F.Full]
[F.Faithful]
:
(sheafCompose J F).Full
instance
CategoryTheory.instReflectsIsomorphismsSheafSheafCompose
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[J.HasSheafCompose F]
[F.ReflectsIsomorphisms]
:
(sheafCompose J F).ReflectsIsomorphisms
def
CategoryTheory.sheafCompose_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
{F G : Functor A B}
(η : F ⟶ G)
[J.HasSheafCompose F]
[J.HasSheafCompose G]
:
sheafCompose J F ⟶ sheafCompose J 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₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
{F : Functor A B}
[J.HasSheafCompose F]
:
sheafCompose_map J (CategoryStruct.id F) = CategoryStruct.id (sheafCompose J F)
@[simp]
theorem
CategoryTheory.sheafCompose_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
{F G : Functor A B}
(H : Functor A B)
(η : F ⟶ G)
(γ : G ⟶ H)
[J.HasSheafCompose F]
[J.HasSheafCompose G]
[J.HasSheafCompose H]
:
sheafCompose_map J (CategoryStruct.comp η γ) = CategoryStruct.comp (sheafCompose_map J η) (sheafCompose_map J γ)
def
CategoryTheory.GrothendieckTopology.Cover.multicospanComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
{J : GrothendieckTopology C}
(F : Functor A B)
(P : 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
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
{J : GrothendieckTopology C}
(F : Functor A B)
(P : Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
(X✝ : Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo)
:
(multicospanComp F P S).hom.app X✝ = (match X✝ with
| Limits.WalkingMulticospan.left a => Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
| Limits.WalkingMulticospan.right a => Iso.refl (F.obj (P.obj (Opposite.op a.r.Z)))).hom
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
{J : GrothendieckTopology C}
(F : Functor A B)
(P : Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
(X✝ : Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo)
:
(multicospanComp F P S).inv.app X✝ = (match X✝ with
| Limits.WalkingMulticospan.left a => Iso.refl (F.obj (P.obj (Opposite.op a.Y)))
| Limits.WalkingMulticospan.right a => Iso.refl (F.obj (P.obj (Opposite.op a.r.Z)))).inv
def
CategoryTheory.GrothendieckTopology.Cover.mapMultifork
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
{J : GrothendieckTopology C}
(F : Functor A B)
(P : Functor Cᵒᵖ A)
{X : C}
(S : J.Cover X)
:
F.mapCone (S.multifork P) ≅ (Limits.Cones.postcompose (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₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
(F : Functor A B)
[∀ (X : C) (S : J.Cover X) (P : Functor Cᵒᵖ A), 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.
instance
CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{B : Type u₃}
[Category.{v₃, u₃} B]
(J : GrothendieckTopology C)
{F : Functor A B}
[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.
theorem
CategoryTheory.Sheaf.isSeparated
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
[HasForget A]
[J.HasSheafCompose (forget A)]
(F : Sheaf J A)
:
Presheaf.IsSeparated J F.val
theorem
CategoryTheory.Presheaf.IsSheaf.isSeparated
{C : Type u₁}
[Category.{v₁, u₁} C]
{A : Type u₂}
[Category.{v₂, u₂} A]
{J : GrothendieckTopology C}
{F : Functor Cᵒᵖ A}
[HasForget A]
[J.HasSheafCompose (forget A)]
(hF : IsSheaf J F)
:
IsSeparated J F