CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf

theorem CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor A B} [self : J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)

This theorem states that, given a category `C`, a category `A`, and a category `B` with a Grothendieck topology `J` on `C`, as well as a functor `F` from `A` to `B`, if we have a presheaf `P` from `C` to `A` that is a sheaf with respect to `J`, then the composition `P ⋙ F` (which is a functor from `C` to `B`) is also a sheaf with respect to `J`. This is true for every sheaf `P`.

More concisely: Given a functor `F: A → B` from category `A` to category `B`, a Grothendieck topology `J` on category `C`, and a sheaf `P: C → A` on `C` with respect to `J`, then the composition `P ⋙ F: C → B` is also a sheaf on `C` with respect to `J`.