Loogle!

Result

Found 75 declarations mentioning CategoryTheory.GrothendieckTopology.HasSheafCompose.

• CategoryTheory.GrothendieckTopology.HasSheafCompose 📋 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) : Prop
• CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize 📋 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} [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} F] : J.HasSheafCompose F
• CategoryTheory.instHasSheafComposeForgetOfIsCorepresentable 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {FA : A → A → Type u_1} {CA : A → Type v₂} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [(CategoryTheory.forget A).IsCorepresentable] : J.HasSheafCompose (CategoryTheory.forget A)
• CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {A : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} A} {B : Type u₃} {inst✝² : 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)
• CategoryTheory.GrothendieckTopology.HasSheafCompose.mk 📋 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} (isSheaf : ∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)) : J.HasSheafCompose F
• CategoryTheory.Presheaf.IsSheaf.isSeparated 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {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} {FA : A → A → Type u_1} {CA : A → Type u_2} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [J.HasSheafCompose (CategoryTheory.forget A)] (hF : CategoryTheory.Presheaf.IsSheaf J F) : CategoryTheory.Presheaf.IsSeparated J F
• CategoryTheory.hasSheafCompose_of_preservesMulticospan 📋 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) [∀ (X : C) (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Limits.PreservesLimit (S.index P).multicospan F] : J.HasSheafCompose F
• 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.Sheaf.isSeparated 📋 Mathlib.CategoryTheory.Sites.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C} {FA : A → A → Type u_1} {CA : A → Type u_2} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [J.HasSheafCompose (CategoryTheory.forget A)] (F : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSeparated J F.obj
• 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.sheafifyComposeIso 📋 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) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.sheafify J (P.comp F) ≅ (CategoryTheory.sheafify J P).comp F
• CategoryTheory.sheafComposeIso_hom_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) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.sheafifyComposeIso J F P).hom = CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F
• CategoryTheory.sheafComposeIso_inv_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) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.sheafifyComposeIso J F P).inv = CategoryTheory.toSheafify J (P.comp F)
• CategoryTheory.sheafComposeIso_hom_fac_assoc 📋 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) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : (CategoryTheory.sheafify J P).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) h
• CategoryTheory.sheafComposeIso_inv_fac_assoc 📋 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) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : CategoryTheory.sheafify J (P.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) h
• 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.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.Presheaf.isLocallyInjective_toSheafify' 📋 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} (J : CategoryTheory.GrothendieckTopology C) {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.Sheaf.mono_of_isLocallyInjective 📋 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.Mono φ
• 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.isLocallyInjective_iff_injective 📋 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 φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.hom.app X))
• CategoryTheory.Presheaf.isLocallySurjective_toSheafify' 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] {FD : D → D → Type u_3} {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.Sheaf.epi_of_isLocallySurjective 📋 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.Epi φ
• 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 φ)
• CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_2} {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : J.WEqualsLocallyBijective D
• CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk' 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {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] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [J.HasSheafCompose (CategoryTheory.forget A)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)] : J.WEqualsLocallyBijective A
• CategoryTheory.Sheaf.isLocallyBijective_iff_isIso 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {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 G : CategoryTheory.Sheaf J A} (f : F ⟶ G) [(CategoryTheory.forget A).ReflectsIsomorphisms] [J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f
• CategoryTheory.Equivalence.hasSheafCompose 📋 Mathlib.CategoryTheory.Sites.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2} [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [K.HasSheafCompose F] : J.HasSheafCompose F
• CategoryTheory.hasSheafComposeEssentiallySmallSite 📋 Mathlib.CategoryTheory.Sites.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} A] (B : Type u₄) [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor A B) [CategoryTheory.EssentiallySmall.{w, v₁, u₁} C] [((CategoryTheory.equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F] : J.HasSheafCompose F
• 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.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.JointlyReflectIsomorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : CategoryTheory.JointlyReflectEpimorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyFaithful fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.JointlyReflectMonomorphisms fun Φ => Φ.obj.sheafFiber
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff 📋 Mathlib.CategoryTheory.Sites.Point.Conservative
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [hJ : J.HasSheafCompose (CategoryTheory.forget A)] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)
• CategoryTheory.sheafForget 📋 Mathlib.CategoryTheory.Sites.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {FD : D → D → Type u_2} {CD : D → Type u_3} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [J.HasSheafCompose (CategoryTheory.forget D)] : CategoryTheory.Functor (CategoryTheory.Sheaf J D) (CategoryTheory.Sheaf J (Type u_3))
• 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.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)
• CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X] [CategoryTheory.Limits.PreservesFiniteProducts s] : (CategoryTheory.coherentTopology C).HasSheafCompose s
• CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits 📋 Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] [h : ∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Limits.PreservesFiniteLimits s] : (CategoryTheory.coherentTopology C).HasSheafCompose s
• CategoryTheory.Sheaf.isLocallySurjective_iff_epi' 📋 Mathlib.CategoryTheory.Sites.EpiMono
  {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] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A] [CategoryTheory.HasSheafify J A] [J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Balanced (CategoryTheory.Sheaf J A)] {F G : CategoryTheory.Sheaf J A} (φ : F ⟶ G) : CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ
• CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization 📋 Mathlib.CategoryTheory.Sites.EpiMono
  {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] [J.WEqualsLocallyBijective A] (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A)) [J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.Epi ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).i.app f)
• CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization 📋 Mathlib.CategoryTheory.Sites.EpiMono
  {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] [J.WEqualsLocallyBijective A] (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A)) [J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.Mono ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).p.app f)
• CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] [J.HasEnoughPoints] : J.W.IsMonoidal
• CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W 📋 Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.ObjectProperty J.Point} (hP : P.IsConservativeFamilyOfPoints) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A] {FC : A → A → Type u_1} {CC : A → Type w} [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : A), CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (CategoryTheory.MonoidalCategory.tensorRight X)] [J.HasSheafCompose (CategoryTheory.forget A)] : J.W.IsMonoidal
• Condensed.epi_iff_surjective_on_stonean 📋 Mathlib.Condensed.Epi
  (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [(CategoryTheory.extensiveTopology Stonean).WEqualsLocallyBijective A] [CategoryTheory.HasSheafify (CategoryTheory.extensiveTopology Stonean) A] [(CategoryTheory.extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology Stonean) A)] : CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.compHaus)))
• Condensed.epi_iff_locallySurjective_on_compHaus 📋 Mathlib.Condensed.Epi
  (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y) [(CategoryTheory.coherentTopology CompHaus).WEqualsLocallyBijective A] [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology CompHaus) A] [(CategoryTheory.coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) A)] [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] : CategoryTheory.Epi f ↔ ∀ (S : CompHaus) (y : CategoryTheory.ToType (Y.obj.obj (Opposite.op S))), ∃ S' φ, ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)), ∃ x, (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
• TopCat.Sheaf.isLocallySurjective_iff_epi 📋 Mathlib.Topology.Sheaves.LocallySurjective
  {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Balanced (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C)] [(Opens.grothendieckTopology ↑X).HasSheafCompose (CategoryTheory.forget C)] [CategoryTheory.HasSheafify (Opens.grothendieckTopology ↑X) C] [(Opens.grothendieckTopology ↑X).WEqualsLocallyBijective C] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C] {F G : TopCat.Sheaf C X} (φ : F ⟶ G) : TopCat.Presheaf.IsLocallySurjective φ.hom ↔ CategoryTheory.Epi φ

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