Loogle!

Result

Found 268 declarations mentioning CategoryTheory.Sieve.arrows. Of these, only the first 200 are shown.

• CategoryTheory.Sieve.arrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) : CategoryTheory.Presieve X
• CategoryTheory.Sieve.generate_sieve 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.generate S.arrows = S
• CategoryTheory.Sieve.arrows_ext 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} : R.arrows = S.arrows → R = S
• CategoryTheory.Sieve.ofArrows_mk 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) (i : I) : (CategoryTheory.Sieve.ofArrows Y f).arrows (f i)
• CategoryTheory.Sieve.ofArrows.i 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) : I
• CategoryTheory.Sieve.ext 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f) : R = S
• CategoryTheory.Sieve.mem_ofObjects_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {Z X : C} (g : Z ⟶ X) : (CategoryTheory.Sieve.ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)
• CategoryTheory.Sieve.ext_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} : R = S ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f
• 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.pushforward_arrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve X) : (CategoryTheory.Sieve.pushforward f S).arrows = CategoryTheory.Presieve.pushforward f S.arrows
• CategoryTheory.Sieve.le_generate 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) : R ≤ (CategoryTheory.Sieve.generate R).arrows
• CategoryTheory.Sieve.downward_closed 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) {Y Z : C} {f : Y ⟶ X} : self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.Sieve.arrows_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Monotone CategoryTheory.Sieve.arrows
• CategoryTheory.Sieve.pushforward_apply_comp 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {R : CategoryTheory.Sieve Y} {Z : C} {g : Z ⟶ Y} (hg : R.arrows g) (f : Y ⟶ X) : (CategoryTheory.Sieve.pushforward f R).arrows (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.Sieve.comp_mem_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (i : X ⟶ Y) (f : Y ⟶ Z) [CategoryTheory.IsIso i] (S : CategoryTheory.Sieve Z) : S.arrows (CategoryTheory.CategoryStruct.comp i f) ↔ S.arrows f
• CategoryTheory.Sieve.giGenerate 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : GaloisInsertion CategoryTheory.Sieve.generate CategoryTheory.Sieve.arrows
• 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.ofArrows.h 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) : W ⟶ Y (CategoryTheory.Sieve.ofArrows.i hg)
• CategoryTheory.Sieve.bind_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) : (CategoryTheory.Sieve.bind S R).arrows = S.bind fun x x_1 h => (R h).arrows
• CategoryTheory.Sieve.inter_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} {Y : C} (f : Y ⟶ X) : (R ⊓ S).arrows f ↔ R.arrows f ∧ S.arrows f
• CategoryTheory.Sieve.union_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} {Y : C} (f : Y ⟶ X) : (R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f
• CategoryTheory.Sieve.sInf_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C} (f : Y ⟶ X) : (sInf Ss).arrows f ↔ ∀ S ∈ Ss, S.arrows f
• CategoryTheory.Sieve.generate_le_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.generate R ≤ S ↔ R ≤ S.arrows
• CategoryTheory.Sieve.ofArrows.exists 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) : ∃ i h, g = CategoryTheory.CategoryStruct.comp h (f i)
• CategoryTheory.Sieve.mem_ofArrows_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) {W : C} (g : W ⟶ X) : (CategoryTheory.Sieve.ofArrows Y f).arrows g ↔ ∃ i a, g = CategoryTheory.CategoryStruct.comp a (f i)
• CategoryTheory.Sieve.pushforward_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y) (x✝ : C) (gf : x✝ ⟶ X) : (CategoryTheory.Sieve.pushforward f R).arrows gf = ∃ g, CategoryTheory.CategoryStruct.comp g f = gf ∧ R.arrows g
• CategoryTheory.Sieve.ofArrows.fac 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.ofArrows.h hg) (f (CategoryTheory.Sieve.ofArrows.i hg)) = g
• CategoryTheory.Sieve.generate_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) (Z : C) (f : Z ⟶ X) : (CategoryTheory.Sieve.generate R).arrows f = ∃ Y h g, R g ∧ CategoryTheory.CategoryStruct.comp h g = f
• CategoryTheory.Sieve.sSup_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Ss : Set (CategoryTheory.Sieve X)} {Y : C} (f : Y ⟶ X) : (sSup Ss).arrows f ↔ ∃ S, ∃ (_ : S ∈ Ss), S.arrows f
• CategoryTheory.Sieve.top_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : ⊤.arrows f
• CategoryTheory.Sieve.bot_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : ⊥.arrows f ↔ False
• CategoryTheory.Sieve.id_mem_iff_eq_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : S.arrows (CategoryTheory.CategoryStruct.id X) ↔ S = ⊤
• CategoryTheory.Sieve.ofArrows_category 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {S : C} (R : CategoryTheory.Sieve S) : (CategoryTheory.Sieve.ofArrows (fun f => f.obj.left) fun f => f.obj.hom) = 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.Sieve.ofArrows.fac_assoc 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.ofArrows.h hg) (CategoryTheory.CategoryStruct.comp (f (CategoryTheory.Sieve.ofArrows.i hg)) h) = CategoryTheory.CategoryStruct.comp g h
• 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.arrows_bot 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : ⊥.arrows = ⊥
• CategoryTheory.Sieve.arrows_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : ⊤.arrows = ⊤
• CategoryTheory.Sieve.arrows_eq_bot_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : S.arrows = ⊥ ↔ S = ⊥
• CategoryTheory.Sieve.arrows_eq_top_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : S.arrows = ⊤ ↔ S = ⊤
• CategoryTheory.GrothendieckTopology.arrow_max 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.Sieve X) (hf : S.arrows f) : J.Covers S f
• CategoryTheory.GrothendieckTopology.arrow_trans 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S R : CategoryTheory.Sieve X) (h : J.Covers S f) : (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.mk 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (Y : C) (f : Y ⟶ X) (hf : (↑S).arrows f) : S.Arrow
• CategoryTheory.GrothendieckTopology.Cover.Arrow.hf 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (self : S.Arrow) : (↑S).arrows self.f
• CategoryTheory.GrothendieckTopology.dense_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ CategoryTheory.GrothendieckTopology.dense X ↔ ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.GrothendieckTopology.bot_covers 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : ⊥.Covers S f ↔ S.arrows f
• 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.Cover.Arrow.from_middle_condition 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow) : (↑S).arrows I.fromMiddleHom
• CategoryTheory.GrothendieckTopology.Cover.ext 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S T : J.Cover X) (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (↑S).arrows f ↔ (↑T).arrows f) : S = T
• CategoryTheory.GrothendieckTopology.Cover.ext_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S T : J.Cover X} : S = T ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), (↑S).arrows f ↔ (↑T).arrows f
• 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.Cover.coe_pullback 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) (S : J.Cover X) : (↑(S.pullback f)).arrows g ↔ (↑S).arrows (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.GrothendieckTopology.bind_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C) {S : CategoryTheory.Sieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → CategoryTheory.Sieve Y} (hS : S ∈ J X) (hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ J Y) : CategoryTheory.Sieve.bind S.arrows R ∈ J X
• CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow) : (↑(T I.fromMiddle)).arrows I.toMiddleHom
• 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.functorPushforward_extend_eq 📋 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 : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.functorPushforward F (CategoryTheory.Sieve.generate R).arrows = CategoryTheory.Presieve.functorPushforward F R
• CategoryTheory.Presieve.functorPullback_arrows 📋 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 : C} (S : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Presieve.functorPullback F S.arrows = (CategoryTheory.Sieve.functorPullback F S).arrows
• CategoryTheory.Sieve.functorPullback_apply 📋 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 : C} (R : CategoryTheory.Sieve (F.obj X)) : (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows
• CategoryTheory.Sieve.functorPullback_arrows 📋 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 : C} (R : CategoryTheory.Sieve (F.obj X)) : (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows
• CategoryTheory.Sieve.functorPushforward_apply 📋 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 : C} (R : CategoryTheory.Sieve X) : (CategoryTheory.Sieve.functorPushforward F R).arrows = CategoryTheory.Presieve.functorPushforward F R.arrows
• CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward 📋 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 : C} {s : CategoryTheory.Presieve X} : (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.map F s)).arrows = CategoryTheory.Presieve.functorPushforward F s
• CategoryTheory.Sieve.image_mem_functorPushforward 📋 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 : C} (R : CategoryTheory.Sieve X) {V : C} {f : V ⟶ X} (h : R.arrows f) : (CategoryTheory.Sieve.functorPushforward F R).arrows (F.map f)
• CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful 📋 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) [F.Full] [F.Faithful] {X Y : C} (R : CategoryTheory.Sieve X) (f : Y ⟶ X) : CategoryTheory.Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f
• CategoryTheory.Presieve.functorPushforward_overForget 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {S : C} {X : CategoryTheory.Over S} (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve.functorPushforward (CategoryTheory.Over.forget S) R = (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.map (CategoryTheory.Over.forget S) R)).arrows
• CategoryTheory.Sieve.mem_functorPushforward_iff_of_full 📋 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) [F.Full] {X Y : C} (R : CategoryTheory.Sieve X) (f : F.obj Y ⟶ F.obj X) : CategoryTheory.Presieve.functorPushforward F R.arrows f ↔ ∃ g, F.map g = f ∧ R.arrows g
• CategoryTheory.Sieve.mem_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} {Y : D} {S : CategoryTheory.Sieve X} {e : C ≌ D} {f : Y ⟶ e.functor.obj X} : (CategoryTheory.Sieve.functorPushforward e.functor S).arrows f ↔ S.arrows (CategoryTheory.CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))
• CategoryTheory.Sieve.mem_functorPushforward_inverse 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {X : D} {S : CategoryTheory.Sieve X} {e : C ≌ D} {f : Y ⟶ e.inverse.obj X} : (CategoryTheory.Sieve.functorPushforward e.inverse S).arrows f ↔ S.arrows (CategoryTheory.CategoryStruct.comp (e.functor.map f) (e.counit.app X))
• CategoryTheory.Pretopology.mem_toGrothendieck 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) (X : C) (S : CategoryTheory.Sieve X) : S ∈ K.toGrothendieck X ↔ ∃ R ∈ K.coverings X, R ≤ S.arrows
• CategoryTheory.Sieve.functor_obj 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) : S.functor.obj Y = { g // S.arrows g }
• CategoryTheory.Sieve.toFunctor 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.yoneda.obj Y ⟶ S.functor
• CategoryTheory.Sieve.toUliftFunctor 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj Y ⟶ S.uliftFunctor
• CategoryTheory.Sieve.functorInclusion_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (x✝ : Cᵒᵖ) : S.functorInclusion.app x✝ = TypeCat.ofHom fun f => ↑f
• CategoryTheory.Sieve.natTransOfLe_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) (x✝ : Cᵒᵖ) : (CategoryTheory.Sieve.natTransOfLe h).app x✝ = TypeCat.ofHom fun f => ⟨↑f, ⋯⟩
• CategoryTheory.Sieve.uliftNatTransOfLe_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) (x✝ : Cᵒᵖ) : (CategoryTheory.Sieve.uliftNatTransOfLe h).app x✝ = TypeCat.ofHom fun f => { down := ⟨↑f.down, ⋯⟩ }
• CategoryTheory.Sieve.toFunctor_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) : (S.toFunctor f hf).app Z = TypeCat.ofHom fun g => ⟨CategoryTheory.CategoryStruct.comp g f, ⋯⟩
• CategoryTheory.Sieve.uliftFunctorInclusion_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X✝ : Cᵒᵖ) : S.uliftFunctorInclusion.app X✝ = TypeCat.ofHom fun x => { down := ↑x.down }
• CategoryTheory.Sieve.functor_map 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : S.functor.map f = TypeCat.ofHom fun g => ⟨CategoryTheory.CategoryStruct.comp f.unop ↑g, ⋯⟩
• CategoryTheory.Sieve.toUliftFunctor_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) : (S.toUliftFunctor f hf).app Z = TypeCat.ofHom fun g => { down := ⟨CategoryTheory.CategoryStruct.comp g.down f, ⋯⟩ }
• CategoryTheory.Sieve.sieveOfSubfunctor_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : R ⟶ CategoryTheory.yoneda.obj X) (Y : C) (g : Y ⟶ X) : (CategoryTheory.Sieve.sieveOfSubfunctor f).arrows g = ∃ t, (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) t = g
• CategoryTheory.Sieve.sieveOfUliftSubfunctor_apply 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (f : R ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X) (Y : C) (g : Y ⟶ X) : (CategoryTheory.Sieve.sieveOfUliftSubfunctor f).arrows g = ∃ t, (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) t = { down := g }
• CategoryTheory.Sieve.shrinkFunctor_obj 📋 Mathlib.CategoryTheory.Sites.Sieves.Shrink
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).obj Y = {f | S.arrows (CategoryTheory.shrinkYonedaObjObjEquiv f)}
• CategoryTheory.Sieve.shrinkFunctorIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Shrink
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X✝ : Cᵒᵖ) : S.shrinkFunctorIsoFunctor.hom.app X✝ = (CategoryTheory.shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom
• CategoryTheory.Sieve.shrinkFunctorIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Sites.Sieves.Shrink
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X✝ : Cᵒᵖ) : S.shrinkFunctorIsoFunctor.inv.app X✝ = (CategoryTheory.shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.inv
• CategoryTheory.Presieve.FamilyOfElements.SieveCompatible 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : Prop
• 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.FamilyOfElements.sieveExtend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows
• CategoryTheory.Presieve.isSeparatedFor_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.IsSeparatedFor P R ↔ CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.generate R).arrows
• 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.FamilyOfElements.Compatible.to_sieveCompatible 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : x.Compatible) : x.SieveCompatible
• CategoryTheory.Presieve.compatible_iff_sieveCompatible 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) : x.Compatible ↔ x.SieveCompatible
• CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) : x.sieveExtend.Compatible
• 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.isAmalgamation_sieveExtend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (t : P.obj (Opposite.op X)) (ht : x.IsAmalgamation t) : x.sieveExtend.IsAmalgamation t
• CategoryTheory.Presieve.restrict_extend 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} (t : x.Compatible) : CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x.sieveExtend = x
• 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.compatibleEquivGenerateSieveCompatible 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} : { x // x.Compatible } ≃ { x // 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.extend_restrict 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows} (t : x.Compatible) : (CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x).sieveExtend = x
• 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.natTransEquivCompatibleFamily 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : ((CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) ≃ { x // x.Compatible }
• CategoryTheory.Presieve.shrinkFunctorHomEquiv 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : ((CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) ≃ { x // x.Compatible }
• 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.restrict_inj 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} {x₁ x₂ : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows} (t₁ : x₁.Compatible) (t₂ : x₂.Compatible) : CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₁ = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₂ → x₁ = x₂
• 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.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.FamilyOfElements.comp_of_compatible 📋 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) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows} (t : x.Compatible) {f : Y ⟶ X} (hf : S.arrows f) {Z : C} (g : Z ⟶ Y) : x (CategoryTheory.CategoryStruct.comp g f) ⋯ = (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (x f hf)
• 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.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.compatibleEquivGenerateSieveCompatible_apply_coe 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : { x // x.Compatible }) : ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible x) = (↑x).sieveExtend
• CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C} {R : CategoryTheory.Presieve X} (x : { x // x.Compatible }) : ↑(CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible.symm x) = CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ ↑x
• CategoryTheory.Presieve.extension_iff_amalgamation 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (f : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) (g : CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g = f ↔ (↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv f)).IsAmalgamation (CategoryTheory.shrinkYonedaEquiv g)
• CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (f : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) (g : CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).ι g = f ↔ (↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv f)).IsAmalgamation (CategoryTheory.shrinkYonedaEquiv g)
• CategoryTheory.Presieve.shrinkFunctorHomEquiv_symm_apply_app 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (t : { x // x.Compatible }) (X✝ : Cᵒᵖ) : (CategoryTheory.Presieve.shrinkFunctorHomEquiv.symm t).app X✝ = TypeCat.ofHom fun f => ↑t (CategoryTheory.shrinkYonedaObjObjEquiv ↑f) ⋯
• CategoryTheory.Presieve.shrinkFunctorHomEquiv_apply_coe 📋 Mathlib.CategoryTheory.Sites.IsSheafFor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (t : (CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) (Y : C) (f : Y ⟶ X) (hf : S.arrows f) : ↑(CategoryTheory.Presieve.shrinkFunctorHomEquiv t) f hf = (CategoryTheory.ConcreteCategory.hom (t.app (Opposite.op Y))) ⟨CategoryTheory.shrinkYonedaObjObjEquiv.symm f, ⋯⟩
• 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.Presieve.IsSeparated.isSheaf 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (h : CategoryTheory.Presieve.IsSeparated J P) (h' : ∀ (X : C), ∀ S ∈ J X, ∀ (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t) : CategoryTheory.Presieve.IsSheaf J P
• CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X) (s : CategoryTheory.Limits.Cocone S.arrows.diagram) : (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible
• CategoryTheory.Equalizer.Sieve.firstMap 📋 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.Equalizer.FirstObj P S.arrows ⟶ CategoryTheory.Equalizer.Sieve.SecondObj P S
• CategoryTheory.Equalizer.Sieve.secondMap 📋 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.Equalizer.FirstObj P S.arrows ⟶ CategoryTheory.Equalizer.Sieve.SecondObj P S
• CategoryTheory.Equalizer.instInhabitedFirstObjArrowsBotSieve 📋 Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} : Inhabited (CategoryTheory.Equalizer.FirstObj P ⊥.arrows)
• 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.Sieve.w 📋 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.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows) (CategoryTheory.Equalizer.Sieve.firstMap P S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows) (CategoryTheory.Equalizer.Sieve.secondMap P S)
• CategoryTheory.Equalizer.Sieve.compatible_iff 📋 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) (x : CategoryTheory.Equalizer.FirstObj P S.arrows) : CategoryTheory.Presieve.FamilyOfElements.Compatible ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.firstObjEqFamily P S.arrows).hom) x) ↔ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Sieve.firstMap P S)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Sieve.secondMap P S)) x
• CategoryTheory.Equalizer.Sieve.SecondObj.ext 📋 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} (z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂) : z₁ = z₂
• CategoryTheory.Equalizer.Sieve.SecondObj.ext_iff 📋 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} {z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S} : z₁ = z₂ ↔ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
• 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.Presieve.FamilyOfElements.SieveCompatible.cone 📋 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} {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} (hx : x.SieveCompatible) : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)
• CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily 📋 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) (E : Aᵒᵖ) : (S.arrows.diagram.op.comp P).cones.obj E ≃ { x // x.SieveCompatible }
• 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.isSheaf_iff_isLimit 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op))
• 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.Presheaf.isSheaf_iff_isLimit_pretopology 📋 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) [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.Presheaf.IsSheaf K.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
• CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor 📋 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) : (∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
• CategoryTheory.Presheaf.homEquivAmalgamation 📋 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} {E : Aᵒᵖ} {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} (hx : x.SieveCompatible) : (hx.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // x.IsAmalgamation t }
• CategoryTheory.Presheaf.isSeparated_iff_subsingleton 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A) : (∀ (E : A), CategoryTheory.Presieve.IsSeparated J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) ↔ ∀ ⦃X : C⦄, ∀ S ∈ J X, ∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
• CategoryTheory.Meq.congr_apply 📋 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)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) {Y : C} {f g : Y ⟶ X} (h : f = g) (hf : (↑S).arrows f) : ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }
• CategoryTheory.Subfunctor.familyOfElementsOfSection 📋 Mathlib.CategoryTheory.Subfunctor.Sieves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) : CategoryTheory.Presieve.FamilyOfElements G.toFunctor (G.sieveOfSection s).arrows
• CategoryTheory.Subfunctor.family_of_elements_compatible 📋 Mathlib.CategoryTheory.Subfunctor.Sieves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) : (G.familyOfElementsOfSection s).Compatible
• CategoryTheory.Subfunctor.sieveOfSection_apply 📋 Mathlib.CategoryTheory.Subfunctor.Sieves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V ⟶ Opposite.unop U) : (G.sieveOfSection s).arrows f = ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) s ∈ G.obj (Opposite.op V))
• CategoryTheory.Presheaf.equalizerSieve_apply 📋 Mathlib.CategoryTheory.Sites.LocallyInjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {FD : D → D → Type u_1} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : CategoryTheory.ToType (F.obj X)) (x✝ : C) (f : x✝ ⟶ Opposite.unop X) : (CategoryTheory.Presheaf.equalizerSieve x y).arrows f = ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) y)
• CategoryTheory.Presieve.FamilyOfElements.localPreimage 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} (φ : R ⟶ R') {X : Cᵒᵖ} (r' : R'.obj X) : CategoryTheory.Presieve.FamilyOfElements R (CategoryTheory.Presheaf.imageSieve φ r').arrows
• CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} (φ : R ⟶ R') {X : Cᵒᵖ} (r' : R'.obj X) : ((CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r').map φ).IsAmalgamation r'
• CategoryTheory.Presheaf.localPreimage 📋 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 U)) {V : C} (g : V ⟶ Opposite.unop U) (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g) : CategoryTheory.ToType (F.obj (Opposite.op V))
• CategoryTheory.Presheaf.app_localPreimage 📋 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 U)) {V : C} (g : V ⟶ Opposite.unop U) (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g) : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) (CategoryTheory.Presheaf.localPreimage f s g hg) = (CategoryTheory.ConcreteCategory.hom (G.map g.op)) s
• CategoryTheory.Presheaf.imageSieve_apply 📋 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) (i : V ⟶ U) : (CategoryTheory.Presheaf.imageSieve f s).arrows i = ∃ t, (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op V))) t = (CategoryTheory.ConcreteCategory.hom (G.map i.op)) s
• PresheafOfModules.Sheafify.SMulCandidate.mk' 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj) [CategoryTheory.Presheaf.IsLocallyInjective J φ] {X : Cᵒᵖ} (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)) (S : CategoryTheory.Sieve (Opposite.unop X)) (hS : S ∈ J (Opposite.unop X)) (r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat)) S.arrows) (m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf.comp (CategoryTheory.forget Ab)) S.arrows) (hr₀ : (r₀.map (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r) (hm₀ : (m₀.map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation m) (a : ↑(A.obj.obj X)) (ha : ((r₀.smul m₀).map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation a) : PresheafOfModules.Sheafify.SMulCandidate α φ r m
• CategoryTheory.PreZeroHypercover.sieve₀_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀) : E.sieve₀.arrows (E.f i)
• 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.GrothendieckTopology.arrows_mem_toPrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_3} [CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C) {S : C} (R : CategoryTheory.Sieve S) : R.arrows ∈ J.toPrecoverage.coverings S ↔ R ∈ J S
• 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.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.HasIsos] {X : C} {S : CategoryTheory.Sieve X} : S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows
• CategoryTheory.PreOneHypercover.sieve₁_apply 📋 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₂) (Z : C) (g : Z ⟶ W) : (E.sieve₁ p₁ p₂).arrows g = ∃ j h, CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (E.p₁ j) ∧ CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (E.p₂ j)
• 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.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.hom_ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (H : J.OneHypercoverFamily) (P : CategoryTheory.Functor Cᵒᵖ A) (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) [H.IsGenerating] {X : C} (S : CategoryTheory.Sieve X) (hS : S ∈ J X) {T : A} {x y : T ⟶ P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → CategoryTheory.CategoryStruct.comp x (P.map f.op) = CategoryTheory.CategoryStruct.comp y (P.map f.op)) : x = y
• CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) [H.IsGenerating] {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map f.op) = F.ι { Y := Y, f := f, hf := hf }
• 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.Presieve.le_of_factorsThru_sieve 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X) (T : CategoryTheory.Sieve X) (h : S.FactorsThru T.arrows) : S ≤ T.arrows
• CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X : C} {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X} (h : R ≤ S.arrows) (hR : R ∈ K.coverings X) : S ∈ K.toGrothendieck X
• 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.Presheaf.isSheaf_iff_isLimit_coverage 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf K.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
• CategoryTheory.GrothendieckTopology.close_apply 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) (x✝ : C) (f : x✝ ⟶ X) : (J₁.close S).arrows f = J₁.Covers S f
• CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} {S : CategoryTheory.Sieve X} (h : J₁.IsClosed S) {Y : C} (f : Y ⟶ X) : J₁.Covers S f ↔ S.arrows f
• 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.Sieve.equalizer_apply 📋 Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
  {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U V : C} (f₁ f₂ : U ⟶ V) (x✝ : C) (i : x✝ ⟶ U) : (CategoryTheory.Sieve.equalizer f₁ f₂).arrows i = (CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂)
• CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] (ℱ : CategoryTheory.Sheaf K A) {X : A} {U : D} {T : CategoryTheory.Sieve U} (hT : T ∈ K U) (x : CategoryTheory.Presieve.FamilyOfElements (ℱ.obj.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows) (hx : x.Compatible) (t : (ℱ.obj.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)) (h : x.IsAmalgamation t) : t = ⋯.amalgamate x hx
• CategoryTheory.Functor.IsCoverDense.Types.presheafIso_hom_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : Dᵒᵖ) (x : ℱ.obj.obj (Opposite.op (Opposite.unop X))) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).hom.app X)) x = ⋯.amalgamate (fun x_1 x_2 hf => (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).lift.op)) ((CategoryTheory.ConcreteCategory.hom (i.hom.app (Opposite.op (Nonempty.some hf).1))) ((CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (Nonempty.some hf).map.op)) x))) ⋯
• CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app_hom_apply 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} [G.IsCoverDense K] [G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : Dᵒᵖ) (x : ℱ'.obj.obj (Opposite.op (Opposite.unop X))) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).inv.app X)) x = ⋯.amalgamate (fun x_1 x_2 hf => (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (Nonempty.some hf).lift.op)) ((CategoryTheory.ConcreteCategory.hom (i.inv.app (Opposite.op (Nonempty.some hf).1))) ((CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).map.op)) x))) ⋯
• 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.Sieve.functorPushforward_overForget_arrows 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y) : CategoryTheory.Presieve.functorPushforward (CategoryTheory.Over.forget X) S.arrows = CategoryTheory.Presieve.map (CategoryTheory.Over.forget X) S.arrows
• CategoryTheory.Sieve.overEquiv_iff 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y) {Z : C} (f : Z ⟶ Y.left) : ((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)
• CategoryTheory.Sieve.overEquiv_symm_iff 📋 Mathlib.CategoryTheory.Sites.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y.left) {Z : CategoryTheory.Over X} (f : Z ⟶ Y) : ((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f ↔ S.arrows (CategoryTheory.Over.Hom.left f)
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} (x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y) (X : C) : CategoryTheory.Presieve.FamilyOfElements F (CategoryTheory.Sieve.ofObjects Y X).arrows
• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (X : C) : (x.familyOfElements X).Compatible
• Opens.mem_grothendieckTopology 📋 Mathlib.CategoryTheory.Sites.Spaces
  (T : Type u) [TopologicalSpace T] {U : TopologicalSpace.Opens T} {S : CategoryTheory.Sieve U} : S ∈ (Opens.grothendieckTopology T) U ↔ ∀ x ∈ U, ∃ V f, S.arrows f ∧ x ∈ V
• TopCat.Presheaf.generateEquivalenceOpensLe_functor' 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} : CategoryTheory.Functor (CategoryTheory.ObjectProperty.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom) (TopCat.Presheaf.SheafCondition.OpensLeCover U)
• TopCat.Presheaf.generateEquivalenceOpensLe 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (CategoryTheory.ObjectProperty.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom) ≌ TopCat.Presheaf.SheafCondition.OpensLeCover U
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse' 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : CategoryTheory.Functor (TopCat.Presheaf.SheafCondition.OpensLeCover U) (CategoryTheory.ObjectProperty.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom)
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) (V : TopCat.Presheaf.SheafCondition.OpensLeCover U) : ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.right.as = PUnit.unit
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) (V : TopCat.Presheaf.SheafCondition.OpensLeCover U) : ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.left = V.obj
• TopCat.Presheaf.generateEquivalenceOpensLe_functor 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (TopCat.Presheaf.generateEquivalenceOpensLe U hY).functor = TopCat.Presheaf.generateEquivalenceOpensLe_functor' U
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (TopCat.Presheaf.generateEquivalenceOpensLe U hY).inverse = TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY
• TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (f : CategoryTheory.ObjectProperty.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom) : ((TopCat.Presheaf.generateEquivalenceOpensLe_functor' U).obj f).obj = f.obj.left
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) (V : TopCat.Presheaf.SheafCondition.OpensLeCover U) : ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.hom = CategoryTheory.homOfLE ⋯
• TopCat.Presheaf.generateEquivalenceOpensLe_counitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (TopCat.Presheaf.generateEquivalenceOpensLe U hY).counitIso = CategoryTheory.eqToIso ⋯
• TopCat.Presheaf.isLimitOpensLeEquivGenerate₁ 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows.cocone.op)
• TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} {X✝ Y✝ : CategoryTheory.ObjectProperty.FullSubcategory fun f => (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom} (g : X✝ ⟶ Y✝) : (TopCat.Presheaf.generateEquivalenceOpensLe_functor' U).map g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.Hom.left g.hom)
• TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) {X✝ Y✝ : TopCat.Presheaf.SheafCondition.OpensLeCover U} (g : X✝ ⟶ Y✝) : (TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).map g = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk g.hom ⋯)
• TopCat.Presheaf.generateEquivalenceOpensLe_unitIso 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (TopCat.Presheaf.generateEquivalenceOpensLe U hY).unitIso = CategoryTheory.eqToIso ⋯
• TopCat.Presheaf.isLimitOpensLeEquivGenerate₂ 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {Y : TopologicalSpace.Opens ↑X} (R : CategoryTheory.Presieve Y) (hR : CategoryTheory.Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone (TopCat.Presheaf.coveringOfPresieve Y R)).op) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Sieve.generate R).arrows.cocone.op)
• TopCat.Presheaf.whiskerIsoMapGenerateCocone 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : CategoryTheory.Limits.Cone.whisker (TopCat.Presheaf.generateEquivalenceOpensLe U hY).op.functor (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≅ CategoryTheory.Functor.mapCone F (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows.cocone.op
• TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (F.whiskerIsoMapGenerateCocone U hY).hom.hom = F.map (CategoryTheory.eqToHom ⋯)
• TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom 📋 Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U) : (F.whiskerIsoMapGenerateCocone U hY).inv.hom = F.map (CategoryTheory.eqToHom ⋯)
• AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology 📋 Mathlib.AlgebraicGeometry.Sites.Pretopology
  {X : AlgebraicGeometry.Scheme} {s : CategoryTheory.Sieve X} : s ∈ AlgebraicGeometry.Scheme.jointlySurjectiveTopology X ↔ s.arrows ∈ AlgebraicGeometry.Scheme.jointlySurjectivePretopology.coverings X
• AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology 📋 Mathlib.AlgebraicGeometry.Sites.Pretopology
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.Sieve X} : S ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X → ∃ 𝒰, CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

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