Loogle!

Result

Found 47 declarations mentioning CategoryTheory.sheafCompose.

• CategoryTheory.sheafCompose 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)
• CategoryTheory.fullyFaithfulSheafCompose 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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] (hF : F.FullyFaithful) : (CategoryTheory.sheafCompose J F).FullyFaithful
• CategoryTheory.instFaithfulSheafSheafCompose 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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
• CategoryTheory.instReflectsIsomorphismsSheafSheafCompose 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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
• CategoryTheory.instFullSheafSheafComposeOfFaithful 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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
• CategoryTheory.fullyFaithfulSheafComposeCompSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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] (hF : F.FullyFaithful) : ((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).FullyFaithful
• CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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
• CategoryTheory.sheafCompose_obj_obj 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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 : CategoryTheory.Sheaf J A) : ((CategoryTheory.sheafCompose J F).obj X).obj = X.obj.comp F
• CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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
• CategoryTheory.sheafCompose_map 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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 G : CategoryTheory.Functor A B} (η : F ⟶ G) [J.HasSheafCompose F] [J.HasSheafCompose G] : CategoryTheory.sheafCompose J F ⟶ CategoryTheory.sheafCompose J G
• CategoryTheory.sheafCompose_id 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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] : CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafCompose J F)
• CategoryTheory.sheafCompose_comp 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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 G : CategoryTheory.Functor A B} (H : CategoryTheory.Functor A B) (η : F ⟶ G) (γ : G ⟶ H) [J.HasSheafCompose F] [J.HasSheafCompose G] [J.HasSheafCompose H] : CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafCompose_map J η) (CategoryTheory.sheafCompose_map J γ)
• CategoryTheory.sheafCompose_map_hom 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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} (f : X✝ ⟶ Y✝) : ((CategoryTheory.sheafCompose J F).map f).hom = CategoryTheory.Functor.whiskerRight f.hom F
• CategoryTheory.sheafComposeNatIso 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ≅ G₁.comp (CategoryTheory.sheafCompose J F)
• CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
• CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : J.PreservesSheafification F ↔ CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
• CategoryTheory.sheafComposeNatTrans 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ⟶ G₁.comp (CategoryTheory.sheafCompose J F)
• CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E))
• CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.IsIso ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P)
• CategoryTheory.sheafComposeNatTrans_fac 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map ((CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P)) = CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F
• CategoryTheory.sheafComposeNatTrans_app_uniq 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) (α : G₂.obj (P.comp F) ⟶ (CategoryTheory.sheafCompose J F).obj (G₁.obj P)) (hα : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map α) = CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F) : α = (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P
• CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Category.{v_4, u_4} E] (F : CategoryTheory.Functor D E) [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] [∀ (J : CategoryTheory.Limits.MulticospanShape), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafToPresheaf J E).map ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P) = (J.sheafifyCompIso F P).inv
• CategoryTheory.Sheaf.isLocallyInjective_forget 📋 Mathlib.CategoryTheory.Sites.LocallyInjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {FD : D → D → Type u_1} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C} {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget D)] [CategoryTheory.Sheaf.IsLocallyInjective φ] : CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.sheafCompose J (CategoryTheory.forget D)).map φ)
• CategoryTheory.Sheaf.instIsLocallySurjectiveFunMapTypeSheafComposeForget 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Sheaf.IsLocallySurjective φ] : CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.sheafCompose J (CategoryTheory.forget A)).map φ)
• SheafOfModules.forgetToSheafModuleCatOfIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X Y : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hY : CategoryTheory.Limits.IsInitial Y) (φ : X ≅ Y) : SheafOfModules.forgetToSheafModuleCat R X hX ≅ (SheafOfModules.forgetToSheafModuleCat R Y hY).comp (CategoryTheory.sheafCompose J (ModuleCat.restrictScalars (RingCat.Hom.hom (R.obj.map φ.hom))))
• CategoryTheory.GrothendieckTopology.uliftYoneda_map_hom_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) (x : ULift.{w, v} (((CategoryTheory.sheafToPresheaf J (Type v)).obj (J.yoneda.obj X✝)).obj X)) : ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).map f).hom.app X)) x).down = CategoryTheory.CategoryStruct.comp x.down f
• SheafOfModules.pushforwardCompForgetToSheafModuleCat 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hX' : CategoryTheory.Limits.IsInitial (F.op.obj X)) : (SheafOfModules.pushforward φ).comp (SheafOfModules.forgetToSheafModuleCat S X hX) ≅ (SheafOfModules.forgetToSheafModuleCat R (F.op.obj X) hX').comp ((CategoryTheory.sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X)))).comp (F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K))
• AlgebraicGeometry.Scheme.Modules.sheafComposePushforwardComp 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {R S : CommRingCat} (φ : R ⟶ S) : (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map φ))))).comp ((TopCat.Sheaf.pushforward (ModuleCat ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))) (AlgebraicGeometry.Spec.map φ).base).comp (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv)))) ≅ (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec S)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso S).inv))).comp ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (AlgebraicGeometry.Spec.map φ).base).comp (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))
• AlgebraicGeometry.pushforwardCompModulesSpecToSheafIso 📋 Mathlib.AlgebraicGeometry.Modules.Tilde
  {R S : CommRingCat} (φ : R ⟶ S) : (AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).comp AlgebraicGeometry.modulesSpecToSheaf ≅ AlgebraicGeometry.modulesSpecToSheaf.comp ((TopCat.Sheaf.pushforward (ModuleCat ↑S) (AlgebraicGeometry.Spec.map φ).base).comp (CategoryTheory.sheafCompose (Opens.grothendieckTopology ↥(AlgebraicGeometry.Spec R)) (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))))
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] : (CategoryTheory.sheafCompose J F).comp Φ.sheafFiber ≅ Φ.sheafFiber.comp F
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).hom.app X = CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app X.obj) (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj)))
• CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B) [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] [J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A) : (Φ.sheafFiberCompIso F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj))) ((Φ.presheafFiberCompIso F).inv.app X.obj)
• CategoryTheory.instIsConstantObjSheafSheafCompose 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [h : CategoryTheory.Sheaf.IsConstant J F] : CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)
• CategoryTheory.constantCommuteCompose 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] : (CategoryTheory.constantSheaf J D).comp (CategoryTheory.sheafCompose J U) ≅ U.comp (CategoryTheory.constantSheaf J B)
• CategoryTheory.Sheaf.isConstant_of_forget 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] [CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F
• CategoryTheory.Sheaf.isConstant_iff_forget 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)
• CategoryTheory.constantCommuteCompose_hom_app_hom 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : D) : ((CategoryTheory.constantCommuteCompose J U).hom.app X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)
• CategoryTheory.constantCommuteCompose_hom_app_val 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (X : D) : ((CategoryTheory.constantCommuteCompose J U).hom.app X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)
• CategoryTheory.constantSheafAdj_counit_w 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T))) ((CategoryTheory.constantSheafAdj J B hT).counit.app ((CategoryTheory.sheafCompose J U).obj F)) = (CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_apply_hom_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type (max v' v))) (a✝ : (((CategoryTheory.evaluation Cᵒᵖ (Type (max v v'))).comp (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max v v')) (Type (max (max v v') u))).obj CategoryTheory.uliftFunctor.{u, max v v'}).comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type (max v v'))) (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj (CategoryTheory.sheafToPresheaf J (Type (max v v')))))).obj X).obj X✝) (X✝¹ : Cᵒᵖ) (a✝¹ : (Opposite.unop (((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).comp (CategoryTheory.sheafToPresheaf J (Type (max v v')))).op.obj X)).obj X✝¹) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.inv.app X).app X✝)) a✝).hom.app X✝¹)) a✝¹ = ((((CategoryTheory.uliftYonedaOpCompCoyoneda.inv.app X).app X✝.obj).hom' a✝).app X✝¹).hom' (((J.uliftYonedaCompSheafToPresheaf.hom.app (Opposite.unop X)).app X✝¹).hom' a✝¹)
• CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_hom_apply_down 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : Cᵒᵖ) (X✝ : CategoryTheory.Sheaf J (Type (max v' v))) (a✝ : (((J.yoneda.op.comp (CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).op).comp CategoryTheory.coyoneda).obj X).obj X✝) : ((CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaOpCompCoyoneda.hom.app X).app X✝)) a✝).down = CategoryTheory.uliftYonedaEquiv ((CategoryTheory.CategoryStruct.comp ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app (Opposite.op ((CategoryTheory.sheafCompose J CategoryTheory.uliftFunctor.{v', v}).obj (J.yoneda.obj (Opposite.unop X))))).app X✝) (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (J.uliftYonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom' a✝)
• CategoryTheory.Sheaf.adjunction 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) : CategoryTheory.Sheaf.composeAndSheafify J G ⊣ CategoryTheory.sheafCompose J F
• CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} [CategoryTheory.HasWeakSheafify J D] [F.IsRightAdjoint] : (CategoryTheory.sheafCompose J F).IsRightAdjoint
• CategoryTheory.Sheaf.adjunction_counit_app_hom 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).hom = CategoryTheory.sheafifyLift J ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯
• CategoryTheory.Sheaf.adjunction_counit_app_val 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).hom = CategoryTheory.sheafifyLift J ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯
• CategoryTheory.Sheaf.adjunction_unit_app_hom 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) : ((CategoryTheory.Sheaf.adjunction J adj).unit.app X).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj) (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J (X.obj.comp G)) F)
• CategoryTheory.Sheaf.adjunction_unit_app_val 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) : ((CategoryTheory.Sheaf.adjunction J adj).unit.app X).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj) (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J (X.obj.comp G)) F)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c