Loogle!

Result

Found 40 declarations mentioning CategoryTheory.GrothendieckTopology.sheafify.

• CategoryTheory.GrothendieckTopology.sheafify 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Functor Cᵒᵖ D
• CategoryTheory.GrothendieckTopology.isoSheafify 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ J.sheafify P
• CategoryTheory.GrothendieckTopology.isIso_toSheafify 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (J.toSheafify P)
• CategoryTheory.GrothendieckTopology.toSheafify 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : P ⟶ J.sheafify P
• CategoryTheory.GrothendieckTopology.sheafification_obj 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafification D).obj P = J.sheafify P
• CategoryTheory.GrothendieckTopology.sheafifyLift 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : J.sheafify P ⟶ Q
• CategoryTheory.GrothendieckTopology.sheafifyMap 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : J.sheafify P ⟶ J.sheafify Q
• CategoryTheory.GrothendieckTopology.isoSheafify_hom 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoSheafify hP).hom = J.toSheafify P
• CategoryTheory.GrothendieckTopology.sheafify_isSheaf 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {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_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf J (J.sheafify P)
• CategoryTheory.GrothendieckTopology.sheafifyMap_id 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D) : J.sheafifyMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.sheafify P)
• CategoryTheory.GrothendieckTopology.isoSheafify_inv 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : (J.isoSheafify hP).inv = J.sheafifyLift (CategoryTheory.CategoryStruct.id P) hP
• CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyLift η hQ) = η
• CategoryTheory.GrothendieckTopology.toSheafify_naturality 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp η (J.toSheafify Q) = CategoryTheory.CategoryStruct.comp (J.toSheafify P) (J.sheafifyMap η)
• CategoryTheory.plusPlusSheaf_obj_obj 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {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_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : ((CategoryTheory.plusPlusSheaf J D).obj P).obj = J.sheafify P
• CategoryTheory.GrothendieckTopology.sheafifyLift_unique 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.sheafify P ⟶ Q) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ = η → γ = J.sheafifyLift η hQ
• CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) : CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyLift γ hR) = J.sheafifyLift (CategoryTheory.CategoryStruct.comp η γ) hR
• CategoryTheory.GrothendieckTopology.sheafifyMap_comp 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : J.sheafifyMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyMap γ)
• CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift_assoc 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift η hQ) h) = CategoryTheory.CategoryStruct.comp η h
• CategoryTheory.GrothendieckTopology.sheafify_hom_ext 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η γ : J.sheafify P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (J.toSheafify P) η = CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ) : η = γ
• CategoryTheory.GrothendieckTopology.toSheafify_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : J.sheafify Q ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (J.toSheafify Q) h) = CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) h)
• CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift_assoc 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (CategoryTheory.CategoryStruct.comp (J.sheafifyLift γ hR) h) = CategoryTheory.CategoryStruct.comp (J.sheafifyLift (CategoryTheory.CategoryStruct.comp η γ) hR) h
• CategoryTheory.plusPlusSheaf_map_hom 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {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_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ D} (η : X✝ ⟶ Y✝) : ((CategoryTheory.plusPlusSheaf J D).map η).hom = J.sheafifyMap η
• CategoryTheory.GrothendieckTopology.sheafifyCompIso 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafify P).comp F ≅ J.sheafify (P.comp F)
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅ ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ D E).obj P).comp (J.sheafification E)
• CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) (J.sheafifyCompIso F P).inv = CategoryTheory.Functor.whiskerRight (J.toSheafify P) F
• CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) (J.sheafifyCompIso F P).hom = J.toSheafify (P.comp F)
• CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) {FD : D → D → Type u_3} {CD : D → Type u_4} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : (J.sheafifyCompIso F P).inv = J.sheafifyLift (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) ⋯
• CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv_assoc 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : (J.sheafify P).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) (CategoryTheory.CategoryStruct.comp (J.sheafifyCompIso F P).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) h
• CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom_assoc 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : J.sheafify (P.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F) (CategoryTheory.CategoryStruct.comp (J.sheafifyCompIso F P).hom h) = CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) h
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] : (J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom
• CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app 📋 Mathlib.CategoryTheory.Sites.CompatibleSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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] (P : CategoryTheory.Functor Cᵒᵖ D) : (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv
• CategoryTheory.plusPlusIsoSheafify 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) : J.sheafify P ≅ CategoryTheory.sheafify J P
• CategoryTheory.toSheafify_plusPlusIsoSheafify_hom 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.plusPlusIsoSheafify J D P).hom = CategoryTheory.toSheafify J P
• CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w) [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.sheafify J P ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.plusPlusIsoSheafify J D P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) h
• 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.Presheaf.isLocallyInjective_toSheafify 📋 Mathlib.CategoryTheory.Sites.LocallyInjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallyInjective J (J.toSheafify P)
• CategoryTheory.Presheaf.isLocallySurjective_toSheafify 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallySurjective J (J.toSheafify P)
• CategoryTheory.Presheaf.sheafificationIsoImagePresheaf 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : J.sheafify F ≅ (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range (J.toSheafify F))).toFunctor

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