Loogle!

Result

Found 96 declarations mentioning CategoryTheory.Presieve.IsSheafFor.

• CategoryTheory.Presieve.IsSheafFor 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) (R : CategoryTheory.Presieve X) : Prop
• CategoryTheory.Presieve.isSheafFor_singleton_iso 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.Presieve.IsSheafFor.isSeparatedFor 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSeparatedFor P R
• CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} : CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ CategoryTheory.Presieve.YonedaSheafCondition P S
• CategoryTheory.Presieve.isSheafFor_iff_generate 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.generate R).arrows
• CategoryTheory.Presieve.IsSheafFor.amalgamate 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) (x : CategoryTheory.Presieve.FamilyOfElements P R) (hx : x.Compatible) : P.obj (Opposite.op X)
• CategoryTheory.Presieve.IsSheafFor.isAmalgamation 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) : x.IsAmalgamation (t.amalgamate x hx)
• CategoryTheory.Presieve.isSheafFor_iso 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P') (hP : CategoryTheory.Presieve.IsSheafFor P R) : CategoryTheory.Presieve.IsSheafFor P' R
• CategoryTheory.Presieve.isSheafFor_iff_of_iso 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P') : CategoryTheory.Presieve.IsSheafFor P R ↔ CategoryTheory.Presieve.IsSheafFor P' R
• 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.IsSeparatedFor.isSheafFor 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSeparatedFor P R) : (∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) → CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.IsSheafFor.of_singleton_comp 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y S : C} (p : Y ⟶ X) (f : X ⟶ S) (h : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.comp p f))) (h' : CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Presieve.singleton p)) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton f)
• CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : (CategoryTheory.Presieve.IsSeparatedFor P R ∧ ∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ Function.Bijective (CategoryTheory.Presieve.Arrows.toCompatible P π)
• 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_top 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheafFor P ⊤
• 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.extend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) : CategoryTheory.yoneda.obj X ⟶ P
• 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.of_singleton 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X S : C} {f : X ⟶ S} (hf : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton f)) {R : CategoryTheory.Presieve S} (hf' : R f) (H : ∀ {Y : C} (g : Y ⟶ S), R g → ∃ Z a b, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp b f ∧ CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Presieve.singleton a)) : CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) : CategoryTheory.CategoryStruct.comp S.functorInclusion (h.extend f) = f
• CategoryTheory.Presieve.IsSheafFor.valid_glue 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R) {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f) : (CategoryTheory.ConcreteCategory.hom (P.map f.op)) (t.amalgamate x hx) = x f Hf
• CategoryTheory.Presieve.isSheafFor_arrows_iff 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.Compatible P π x → ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
• CategoryTheory.Presieve.isSheafFor_over_map_op_comp_ofArrows_iff 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {B B' : C} (p : B ⟶ B') (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B} {Y : I → CategoryTheory.Over B} (f : (i : I) → Y i ⟶ X) : CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) (CategoryTheory.Presieve.ofArrows Y f) ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows (fun i => (CategoryTheory.Over.map p).obj (Y i)) fun i => (CategoryTheory.Over.map p).map (f i))
• 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.Presieve.isSheafFor_arrows_iff_pullbacks 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (Opposite.op (X i))), CategoryTheory.Presieve.Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x i
• CategoryTheory.Presieve.IsSheafFor.unique_extend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : S.functor ⟶ P} (t : CategoryTheory.yoneda.obj X ⟶ P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t = f) : t = h.extend f
• CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P) {Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp S.functorInclusion (CategoryTheory.CategoryStruct.comp (h.extend f) h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheafFor F S.arrows ↔ Function.Bijective fun g => CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g
• CategoryTheory.Presieve.IsSheafFor.hom_ext 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (t₁ t₂ : CategoryTheory.yoneda.obj X ⟶ P) (ht : CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ = CategoryTheory.CategoryStruct.comp S.functorInclusion t₂) : t₁ = t₂
• CategoryTheory.Presieve.isSheafFor_singleton 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C} {f : X ⟶ Y} : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton f) ↔ ∀ (x : P.obj (Opposite.op X)), (∀ {Z : C} (p₁ p₂ : Z ⟶ X), CategoryTheory.CategoryStruct.comp p₁ f = CategoryTheory.CategoryStruct.comp p₂ f → (CategoryTheory.ConcreteCategory.hom (P.map p₁.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map p₂.op)) x) → ∃! y, (CategoryTheory.ConcreteCategory.hom (P.map f.op)) y = x
• CategoryTheory.Presieve.isSheafFor_of_nat_equiv 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)), e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) = (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) {X : C} {R : CategoryTheory.Presieve X} (hP₁ : CategoryTheory.Presieve.IsSheafFor P₁ R) : CategoryTheory.Presieve.IsSheafFor P₂ R
• CategoryTheory.Presieve.isSheafFor_iff_of_nat_equiv 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)) (he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)), e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) = (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.IsSheafFor P₁ R ↔ CategoryTheory.Presieve.IsSheafFor P₂ R
• CategoryTheory.Presieve.isSheafFor_comp_uliftFunctor_iff 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.IsSheafFor (P.comp CategoryTheory.uliftFunctor.{w', w}) R ↔ CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.isSheaf_pretopology 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.IsSheaf.isSheafFor 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (hp : CategoryTheory.Presieve.IsSheaf J P) (R : CategoryTheory.Presieve X) (hr : CategoryTheory.Sieve.generate R ∈ J X) : CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) : (∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) ↔ Nonempty (CategoryTheory.Limits.IsColimit S.arrows.cocone)
• CategoryTheory.Equalizer.Presieve.sheaf_condition 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) [R.HasPairwisePullbacks] : CategoryTheory.Presieve.IsSheafFor P R ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P R) ⋯))
• CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))
• CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))
• CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasPullback f f] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (F.map f.op) ⋯))
• CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (F.map f.op) ⋯))
• CategoryTheory.Presheaf.IsSheaf.isSheafFor 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (hP : CategoryTheory.Presheaf.IsSheaf J P) {X : C} (S : CategoryTheory.Sieve X) (hS : S ∈ J X) : CategoryTheory.Presieve.IsSheafFor P S.arrows
• CategoryTheory.Presheaf.isLimit_iff_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.Sieve X) : Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
• CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (R : CategoryTheory.Presieve X) : Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) R
• CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_3} [CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {S : C} {𝒰 𝒱 : CategoryTheory.PreZeroHypercover S} (e : 𝒰 ≅ 𝒱) : CategoryTheory.Presieve.IsSheafFor F 𝒰.presieve₀ ↔ CategoryTheory.Presieve.IsSheafFor F 𝒱.presieve₀
• CategoryTheory.Presieve.IsSheaf.isSheafFor_of_mem_precoverage 📋 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)} (h : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P) {S : C} {R : CategoryTheory.Presieve S} (hR : R ∈ J.coverings S) : CategoryTheory.Presieve.IsSheafFor P 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.Presieve.isSheafFor_ofArrows_comp_iff 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_4} [CategoryTheory.Category.{u_3, u_4} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C} {ι : Type u_2} {Y Z : ι → C} (g : (i : ι) → Z i ⟶ X) (e : (i : ι) → Y i ≅ Z i) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Y fun i => CategoryTheory.CategoryStruct.comp (e i).hom (g i)) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Z g)
• CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_4} [CategoryTheory.Category.{u_3, u_4} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) (P : CategoryTheory.Functor Dᵒᵖ (Type u_2)) {X : C} (R : CategoryTheory.Presieve X) [R.HasPairwisePullbacks] [F.PreservesPairwisePullbacks R] : CategoryTheory.Presieve.IsSheafFor (F.op.comp P) R ↔ CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.map F R)
• CategoryTheory.Presieve.isSheafFor_singleton_iff_of_iso 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_3} [CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {S X Y : C} (f : X ⟶ S) (g : Y ⟶ S) (e : X ≅ Y) (he : CategoryTheory.CategoryStruct.comp e.hom g = f) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton g)
• CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.Small] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), CategoryTheory.Presieve.IsSheafFor P E.presieve₀
• CategoryTheory.Presieve.isSheaf_coverage 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Presieve.isSheafFor_of_factorsThru 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {X : C} {S T : CategoryTheory.Presieve X} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) (H : S.FactorsThru T) (hS : CategoryTheory.Presieve.IsSheafFor P S) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, CategoryTheory.Presieve.IsSeparatedFor P R ∧ R.FactorsThruAlong S f) : CategoryTheory.Presieve.IsSheafFor P T
• CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : S ∈ J X ↔ CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.closedSieves J).toFunctor S.arrows
• 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.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀ 📋 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_3)} (self : E.IsStronglySheafFor F) : CategoryTheory.Presieve.IsSheafFor F E.presieve₀
• CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : Nonempty (CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔ CategoryTheory.Presieve.IsSheafFor F E.presieve₀
• CategoryTheory.PreOneHypercover.IsStronglySheafFor.mk 📋 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_3)} (isSheafFor_presieve₀ : CategoryTheory.Presieve.IsSheafFor F E.presieve₀) (isSeparatedFor_sieve₁ : ∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j), CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) → CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows) : E.IsStronglySheafFor F
• 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.Precoverage.ZeroHypercover.Hom.isSheafFor_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderBaseChange] {S : C} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {𝒰 : K.ZeroHypercover S} {𝒱 : K.ZeroHypercover S} (f : CategoryTheory.Precoverage.ZeroHypercover.Hom K 𝒰 𝒱) (H₁ : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)) (H₂ : ∀ {X : C} (f : X ⟶ S), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Presieve.ofArrows (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).X (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).f)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒱.X 𝒱.f)
• CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff 📋 Mathlib.CategoryTheory.Sites.CoproductSheafCondition
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} {ι : Type u_3} {X : ι → C} (f : (i : ι) → X i ⟶ S) [(CategoryTheory.Presieve.ofArrows X f).HasPairwisePullbacks] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (hc' : CategoryTheory.IsUniversalColimit c) [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)] [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)] (F : CategoryTheory.Functor Cᵒᵖ (Type u_4)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun ij => Opposite.op (CategoryTheory.Limits.pullback (f ij.1) (f ij.2))) F] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X f)
• CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : C) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op I))
• CategoryTheory.Presieve.preservesTerminal_of_isSheaf_for_empty 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty Cᵒᵖ) F
• CategoryTheory.Presieve.isSheafFor_of_preservesProduct 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)
• CategoryTheory.Presieve.preservesProduct_of_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) (hF' : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.isSheafFor_iff_preservesProduct 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔ CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.firstMap_eq_secondMap 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj = CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
• AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff 📋 Mathlib.AlgebraicGeometry.Sites.BigZariski
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u_1)} [AlgebraicGeometry.IsZariskiLocalAtSource P] (hF : CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F) {S : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) [Finite 𝒰.I₀] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)
• AlgebraicGeometry.isSheaf_type_propQCTopology_iff 📋 Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] (F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u_1)) [AlgebraicGeometry.IsZariskiLocalAtSource P] : CategoryTheory.Presieve.IsSheaf (AlgebraicGeometry.Scheme.propQCTopology P) F ↔ CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F ∧ ∀ {R S : CommRingCat} (f : R ⟶ S), P (AlgebraicGeometry.Spec.map f) → AlgebraicGeometry.Surjective (AlgebraicGeometry.Spec.map f) → CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton (AlgebraicGeometry.Spec.map f))
• AlgebraicGeometry.isSheaf_propQCTopology_iff 📋 Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [P.IsMultiplicative] (F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ A) [AlgebraicGeometry.IsZariskiLocalAtSource P] : CategoryTheory.Presheaf.IsSheaf (AlgebraicGeometry.Scheme.propQCTopology P) F ↔ CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F ∧ ∀ {R S : CommRingCat} (f : R ⟶ S), P (AlgebraicGeometry.Spec.map f) → AlgebraicGeometry.Surjective (AlgebraicGeometry.Spec.map f) → ∀ (M : A), CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M))) (CategoryTheory.Presieve.singleton (AlgebraicGeometry.Spec.map f))
• CategoryTheory.Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable 📋 Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {R : CategoryTheory.Presieve X} (hR : R.EffectiveEpimorphic) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) [F.IsRepresentable] : CategoryTheory.Presieve.IsSheafFor F R
• CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda 📋 Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.Presieve X) : R.EffectiveEpimorphic ↔ ∀ (Y : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj Y) R
• CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi 📋 Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f] (F : CategoryTheory.Functor Cᵒᵖ (Type u_1)) [F.IsRepresentable] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f)
• CategoryTheory.Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda 📋 Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) : S.EffectiveEpimorphic ↔ ∀ (Y : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj Y) S.arrows
• CategoryTheory.isSheaf_coherent 📋 Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) P ↔ ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B), CategoryTheory.EffectiveEpiFamily X π → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π)
• CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [S.Extensive] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Presieve.IsSheafFor F S
• CategoryTheory.regularTopology.isSheafFor_regular_of_projective 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X) [S.regular] [CategoryTheory.Projective X] (F : CategoryTheory.Functor Cᵒᵖ (Type u_4)) : CategoryTheory.Presieve.IsSheafFor F S
• CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor' 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S₀ : C} (S : CategoryTheory.Over S₀) {R : CategoryTheory.Sieve S} (hF : F.IsPrestackFor ((CategoryTheory.Sieve.overEquiv S) R).arrows) (M N : ↑(F.obj { as := Opposite.op S₀ })) : CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) R.arrows
• CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor' 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (R : CategoryTheory.Sieve S) : F.IsPrestackFor R.arrows ↔ ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := Opposite.op S₀ })) (a : S ⟶ S₀), CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) ((CategoryTheory.Sieve.overEquiv (CategoryTheory.Over.mk a)).symm R).arrows
• CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (R : CategoryTheory.Sieve S) : F.IsPrestackFor R.arrows ↔ ∀ (M N : ↑(F.obj { as := Opposite.op S })), CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) ((CategoryTheory.Sieve.overEquiv (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S))).symm R).arrows
• CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff 📋 Mathlib.CategoryTheory.Sites.Descent.DescentData
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M N : ↑(F.obj { as := Opposite.op S })) : Function.Bijective (F.toDescentData f).map ↔ CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N) (CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Over.mk (f i)) fun i => CategoryTheory.Over.homMk (f i) ⋯)
• CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.Saturate
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)) : Nonempty (CategoryTheory.Limits.IsLimit (E.saturate.multifork F)) ↔ CategoryTheory.Presieve.IsSheafFor F E.presieve₀
• 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.Precoverage.isSheafFor_subsheafify 📋 Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) {X : C} {R : CategoryTheory.Presieve X} (h : R ∈ K.coverings X) (h' : CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R
• CategoryTheory.Precoverage.small_subsheafify_of_small 📋 Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)) : CategoryTheory.FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor
• CategoryTheory.Precoverage.Generates.isSheaf_of_forall 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (h : K.Generates J) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheaf J F
• CategoryTheory.Precoverage.Generates.isSheaf_of_forall_max 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (self : K.Generates J) (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheaf J F
• CategoryTheory.Precoverage.Generates.isSheaf_type_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (H : K.Generates J) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : CategoryTheory.Presieve.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R
• CategoryTheory.Precoverage.Generates.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (le_toPrecoverage : K ≤ J.toPrecoverage) (isSheaf_of_forall_max : ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) → CategoryTheory.Presieve.IsSheaf J F) : K.Generates J
• CategoryTheory.Precoverage.Generates.isSheaf_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (H : K.Generates J) {F : CategoryTheory.Functor Cᵒᵖ A} : CategoryTheory.Presheaf.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (M : A), CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M))) R

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