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 (CategoryTheory.Functor.comp P F)
For every sheaf
P,P ⋙ Fis a sheaf.
Instances
@[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)
[CategoryTheory.GrothendieckTopology.HasSheafCompose J F]
:
∀ {X Y : CategoryTheory.Sheaf J A} (η : X ⟶ Y),
((CategoryTheory.sheafCompose J F).toPrefunctor.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)
[CategoryTheory.GrothendieckTopology.HasSheafCompose J F]
(G : CategoryTheory.Sheaf J A)
:
((CategoryTheory.sheafCompose J F).toPrefunctor.obj G).val = CategoryTheory.Functor.comp G.val 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)
[CategoryTheory.GrothendieckTopology.HasSheafCompose J 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
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)
[CategoryTheory.GrothendieckTopology.HasSheafCompose J F]
[CategoryTheory.GrothendieckTopology.HasSheafCompose 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 η = CategoryTheory.NatTrans.mk fun (X : CategoryTheory.Sheaf J A) => { val := CategoryTheory.whiskerLeft X.val η }
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}
[CategoryTheory.GrothendieckTopology.HasSheafCompose J 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)
[CategoryTheory.GrothendieckTopology.HasSheafCompose J F]
[CategoryTheory.GrothendieckTopology.HasSheafCompose J G]
[CategoryTheory.GrothendieckTopology.HasSheafCompose J H]
:
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 : CategoryTheory.GrothendieckTopology.Cover J X)
:
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_app_left
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).app
(CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToIso
(_ :
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a))
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_right
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).app
(CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToIso
(_ :
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b))
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_left
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app
(CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a))
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_right
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app
(CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b))
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_left
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app
(CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Functor.comp
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S P))
F).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Functor.comp
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S P))
F).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.left a))
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_right
{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 : CategoryTheory.GrothendieckTopology.Cover J X)
(b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R)
:
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app
(CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToHom
(_ :
(CategoryTheory.Functor.comp
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S P))
F).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Functor.comp
(CategoryTheory.Limits.MulticospanIndex.multicospan
(CategoryTheory.GrothendieckTopology.Cover.index S P))
F).toPrefunctor.obj
(CategoryTheory.Limits.WalkingMulticospan.right b))
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 : CategoryTheory.GrothendieckTopology.Cover J X)
:
F.mapCone (CategoryTheory.GrothendieckTopology.Cover.multifork S P) ≅ (CategoryTheory.Limits.Cones.postcompose
(CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom).toPrefunctor.obj
(CategoryTheory.GrothendieckTopology.Cover.multifork S (CategoryTheory.Functor.comp P 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
- One or more equations did not get rendered due to their size.
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 : CategoryTheory.GrothendieckTopology.Cover J X) →
(P : CategoryTheory.Functor Cᵒᵖ A) →
CategoryTheory.Limits.PreservesLimit
(CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) 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]
:
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.