Loogle!

Result

Found 74 declarations mentioning CategoryTheory.Sieve.pullback.

• CategoryTheory.Sieve.pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve Y
• CategoryTheory.Sieve.pullback_id 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.id X) S = S
• CategoryTheory.Sieve.pullback_ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (X : I → C) {Y Z : C} (f : Z ⟶ Y) : CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.ofObjects X Y) = CategoryTheory.Sieve.ofObjects X Z
• CategoryTheory.Sieve.pullback_arrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve Y) : (CategoryTheory.Sieve.pullback f S).arrows = CategoryTheory.Presieve.pullback f S.arrows
• CategoryTheory.Sieve.pullbackArrows_comm 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve X) [R.HasPullbacks f] : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pullbackArrows f R) = CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)
• CategoryTheory.Sieve.pullback_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : CategoryTheory.Sieve X) (x✝ : C) (sl : x✝ ⟶ Y) : (CategoryTheory.Sieve.pullback h S).arrows sl = S.arrows (CategoryTheory.CategoryStruct.comp sl h)
• CategoryTheory.Sieve.le_pushforward_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y) : R ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.pushforward f R)
• CategoryTheory.Sieve.pullback_pushforward_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pullback f R) ≤ R
• CategoryTheory.Sieve.pullback_comp 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)
• CategoryTheory.Sieve.pullback_monotone 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : Monotone (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.pullback_ofArrows_of_iso 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Z : I → C) (f : (i : I) → Z i ⟶ X) {X' : C} (e : X' ≅ X) : CategoryTheory.Sieve.pullback e.hom (CategoryTheory.Sieve.ofArrows Z f) = CategoryTheory.Sieve.ofArrows Z fun i => CategoryTheory.CategoryStruct.comp (f i) e.inv
• CategoryTheory.Sieve.galoisConnection 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.galoisCoinsertionOfMono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f] : GaloisCoinsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f] : GaloisInsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.le_pullback_bind 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f) : R h ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.bind S R)
• CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {Y : C} {g : Y ⟶ S} {P : ι → C} {p₁ : (i : ι) → P i ⟶ Y} {p₂ : (i : ι) → P i ⟶ X i} (h : ∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) : CategoryTheory.Sieve.ofArrows P p₁ = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
• CategoryTheory.Sieve.pullback_inter 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback f (S ⊓ R) = CategoryTheory.Sieve.pullback f S ⊓ CategoryTheory.Sieve.pullback f R
• CategoryTheory.Sieve.pullback_eq_top_of_mem 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Sieve X) {f : Y ⟶ X} : S.arrows f → CategoryTheory.Sieve.pullback f S = ⊤
• CategoryTheory.Sieve.mem_iff_pullback_eq_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) : S.arrows f ↔ CategoryTheory.Sieve.pullback f S = ⊤
• CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {X : C} (Z : ι → C) (f : (i : ι) → Z i ⟶ X) (R : (i : ι) → CategoryTheory.Presieve (Z i)) : (CategoryTheory.Sieve.bind (CategoryTheory.Sieve.ofArrows Z f).arrows fun x x_1 hg => CategoryTheory.Sieve.pullback (CategoryTheory.Sieve.ofArrows.h hg) (CategoryTheory.Sieve.generate (R (CategoryTheory.Sieve.ofArrows.i hg)))) ≤ CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows Z f R)
• CategoryTheory.Sieve.pullback_bot 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : CategoryTheory.Sieve.pullback f ⊥ = ⊥
• CategoryTheory.Sieve.pullback_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} : CategoryTheory.Sieve.pullback f ⊤ = ⊤
• CategoryTheory.GrothendieckTopology.covers_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : J.Covers S f ↔ CategoryTheory.Sieve.pullback f S ∈ J Y
• CategoryTheory.GrothendieckTopology.pullback_stable' 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X) : S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y
• CategoryTheory.GrothendieckTopology.pullback_stable 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (hS : S ∈ J X) : CategoryTheory.Sieve.pullback f S ∈ J Y
• CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {i : X ⟶ Y} [CategoryTheory.IsIso i] {S : CategoryTheory.Sieve Y} : CategoryTheory.Sieve.pullback i S ∈ J X ↔ S ∈ J Y
• CategoryTheory.GrothendieckTopology.transitive' 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄ : S ∈ self.sieves X → ∀ (R : CategoryTheory.Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X
• CategoryTheory.GrothendieckTopology.transitive 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (hS : S ∈ J X) (R : CategoryTheory.Sieve X) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ J Y) : R ∈ J X
• CategoryTheory.GrothendieckTopology.mk 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (sieves : (X : C) → Set (CategoryTheory.Sieve X)) (top_mem' : ∀ (X : C), ⊤ ∈ sieves X) (pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y) (transitive' : ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄, S ∈ sieves X → ∀ (R : CategoryTheory.Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X) : CategoryTheory.GrothendieckTopology C
• CategoryTheory.Sieve.functorPullback_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve (F.obj Y)) : CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.pullback (F.map f) S) = CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.functorPullback F S)
• CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback (e.unit.app X) (CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S)) = S
• CategoryTheory.Sieve.functorPushforward_pullback_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.pullback f S) ≤ CategoryTheory.Sieve.pullback (F.map f) (CategoryTheory.Sieve.functorPushforward F S)
• CategoryTheory.Sieve.functorPushforward_functor 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (S : CategoryTheory.Sieve X) (e : C ≌ D) : CategoryTheory.Sieve.functorPushforward e.functor S = CategoryTheory.Sieve.functorPullback e.inverse (CategoryTheory.Sieve.pullback (e.unitInv.app X) S)
• CategoryTheory.Sieve.functorPushforward_inverse 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : D} (S : CategoryTheory.Sieve X) (e : C ≌ D) : CategoryTheory.Sieve.functorPushforward e.inverse S = CategoryTheory.Sieve.functorPullback e.functor (CategoryTheory.Sieve.pullback (e.counit.app X) S)
• CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {U : C} (S : CategoryTheory.Sieve U) : CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S) = CategoryTheory.Sieve.pullback (e.unitInv.app U) S
• CategoryTheory.Presieve.FamilyOfElements.pullback 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.pullback f S).arrows
• CategoryTheory.Presieve.isSheafFor_pullback_iff 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {X : C} (R : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f] : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f R).arrows ↔ CategoryTheory.Presieve.IsSheafFor P R.arrows
• CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (h : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.pullback f x).Compatible
• CategoryTheory.Presieve.isSheafFor_subsieve 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : S.arrows ≤ R) (trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.isSheafFor_subsieve_aux 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : S.arrows ≤ R) (hS : CategoryTheory.Presieve.IsSheafFor P S.arrows) (trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.isSheafFor_trans 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) (R S : CategoryTheory.Sieve X) (hR : CategoryTheory.Presieve.IsSheafFor P R.arrows) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P S.arrows
• CategoryTheory.Presieve.isSheafFor_bind 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) (U : CategoryTheory.Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y) (hU : CategoryTheory.Presieve.IsSheafFor P U.arrows) (hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows) (hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback g (B h)).arrows) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).arrows
• CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B B' : C} (p : B ⟶ B') (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B} (R : CategoryTheory.Sieve X) {X' : CategoryTheory.Over B'} (e : (CategoryTheory.Over.map p).obj X ≅ X') : CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) R.arrows ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback e.inv (CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map p) R)).arrows
• CategoryTheory.Presheaf.pullback_imageSieve 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} 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.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : CategoryTheory.ToType (G.obj (Opposite.op U))) {V : C} (g : V ⟶ U) : CategoryTheory.Sieve.pullback g (CategoryTheory.Presheaf.imageSieve f s) = CategoryTheory.Presheaf.imageSieve f ((CategoryTheory.ConcreteCategory.hom (G.map g.op)) s)
• CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S) [CategoryTheory.LocallySmall.{w, v, u} C] {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)} (hc : CategoryTheory.Limits.IsColimit c) {U : C} (g : U ⟶ S) : CategoryTheory.Presheaf.imageSieve (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i)) (CategoryTheory.shrinkYonedaObjObjEquiv.symm g) = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
• CategoryTheory.Precoverage.Saturate.pullback 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C) (S : CategoryTheory.Sieve X) : J.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), J.Saturate Y (CategoryTheory.Sieve.pullback f S)
• CategoryTheory.Precoverage.Saturate.transitive 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C) (S R : CategoryTheory.Sieve X) : J.Saturate X S → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (CategoryTheory.Sieve.pullback f R)) → J.Saturate X R
• CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_3} [CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.Precoverage C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)).arrows
• CategoryTheory.PreOneHypercover.pullback_sieve₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) {T : C} (f : T ⟶ W) : CategoryTheory.Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (CategoryTheory.CategoryStruct.comp f p₁) (CategoryTheory.CategoryStruct.comp f p₂)
• CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀} [CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (w : CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂)) : E.sieve₁ p₁ p₂ = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
• CategoryTheory.PreOneHypercover.sieve₁_inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C} {p₁ : W ⟶ CategoryTheory.Limits.pullback (E.f i.1) (F.f i.2)} {p₂ : W ⟶ CategoryTheory.Limits.pullback (E.f j.1) (F.f j.2)} (w : CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)) = CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)) (E.f j.1))) : (E.inter F).sieve₁ p₁ p₂ = CategoryTheory.Sieve.bind (E.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2))) (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows fun x f x_1 => CategoryTheory.Sieve.pullback f (F.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.snd (E.f i.1) (F.f i.2))) (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.snd (E.f j.1) (F.f j.2))))
• CategoryTheory.Coverage.Saturate.pullback 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X Y : C} (f : Y ⟶ X) {S : CategoryTheory.Sieve X} (h : K.Saturate X S) : K.Saturate Y (CategoryTheory.Sieve.pullback f S)
• CategoryTheory.Coverage.Saturate.transitive 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} (X : C) (R S : CategoryTheory.Sieve X) : K.Saturate X R → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (CategoryTheory.Sieve.pullback f S)) → K.Saturate X S
• CategoryTheory.Coverage.eq_top_pullback 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.Sieve.pullback f T = ⊤
• CategoryTheory.GrothendieckTopology.isClosed_pullback 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : J₁.IsClosed S → J₁.IsClosed (CategoryTheory.Sieve.pullback f S)
• CategoryTheory.GrothendieckTopology.pullback_close 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : J₁.close (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (J₁.close S)
• CategoryTheory.Functor.sieves_map 📋 Mathlib.CategoryTheory.Sites.Closed
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Functor.sieves C).map f = TypeCat.ofHom fun S => CategoryTheory.Sieve.pullback f.unop S
• CategoryTheory.topologyOfClosureOperator 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) : CategoryTheory.GrothendieckTopology C
• CategoryTheory.topologyOfClosureOperator_close 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) (X : C) (S : CategoryTheory.Sieve X) : (CategoryTheory.topologyOfClosureOperator c pb).close S = (c X) S
• CategoryTheory.topologyOfClosureOperator_sieves 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) (X : C) : (CategoryTheory.topologyOfClosureOperator c hc).sieves X = {S | (c X) S = ⊤}
• CategoryTheory.Sheaf.mem_finestTopology_of_forall_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Canonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type w))} {X : C} {S : CategoryTheory.Sieve X} (H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) : S ∈ (CategoryTheory.Sheaf.finestTopology Ps) X
• CategoryTheory.Functor.mem_inducedTopology_iff 📋 Mathlib.CategoryTheory.Sites.InducedTopology
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C] (X : C) (S : CategoryTheory.Sieve X) (G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₁ u₂ v₂))) (CategoryTheory.Functor Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)))) (adj : G ⊣ (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op) : S ∈ (F.inducedTopology K) X ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (CategoryTheory.Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (CategoryTheory.Sieve.pullback f S)).ι)
• CategoryTheory.Sieve.overEquiv_pullback 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y₁ Y₂ : CategoryTheory.Over X} (f : Y₁ ⟶ Y₂) (S : CategoryTheory.Sieve Y₂) : (CategoryTheory.Sieve.overEquiv Y₁) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback (CategoryTheory.Over.Hom.left f) ((CategoryTheory.Sieve.overEquiv Y₂) S)
• CategoryTheory.Sieve.overEquiv_symm_pullback 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y₁ Y₂ : CategoryTheory.Over X} (f : Y₁ ⟶ Y₂) (S : CategoryTheory.Sieve Y₂.left) : (CategoryTheory.Sieve.overEquiv Y₁).symm (CategoryTheory.Sieve.pullback (CategoryTheory.Over.Hom.left f) S) = CategoryTheory.Sieve.pullback f ((CategoryTheory.Sieve.overEquiv Y₂).symm S)
• CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (h₁ : E.IsStronglySheafFor F) (h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback f E.sieve₀).arrows) {S : CategoryTheory.Sieve X} (H : ∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) S).arrows) (H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) : CategoryTheory.Presieve.IsSheafFor F S.arrows
• CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_of_pullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (h₁ : E.IsStronglySheafFor F) (h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback f E.sieve₀).arrows) {R : CategoryTheory.Presieve X} (H : ∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) (CategoryTheory.Sieve.generate R)).arrows) (H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.Sieve.generate R)).arrows) : CategoryTheory.Presieve.IsSheafFor F R
• CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (E : J.OneHypercover X) {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (hF : CategoryTheory.Presieve.IsSheaf J F) {S : CategoryTheory.Sieve X} (h₁ : ∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) S).arrows) (h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) : CategoryTheory.Presieve.IsSheafFor F S.arrows
• CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (hF : CategoryTheory.Presieve.IsSheaf J F) {R : CategoryTheory.Presieve X} (h₁ : ∀ (i : E.I₀), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Sieve.pullback (E.f i) (CategoryTheory.Sieve.generate R)).arrows) (h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.Sieve.generate R)).arrows) : CategoryTheory.Presieve.IsSheafFor F R
• CategoryTheory.PreOneHypercover.sieve₀_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : (CategoryTheory.PreOneHypercover.cylinder f g).sieve₀ = CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows E.X E.f fun i => (CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
• CategoryTheory.PreOneHypercover.sieve₁'_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).sieve₁' i j = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.map ((CategoryTheory.PreOneHypercover.cylinder f g).f i) ((CategoryTheory.PreOneHypercover.cylinder f g).f j) (E.f i.fst) (E.f j.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (E.sieve₁' i.fst j.fst)
• CategoryTheory.presheafHom_isSheafFor 📋 Mathlib.CategoryTheory.Sites.SheafHom
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] (F G : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)) : CategoryTheory.Presieve.IsSheafFor (CategoryTheory.presheafHom F G) S.arrows
• CategoryTheory.PresheafHom.IsSheafFor.app 📋 Mathlib.CategoryTheory.Sites.SheafHom
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) : F.obj (Opposite.op Y) ⟶ G.obj (Opposite.op Y)
• CategoryTheory.PresheafHom.IsSheafFor.app_cond 📋 Mathlib.CategoryTheory.Sites.SheafHom
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PresheafHom.IsSheafFor.app hG x hx g) (G.map p.op) = CategoryTheory.CategoryStruct.comp (F.map p.op) ((x (CategoryTheory.CategoryStruct.comp p g) hp).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))
• CategoryTheory.PresheafHom.IsSheafFor.exists_app 📋 Mathlib.CategoryTheory.Sites.SheafHom
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X} (hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) {Y : C} (hx : x.Compatible) (g : Y ⟶ X) : ∃ φ, ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)), CategoryTheory.CategoryStruct.comp φ (G.map p.op) = CategoryTheory.CategoryStruct.comp (F.map p.op) ((x (CategoryTheory.CategoryStruct.comp p g) hp).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))

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