Loogle!

Result

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

• CategoryTheory.Sieve 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)
• CategoryTheory.Sieve.instCompleteLattice 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CompleteLattice (CategoryTheory.Sieve X)
• CategoryTheory.Sieve.instNontrivial 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Nontrivial (CategoryTheory.Sieve X)
• CategoryTheory.Sieve.sieveInhabited 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Inhabited (CategoryTheory.Sieve X)
• CategoryTheory.Sieve.ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) (X : C) : CategoryTheory.Sieve X
• 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 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.inf 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (𝒮 : Set (CategoryTheory.Sieve X)) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.sup 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (𝒮 : Set (CategoryTheory.Sieve X)) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.inter 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S R : CategoryTheory.Sieve X) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.union 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S R : CategoryTheory.Sieve X) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.instCoeFunPresieve 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CoeFun (CategoryTheory.Sieve X) fun x => CategoryTheory.Presieve X
• CategoryTheory.Sieve.ofArrows 📋 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) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve Y
• CategoryTheory.Sieve.pushforward 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y) : CategoryTheory.Sieve 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.pullback_id 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.id X) S = S
• CategoryTheory.Sieve.ofTwoArrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {U V X : C} (i : U ⟶ X) (j : V ⟶ X) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.bind 📋 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 X
• 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.BindStruct 📋 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) {Z : C} (h : Z ⟶ X) : Type (max u₁ v₁)
• CategoryTheory.Sieve.ofArrows_eq_ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) {I : Type u_1} (Y : I → C) (f : (i : I) → Y i ⟶ X) : CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.ofObjects Y X
• CategoryTheory.Sieve.pullback_ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (X : I → C) {Y Z : C} (f : Z ⟶ Y) : CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.ofObjects X Y) = CategoryTheory.Sieve.ofObjects X Z
• CategoryTheory.Sieve.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.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.generate_pushforward 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (R : CategoryTheory.Presieve X) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pushforward f R) = CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.generate R)
• 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.mk 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (arrows : CategoryTheory.Presieve X) (downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f)) : CategoryTheory.Sieve X
• 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.exists_eq_ofArrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X) : ∃ I Y f, R = CategoryTheory.Sieve.ofArrows Y f
• CategoryTheory.Sieve.pullbackArrows_comm 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve X) [R.HasPullbacks f] : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pullbackArrows f R) = CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)
• CategoryTheory.Sieve.arrows_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Monotone CategoryTheory.Sieve.arrows
• CategoryTheory.Sieve.generate_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Monotone CategoryTheory.Sieve.generate
• 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_le_ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} (f : (i : I) → Y i ⟶ X) : CategoryTheory.Sieve.ofArrows Y f ≤ CategoryTheory.Sieve.ofObjects Y X
• CategoryTheory.Sieve.le_pushforward_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y) : R ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.pushforward f R)
• CategoryTheory.Sieve.pullback_pushforward_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pullback f R) ≤ R
• CategoryTheory.Sieve.pullback_comp 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)
• CategoryTheory.Sieve.pushforward_comp 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (R : CategoryTheory.Sieve Z) : CategoryTheory.Sieve.pushforward (CategoryTheory.CategoryStruct.comp g f) R = CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pushforward g R)
• CategoryTheory.Sieve.ofObjects_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : I → C} {I' : Type u_2} {X' : I' → C} {Y : C} (h : Set.range X ⊆ Set.range X') : CategoryTheory.Sieve.ofObjects X Y ≤ CategoryTheory.Sieve.ofObjects X' Y
• 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.pullback_monotone 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : Monotone (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.pushforward_monotone 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : Monotone (CategoryTheory.Sieve.pushforward f)
• 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.pullback_ofArrows_of_iso 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Z : I → C) (f : (i : I) → Z i ⟶ X) {X' : C} (e : X' ≅ X) : CategoryTheory.Sieve.pullback e.hom (CategoryTheory.Sieve.ofArrows Z f) = CategoryTheory.Sieve.ofArrows Z fun i => CategoryTheory.CategoryStruct.comp (f i) e.inv
• CategoryTheory.Sieve.galoisConnection 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.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.galoisCoinsertionOfMono 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f] : GaloisCoinsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f] : GaloisInsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Sieve.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.le_pullback_bind 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f) : R h ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.bind S R)
• CategoryTheory.Sieve.pushforward_le_bind_of_mem 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f) : CategoryTheory.Sieve.pushforward f (R h) ≤ CategoryTheory.Sieve.bind S R
• 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_category' 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {S : C} (R : CategoryTheory.Presieve S) : (CategoryTheory.Sieve.ofArrows (fun f => f.obj.left) fun f => f.obj.hom) = CategoryTheory.Sieve.generate R
• CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {Y : C} {g : Y ⟶ S} {P : ι → C} {p₁ : (i : ι) → P i ⟶ Y} {p₂ : (i : ι) → P i ⟶ X i} (h : ∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) : CategoryTheory.Sieve.ofArrows P p₁ = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
• CategoryTheory.Sieve.pullback_inter 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback f (S ⊓ R) = CategoryTheory.Sieve.pullback f S ⊓ CategoryTheory.Sieve.pullback f R
• CategoryTheory.Sieve.pushforward_union 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve Y) : CategoryTheory.Sieve.pushforward f (S ⊔ R) = CategoryTheory.Sieve.pushforward f S ⊔ CategoryTheory.Sieve.pushforward f R
• 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.ofObjects_id 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : CategoryTheory.Sieve.ofObjects id X = ⊤
• 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_ofObjects_eq_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} {i : I} (g : X ⟶ Y i) : CategoryTheory.Sieve.ofObjects Y X = ⊤
• CategoryTheory.Sieve.generate_of_singleton_isSplitEpi 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f] : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = ⊤
• CategoryTheory.Sieve.generate_of_contains_isSplitEpi 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {R : CategoryTheory.Presieve X} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f] (hf : R f) : CategoryTheory.Sieve.generate R = ⊤
• CategoryTheory.Sieve.pullback_eq_top_of_mem 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Sieve X) {f : Y ⟶ X} : S.arrows f → CategoryTheory.Sieve.pullback f S = ⊤
• CategoryTheory.Sieve.mem_iff_pullback_eq_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X) : S.arrows f ↔ CategoryTheory.Sieve.pullback f S = ⊤
• CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {X : C} (Z : ι → C) (f : (i : ι) → Z i ⟶ X) (R : (i : ι) → CategoryTheory.Presieve (Z i)) : (CategoryTheory.Sieve.bind (CategoryTheory.Sieve.ofArrows Z f).arrows fun x x_1 hg => CategoryTheory.Sieve.pullback (CategoryTheory.Sieve.ofArrows.h hg) (CategoryTheory.Sieve.generate (R (CategoryTheory.Sieve.ofArrows.i hg)))) ≤ CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows Z f R)
• CategoryTheory.Sieve.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.generate_bot 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.Sieve.generate ⊥ = ⊥
• CategoryTheory.Sieve.generate_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.Sieve.generate ⊤ = ⊤
• 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.Sieve.generate_eq_bot_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) : CategoryTheory.Sieve.generate R = ⊥ ↔ R = ⊥
• CategoryTheory.Sieve.pullback_bot 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : CategoryTheory.Sieve.pullback f ⊥ = ⊥
• CategoryTheory.Sieve.pullback_top 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} : CategoryTheory.Sieve.pullback f ⊤ = ⊤
• CategoryTheory.Sieve.pushforward_bot 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : CategoryTheory.Sieve.pushforward f ⊥ = ⊥
• CategoryTheory.Sieve.pushforward_eq_bot_iff 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {S : CategoryTheory.Sieve Y} : CategoryTheory.Sieve.pushforward f S = ⊥ ↔ S = ⊥
• CategoryTheory.GrothendieckTopology.sieves 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) (X : C) : Set (CategoryTheory.Sieve X)
• CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  (C : Type u) [CategoryTheory.Category.{v, u} C] : DFunLike (CategoryTheory.GrothendieckTopology C) C fun X => Set (CategoryTheory.Sieve X)
• CategoryTheory.GrothendieckTopology.Cover.instCoeOutSieve 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} : CoeOut (J.Cover X) (CategoryTheory.Sieve X)
• CategoryTheory.GrothendieckTopology.Covers 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : Prop
• CategoryTheory.GrothendieckTopology.copy 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (s : (X : C) → Set (CategoryTheory.Sieve X)) (h : J.sieves = s) : CategoryTheory.GrothendieckTopology C
• CategoryTheory.GrothendieckTopology.copy_eq 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s} : J.copy s h = J
• 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.sieves_copy 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s} : (J.copy s h).sieves = s
• CategoryTheory.GrothendieckTopology.coe_copy 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s} : ⇑(J.copy s h) = s
• CategoryTheory.GrothendieckTopology.ext 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (h : ⇑J₁ = ⇑J₂) : J₁ = J₂
• CategoryTheory.GrothendieckTopology.ext_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C} : J₁ = J₂ ↔ ⇑J₁ = ⇑J₂
• CategoryTheory.GrothendieckTopology.arrow_stable 📋 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) (h : J.Covers S f) {Z : C} (g : Z ⟶ Y) : J.Covers S (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.GrothendieckTopology.covering_iff_covers_id 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) : S ∈ J X ↔ J.Covers S (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.GrothendieckTopology.mem_sieves_iff_coe 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) : S ∈ J.sieves X ↔ S ∈ J X
• 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.covers_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : J.Covers S f ↔ CategoryTheory.Sieve.pullback f S ∈ J Y
• CategoryTheory.GrothendieckTopology.pullback_stable' 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X) : S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y
• CategoryTheory.GrothendieckTopology.le_def 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C} : J₁ ≤ J₂ ↔ ⇑J₁ ≤ ⇑J₂
• 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.arrow_intersect 📋 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) (hS : J.Covers S f) (hR : J.Covers R f) : J.Covers (S ⊓ R) f
• CategoryTheory.GrothendieckTopology.Cover.condition 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : J.Cover X) : ↑S ∈ J X
• CategoryTheory.GrothendieckTopology.top_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
• 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.pullback_stable 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (hS : S ∈ J X) : CategoryTheory.Sieve.pullback f S ∈ J Y
• CategoryTheory.GrothendieckTopology.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.pullback_mem_iff_of_isIso 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {i : X ⟶ Y} [CategoryTheory.IsIso i] {S : CategoryTheory.Sieve Y} : CategoryTheory.Sieve.pullback i S ∈ J X ↔ S ∈ J Y
• CategoryTheory.GrothendieckTopology.mem_sInf 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (s : Set (CategoryTheory.GrothendieckTopology C)) {X : C} (S : CategoryTheory.Sieve X) : S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X
• 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.top_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ ⊤ X
• CategoryTheory.GrothendieckTopology.top_mem' 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) (X : C) : ⊤ ∈ self.sieves X
• CategoryTheory.GrothendieckTopology.superset_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (Hss : S ≤ R) (sjx : S ∈ J X) : R ∈ J X
• CategoryTheory.GrothendieckTopology.top_mem 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : ⊤ ∈ J X
• CategoryTheory.GrothendieckTopology.covering_of_eq_top 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) : S = ⊤ → S ∈ J X
• CategoryTheory.GrothendieckTopology.trivial_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ (CategoryTheory.GrothendieckTopology.trivial C) X ↔ S = ⊤
• 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.intersection_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (rj : R ∈ J X) (sj : S ∈ J X) : R ⊓ S ∈ J X
• CategoryTheory.GrothendieckTopology.intersection_covering_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) : R ⊓ S ∈ J X ↔ R ∈ J X ∧ S ∈ 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.bindOfArrows 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {ι : Type u_1} {X : C} {Z : ι → C} {f : (i : ι) → Z i ⟶ X} {R : (i : ι) → CategoryTheory.Presieve (Z i)} (h : CategoryTheory.Sieve.ofArrows Z f ∈ J X) (hR : ∀ (i : ι), CategoryTheory.Sieve.generate (R i) ∈ J (Z i)) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows Z f R) ∈ J X
• 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.eq_top_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : J = ⊤ ↔ ∀ (X : C), ⊥ ∈ J X
• CategoryTheory.GrothendieckTopology.bot_covering 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ ⊥ X ↔ S = ⊤
• 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.functorPullback_id 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPullback (CategoryTheory.Functor.id C) R = R
• CategoryTheory.Sieve.functorPullback 📋 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 X
• CategoryTheory.Sieve.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) : CategoryTheory.Sieve (F.obj X)
• CategoryTheory.Sieve.functorPushforward_id 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward (CategoryTheory.Functor.id C) R = R
• CategoryTheory.Sieve.functorPullback_functorPushforward_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} {S : CategoryTheory.Sieve X} [F.Full] [F.Faithful] : CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F S) = S
• 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.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) = CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.generate s)
• CategoryTheory.Sieve.le_functorPushforward_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) : R ≤ CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F R)
• 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.Sieve.functorPullback_comp 📋 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} {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve ((F.comp G).obj X)) : CategoryTheory.Sieve.functorPullback (F.comp G) R = CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPullback G R)
• CategoryTheory.Sieve.functorPushforward_comp 📋 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} {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward (F.comp G) R = CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPushforward F R)
• CategoryTheory.Sieve.generate_functorPullback_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Presieve (F.obj X)) : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.functorPullback F R) ≤ CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.generate R)
• CategoryTheory.Sieve.functorPushforward_ofArrows 📋 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} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.ofArrows Y f) = CategoryTheory.Sieve.ofArrows (fun i => F.obj (Y i)) fun i => F.map (f i)
• CategoryTheory.Sieve.functorPullback_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve (F.obj Y)) : CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.pullback (F.map f) S) = CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.functorPullback F S)
• CategoryTheory.Sieve.functorPullback_monotone 📋 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) : Monotone (CategoryTheory.Sieve.functorPullback F)
• CategoryTheory.Sieve.functorPushforward_monotone 📋 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) : Monotone (CategoryTheory.Sieve.functorPushforward F)
• CategoryTheory.Sieve.functorPullback_pushforward_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.functorPullback F R) ≤ R
• CategoryTheory.Sieve.functor_galoisConnection 📋 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) : GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
• CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion 📋 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.EssSurj] [F.Full] (X : C) : GaloisInsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
• CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion 📋 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 : C) : GaloisCoinsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
• CategoryTheory.Sieve.functorPushforward_ofObjects_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {I : Type u_1} (X : I → C) (Y : C) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.ofObjects X Y) ≤ CategoryTheory.Sieve.ofObjects (F.obj ∘ X) (F.obj Y)
• 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.functorPushforward_union 📋 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 R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward F (S ⊔ R) = CategoryTheory.Sieve.functorPushforward F S ⊔ CategoryTheory.Sieve.functorPushforward F R
• CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pullback (e.unit.app X) (CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S)) = S
• CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback 📋 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 X) (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPushforward F S ≤ R ↔ S ≤ CategoryTheory.Sieve.functorPullback F R
• CategoryTheory.Sieve.functorPushforward_pullback_le 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.pullback f S) ≤ CategoryTheory.Sieve.pullback (F.map f) (CategoryTheory.Sieve.functorPushforward F S)
• CategoryTheory.Sieve.functorPullback_inter 📋 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 R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPullback F (S ⊓ R) = CategoryTheory.Sieve.functorPullback F S ⊓ CategoryTheory.Sieve.functorPullback F R
• CategoryTheory.Sieve.functorPullback_union 📋 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 R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPullback F (S ⊔ R) = CategoryTheory.Sieve.functorPullback F S ⊔ CategoryTheory.Sieve.functorPullback F R
• CategoryTheory.Sieve.functorPushforward_functor 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (S : CategoryTheory.Sieve X) (e : C ≌ D) : CategoryTheory.Sieve.functorPushforward e.functor S = CategoryTheory.Sieve.functorPullback e.inverse (CategoryTheory.Sieve.pullback (e.unitInv.app X) S)
• CategoryTheory.Sieve.functorPushforward_inverse 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : D} (S : CategoryTheory.Sieve X) (e : C ≌ D) : CategoryTheory.Sieve.functorPushforward e.inverse S = CategoryTheory.Sieve.functorPullback e.functor (CategoryTheory.Sieve.pullback (e.counit.app X) S)
• CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {U : C} (S : CategoryTheory.Sieve U) : CategoryTheory.Sieve.functorPushforward e.inverse (CategoryTheory.Sieve.functorPushforward e.functor S) = CategoryTheory.Sieve.pullback (e.unitInv.app U) S
• CategoryTheory.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.Sieve.functorPullback_bot 📋 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) : CategoryTheory.Sieve.functorPullback F ⊥ = ⊥
• CategoryTheory.Sieve.functorPullback_top 📋 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) : CategoryTheory.Sieve.functorPullback F ⊤ = ⊤
• CategoryTheory.Sieve.functorPushforward_bot 📋 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) : CategoryTheory.Sieve.functorPushforward F ⊥ = ⊥
• CategoryTheory.Sieve.functorPushforward_top 📋 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) : CategoryTheory.Sieve.functorPushforward F ⊤ = ⊤
• CategoryTheory.GrothendieckTopology.mem_toPretopology 📋 Mathlib.CategoryTheory.Sites.Pretopology
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (t : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Presieve X) : S ∈ t.toPretopology.coverings X ↔ CategoryTheory.Sieve.generate S ∈ t 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 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Functor Cᵒᵖ (Type v₁)
• CategoryTheory.Sieve.uliftFunctor 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))
• CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Sieve.sieveOfSubfunctor S.functorInclusion = S
• CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Sieve.sieveOfUliftSubfunctor S.uliftFunctorInclusion = S
• CategoryTheory.Sieve.functorInclusion_is_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Mono S.functorInclusion
• 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.uliftFunctorInclusion_is_mono 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Mono S.uliftFunctorInclusion
• CategoryTheory.Sieve.functorInclusion 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : S.functor ⟶ CategoryTheory.yoneda.obj X
• CategoryTheory.Sieve.uliftFunctorInclusion 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : S.uliftFunctor ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X
• CategoryTheory.Sieve.sieveOfSubfunctor 📋 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) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.sieveOfUliftSubfunctor 📋 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) : CategoryTheory.Sieve X
• CategoryTheory.Sieve.natTransOfLe 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) : S.functor ⟶ T.functor
• 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.uliftNatTransOfLe 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) : S.uliftFunctor ⟶ T.uliftFunctor
• CategoryTheory.Sieve.natTransOfLe_comm 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.natTransOfLe h) T.functorInclusion = S.functorInclusion
• CategoryTheory.Sieve.uliftNatTransOfLe_comm 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.uliftNatTransOfLe h) T.uliftFunctorInclusion = S.uliftFunctorInclusion
• 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.functorInclusion_top_isIso 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.IsIso ⊤.functorInclusion
• CategoryTheory.Sieve.uliftFunctorInclusion_top_isIso 📋 Mathlib.CategoryTheory.Sites.Sieves.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.IsIso ⊤.uliftFunctorInclusion
• 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 }

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