Loogle!

Result

Found 144 declarations mentioning CategoryTheory.Precoverage.coverings.

• CategoryTheory.Precoverage.coverings 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Precoverage C) (X : C) : Set (CategoryTheory.Presieve X)
• CategoryTheory.Precoverage.ext 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Precoverage C} (coverings : x.coverings = y.coverings) : x = y
• CategoryTheory.Precoverage.ext_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Precoverage C} : x = y ↔ x.coverings = y.coverings
• CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) [J.HasPullbacks] {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ J.coverings X) : R.HasPairwisePullbacks
• CategoryTheory.Precoverage.hasPullbacks_of_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasPullbacks] {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y) (hR : R ∈ J.coverings Y) : R.HasPullbacks f
• CategoryTheory.Precoverage.mem_coverings_of_isIso 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasIsos] {S T : C} (f : S ⟶ T) [CategoryTheory.IsIso f] : CategoryTheory.Presieve.singleton f ∈ J.coverings T
• CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasIsos] {S T : C} (f : S ⟶ T) [CategoryTheory.IsIso f] : CategoryTheory.Presieve.singleton f ∈ J.coverings T
• CategoryTheory.Precoverage.HasIsos.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (mem_coverings_of_isIso : ∀ {S T : C} (f : S ⟶ T) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ J.coverings T) : J.HasIsos
• CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasPullbacks] {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y) (hR : R ∈ J.coverings Y) : R.HasPullbacks f
• CategoryTheory.Precoverage.HasPullbacks.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (hasPullbacks_of_mem : ∀ {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y), R ∈ J.coverings Y → R.HasPullbacks f) : J.HasPullbacks
• CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D} [self : J.PullbacksPreservedBy F] ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄ : R ∈ J.coverings X → F.PreservesPairwisePullbacks R
• CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D} [self : J.PullbacksPreservedBy F] ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄ : R ∈ J.coverings X → F.PreservesPairwisePullbacks R
• CategoryTheory.Precoverage.PullbacksPreservedBy.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor C D} (preservesPairwisePullbacks_of_mem : ∀ ⦃X : C⦄ ⦃R : CategoryTheory.Presieve X⦄, R ∈ J.coverings X → F.PreservesPairwisePullbacks R := by infer_instance) : J.PullbacksPreservedBy F
• CategoryTheory.Precoverage.pullbackArrows_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X Y : C} (f : X ⟶ Y) {R : CategoryTheory.Presieve Y} (hR : R ∈ J.coverings Y) [R.HasPullbacks f] : CategoryTheory.Presieve.pullbackArrows f R ∈ J.coverings X
• CategoryTheory.Precoverage.mem_comap_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D} {X : C} {R : CategoryTheory.Presieve X} : R ∈ (CategoryTheory.Precoverage.comap F J).coverings X ↔ CategoryTheory.Presieve.map F R ∈ J.coverings (F.obj X)
• CategoryTheory.Precoverage.sup_mem_coverings 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderSup] {X : C} {R S : CategoryTheory.Presieve X} (hR : R ∈ J.coverings X) (hS : S ∈ J.coverings X) : R ⊔ S ∈ J.coverings X
• CategoryTheory.Precoverage.IsStableUnderSup.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (sup_mem_coverings : ∀ {X : C} {R S : CategoryTheory.Presieve X}, R ∈ J.coverings X → S ∈ J.coverings X → R ⊔ S ∈ J.coverings X) : J.IsStableUnderSup
• CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderSup] {X : C} {R S : CategoryTheory.Presieve X} (hR : R ∈ J.coverings X) (hS : S ∈ J.coverings X) : R ⊔ S ∈ J.coverings X
• CategoryTheory.Precoverage.mem_coverings_of_isPullback 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hR : CategoryTheory.Presieve.ofArrows X f ∈ J.coverings 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.Presieve.ofArrows P p₁ ∈ J.coverings Y
• CategoryTheory.Precoverage.IsStableUnderBaseChange.mem_coverings_of_isPullback 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderBaseChange] {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hR : CategoryTheory.Presieve.ofArrows X f ∈ J.coverings 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.Presieve.ofArrows P p₁ ∈ J.coverings Y
• CategoryTheory.Precoverage.IsStableUnderBaseChange.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (mem_coverings_of_isPullback : ∀ {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S), CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S → ∀ {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i), (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) → CategoryTheory.Presieve.ofArrows P p₁ ∈ J.coverings Y) : J.IsStableUnderBaseChange
• CategoryTheory.Precoverage.comp_mem_coverings 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hf : CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S) {σ : ι → Type w'} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) (hg : ∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) : (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x => CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈ J.coverings S
• CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderComposition] {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hf : CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S) {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) (hg : ∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) : (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x => CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈ J.coverings S
• CategoryTheory.Precoverage.IsStableUnderComposition.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (comp_mem_coverings : ∀ {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S), CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S → ∀ {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i), (∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) → (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x => CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈ J.coverings S) : J.IsStableUnderComposition
• CategoryTheory.Pretopology.ext 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasPullbacks C} {x y : CategoryTheory.Pretopology C} (coverings : x.coverings = y.coverings) : x = y
• CategoryTheory.Pretopology.ext_iff 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasPullbacks C} {x y : CategoryTheory.Pretopology C} : x = y ↔ x.coverings = y.coverings
• CategoryTheory.Pretopology.has_isos 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (self : CategoryTheory.Pretopology C) ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f] : CategoryTheory.Presieve.singleton f ∈ self.coverings X
• CategoryTheory.Pretopology.le_def 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {K₁ K₂ : CategoryTheory.Pretopology C} : K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings
• 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.pullbacks 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (self : CategoryTheory.Pretopology C) ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Presieve X) : S ∈ self.coverings X → CategoryTheory.Presieve.pullbackArrows f S ∈ self.coverings Y
• CategoryTheory.Pretopology.mem_sInf 📋 Mathlib.CategoryTheory.Sites.Pretopology
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (T : Set (CategoryTheory.Pretopology C)) {X : C} (S : CategoryTheory.Presieve X) : S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X
• CategoryTheory.Pretopology.mem_inf 📋 Mathlib.CategoryTheory.Sites.Pretopology
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (t₁ t₂ : CategoryTheory.Pretopology C) {X : C} (S : CategoryTheory.Presieve X) : S ∈ (t₁ ⊓ t₂).coverings X ↔ S ∈ t₁.coverings X ∧ S ∈ t₂.coverings X
• CategoryTheory.Pretopology.transitive 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (self : CategoryTheory.Pretopology C) ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y) : S ∈ self.coverings X → (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ self.coverings Y) → S.bind Ti ∈ self.coverings 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.Pretopology.mk 📋 Mathlib.CategoryTheory.Sites.Pretopology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (toPrecoverage : CategoryTheory.Precoverage C) (has_isos : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X) (pullbacks : ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y) (transitive : ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y), S ∈ toPrecoverage.coverings X → (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) → S.bind Ti ∈ toPrecoverage.coverings X) : CategoryTheory.Pretopology C
• CategoryTheory.Presieve.isSheaf_pretopology 📋 Mathlib.CategoryTheory.Sites.SheafOfTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.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.Precoverage.ZeroHypercover.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) (mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S) : J.ZeroHypercover S
• CategoryTheory.Precoverage.ZeroHypercover.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (self : J.ZeroHypercover S) : self.presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.ZeroHypercover.singleton 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f : S ⟶ T) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T) : J.ZeroHypercover T
• CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {E : J.ZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (e : E.toPreZeroHypercover ≅ F) : F.presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.ZeroHypercover.pushforward 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X) : J.ZeroHypercover Y
• CategoryTheory.Precoverage.le_of_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C} (h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X) : J ≤ K
• CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : (E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)).presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f : S ⟶ T) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T) : (CategoryTheory.Precoverage.ZeroHypercover.singleton f hf).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.singleton f
• CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) (hE : E.presieve₀ ∈ J.coverings S) : F.presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.RespectsIso.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (of_iso : ∀ {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F), E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S) : J.RespectsIso
• CategoryTheory.Precoverage.RespectsIso.of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.RespectsIso] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) : E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [self : E.Small] : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S
• CategoryTheory.Precoverage.ZeroHypercover.Small.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E : J.ZeroHypercover S} (exists_restrictIndex_mem : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S) : E.Small
• CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F) : E.presieve₀ ∈ J.coverings S ↔ F.presieve₀ ∈ J.coverings S
• CategoryTheory.PreZeroHypercover.mem_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderComposition] [K.HasIsos] {X : C} {E F : CategoryTheory.PreZeroHypercover X} (e : E ≅ F) (hE : E.presieve₀ ∈ K.coverings X) : F.presieve₀ ∈ K.coverings X
• CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {X : C} {R : CategoryTheory.Presieve X} : R ∈ J.coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
• CategoryTheory.PreZeroHypercover.mem_iff_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderComposition] [K.HasIsos] {X : C} {E F : CategoryTheory.PreZeroHypercover X} (e : E ≅ F) : E.presieve₀ ∈ K.coverings X ↔ F.presieve₀ ∈ K.coverings X
• CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X) : (CategoryTheory.Precoverage.ZeroHypercover.pushforward f hf E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pushforward f E.toPreZeroHypercover
• CategoryTheory.Precoverage.ZeroHypercover.add 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : J.ZeroHypercover S
• CategoryTheory.Precoverage.Small.inf 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C} [J.Small] (of_le : ∀ ⦃X : C⦄ ⦃R S : CategoryTheory.Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X) : (J ⊓ K).Small
• CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : (E.add f hf).toPreZeroHypercover = E.add f
• CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {R T : CategoryTheory.Presieve S} (hRT : ∀ ⦃Z : C⦄ (g : Z ⟶ S), R g → ∃ Y e, T (CategoryTheory.CategoryStruct.comp e.hom g)) (hTR : ∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ Y e, R (CategoryTheory.CategoryStruct.comp e.hom g)) (hR : R ∈ J.coverings S) : T ∈ J.coverings S
• CategoryTheory.Precoverage.Saturate.of 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C) (S : CategoryTheory.Presieve X) (hS : S ∈ J.coverings X) : J.Saturate X (CategoryTheory.Sieve.generate S)
• CategoryTheory.Presieve.IsSheaf.isSheafFor_of_mem_precoverage 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_3} [CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.Precoverage C} {P : CategoryTheory.Functor Cᵒᵖ (Type u_1)} (h : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P) {S : C} {R : CategoryTheory.Presieve S} (hR : R ∈ J.coverings S) : CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Precoverage.generate_mem_toGrothendieck 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Precoverage C} {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ J.coverings X) : CategoryTheory.Sieve.generate R ∈ J.toGrothendieck X
• 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.GrothendieckTopology.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.Presieve S) : R ∈ J.toPrecoverage.coverings S ↔ CategoryTheory.Sieve.generate 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.toGrothendieck_eq_sInf 📋 Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
  {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] (J : CategoryTheory.Precoverage C) : J.toGrothendieck = sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, CategoryTheory.Sieve.generate S ∈ K X}
• 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.Coverage.ext 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Coverage C} (coverings : x.coverings = y.coverings) : x = y
• CategoryTheory.Coverage.ext_iff 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Coverage C} : x = y ↔ x.coverings = y.coverings
• CategoryTheory.Coverage.Saturate.of 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} (X : C) (S : CategoryTheory.Presieve X) (hS : S ∈ K.coverings X) : K.Saturate X (CategoryTheory.Sieve.generate S)
• CategoryTheory.Presieve.isSheaf_coverage 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] (K : CategoryTheory.Coverage C) (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Coverage.sup_covering 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (x y : CategoryTheory.Coverage C) (B : C) : (x ⊔ y).coverings B = x.coverings B ∪ y.coverings B
• CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, CategoryTheory.Presieve.IsSheafFor P R
• CategoryTheory.Pretopology.mem_toCoverage 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (J : CategoryTheory.Pretopology C) {X : C} (S : CategoryTheory.Presieve X) : S ∈ J.toCoverage.coverings X ↔ S ∈ J.coverings X
• CategoryTheory.GrothendieckTopology.mem_toCoverage_iff 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} {S : CategoryTheory.Presieve X} (J : CategoryTheory.GrothendieckTopology C) : S ∈ J.toCoverage.coverings X ↔ CategoryTheory.Sieve.generate S ∈ J X
• CategoryTheory.Coverage.mk 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (toPrecoverage : CategoryTheory.Precoverage C) (pullback : ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f) : CategoryTheory.Coverage C
• CategoryTheory.Coverage.pullback 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Coverage C) ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Presieve X) : S ∈ self.coverings X → ∃ T ∈ self.coverings Y, T.FactorsThruAlong S f
• CategoryTheory.Precoverage.toCoverage_le_toCoverage 📋 Mathlib.CategoryTheory.Sites.Coverage
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] (K : CategoryTheory.GrothendieckTopology C) : (J.toCoverage ≤ K.toCoverage) = ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, CategoryTheory.Sieve.generate S ∈ K X
• 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.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.Precoverage.locallyCoverDense_of_map_functorPullback_mem 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
  {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] (H : ∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) : F.LocallyCoverDense K.toGrothendieck
• CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
  {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [F.Faithful] [F.Full] (H : ∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) : (CategoryTheory.Precoverage.comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck
• CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
  {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [F.Faithful] [F.Full] (H : ∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) : (CategoryTheory.Precoverage.comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck
• CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.JointlySurjective
  {X Y : Type u} {f : X ⟶ Y} : CategoryTheory.Presieve.singleton f ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings Y ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
• CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.JointlySurjective
  {X : Type u} {R : CategoryTheory.Presieve X} : R ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings X ↔ ∀ (x : X), ∃ Y g, R g ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
• CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.JointlySurjective
  {X : Type u} {ι : Type u_1} {Y : ι → Type u} {f : (i : ι) → Y i ⟶ X} : CategoryTheory.Presieve.ofArrows Y f ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings X ↔ ∀ (x : (fun X => X) X), ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f i))
• CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.JointlySurjective
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C (Type u)) {X : C} {R : CategoryTheory.Presieve X} : R ∈ (CategoryTheory.Precoverage.comap F CategoryTheory.Types.jointlySurjectivePrecoverage).coverings X ↔ ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
• CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff 📋 Mathlib.CategoryTheory.Sites.JointlySurjective
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C (Type u)) {X : C} {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} : CategoryTheory.Presieve.ofArrows Y f ∈ (CategoryTheory.Precoverage.comap F CategoryTheory.Types.jointlySurjectivePrecoverage).coverings X ↔ ∀ (x : F.obj X), ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (f i)))
• CategoryTheory.MorphismProperty.singleton_mem_precoverage 📋 Mathlib.CategoryTheory.Sites.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y) : CategoryTheory.Presieve.singleton f ∈ P.precoverage.coverings Y ↔ P f
• CategoryTheory.MorphismProperty.ofArrows_mem_precoverage 📋 Mathlib.CategoryTheory.Sites.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {X : C} {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} : CategoryTheory.Presieve.ofArrows Y f ∈ P.precoverage.coverings X ↔ ∀ (i : ι), P (f i)
• CategoryTheory.MorphismProperty.bot_mem_precoverage 📋 Mathlib.CategoryTheory.Sites.MorphismProperty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} (X : C) : ⊥ ∈ P.precoverage.coverings X
• AlgebraicGeometry.Scheme.bot_mem_precoverage 📋 Mathlib.AlgebraicGeometry.Sites.MorphismProperty
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X] : ⊥ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X
• AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff 📋 Mathlib.AlgebraicGeometry.Sites.MorphismProperty
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : CategoryTheory.Presieve.singleton f ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings S ↔ Function.Surjective ⇑f ∧ P f
• AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff 📋 Mathlib.AlgebraicGeometry.Sites.MorphismProperty
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {ι : Type u_1} {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → X i ⟶ S} : CategoryTheory.Presieve.ofArrows X f ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
• AlgebraicGeometry.Scheme.JointlySurjective.exists_eq 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
  {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.Scheme.JointlySurjective K] {X : AlgebraicGeometry.Scheme} (S : CategoryTheory.Presieve X) (hS : S ∈ K.coverings X) (x : ↥X) : ∃ Y g, S g ∧ x ∈ Set.range ⇑g
• AlgebraicGeometry.Scheme.JointlySurjective.mk 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
  {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} (exists_eq : ∀ {X : AlgebraicGeometry.Scheme}, ∀ S ∈ K.coverings X, ∀ (x : ↥X), ∃ Y g, S g ∧ x ∈ Set.range ⇑g) : AlgebraicGeometry.Scheme.JointlySurjective K
• AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff 📋 Mathlib.AlgebraicGeometry.Cover.MorphismProperty
  {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (E : CategoryTheory.PreZeroHypercover X) : E.presieve₀ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X ↔ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(E.f i)) ∧ ∀ (i : E.I₀), P (E.f i)
• CategoryTheory.MorphismProperty.IsLocalAtSource.comp 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) {U : C} (g : U ⟶ X) (hg : R g) (hf : P f) : P (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.MorphismProperty.IsLocalAtSource.of_forall_comp 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) : (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f
• CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] (H : ∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f))) : P.IsLocalAtSource K
• CategoryTheory.MorphismProperty.IsLocalAtTarget.of_forall_pullbackSnd 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtTarget K] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) (h : ∀ {U : C} {g : U ⟶ X} [inst : CategoryTheory.Limits.HasPullback f g], R g → P (CategoryTheory.Limits.pullback.snd f g)) : P f
• CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtTarget K] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X} {U : C} {g : U ⟶ X} (hR : R ∈ K.coverings X) (hg : R g) (hf : P f) [CategoryTheory.Limits.HasPullback f g] : P (CategoryTheory.Limits.pullback.snd f g)
• CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_forall_pullbackSnd 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {R : CategoryTheory.Presieve Y} (hR : R ∈ K.coverings Y) {f : X ⟶ Y} : P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : CategoryTheory.Limits.HasPullback f g], R g → P (CategoryTheory.Limits.pullback.snd f g)
• CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] (H : ∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : CategoryTheory.Presieve Y⦄, R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : CategoryTheory.Limits.HasPullback f g], R g → P (CategoryTheory.Limits.pullback.snd f g))) : P.IsLocalAtTarget K
• CategoryTheory.MorphismProperty.IsLocalAtSource.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)] (comp : ∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → ∀ {U : C} (g : U ⟶ X), R g → P f → P (CategoryTheory.CategoryStruct.comp g f)) (of_forall_comp : ∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f) : P.IsLocalAtSource K
• CategoryTheory.MorphismProperty.IsLocalAtTarget.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)] (pullbackSnd : ∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X} {U : C} {g : U ⟶ X}, R ∈ K.coverings X → R g → P f → ∀ [inst : CategoryTheory.Limits.HasPullback f g], P (CategoryTheory.Limits.pullback.snd f g)) (of_forall_pullbackSnd : ∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → (∀ {U : C} {g : U ⟶ X} [inst : CategoryTheory.Limits.HasPullback f g], R g → P (CategoryTheory.Limits.pullback.snd f g)) → P f) : P.IsLocalAtTarget K
• AlgebraicGeometry.Scheme.OpenCover.exists_of_isCofiltered_of_finite 📋 Mathlib.AlgebraicGeometry.AffineTransitionLimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] (𝒰 : c.pt.OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)] [Finite 𝒰.I₀] : ∃ i R f, ∃ (_ : CategoryTheory.Presieve.ofArrows (fun i => AlgebraicGeometry.Spec (R i)) f ∈ AlgebraicGeometry.Scheme.zariskiPrecoverage.coverings (D.obj i)), ∃ g, ∀ (j : 𝒰.I₀), CategoryTheory.IsPullback (g j) (𝒰.f j) (f j) (c.π.app i)
• 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.Cover.mem_pretopology 📋 Mathlib.AlgebraicGeometry.Sites.Pretopology
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} : CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X
• AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology 📋 Mathlib.AlgebraicGeometry.Sites.Pretopology
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {R : CategoryTheory.Presieve X} : R ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X → ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
• AlgebraicGeometry.Scheme.mem_pretopology_iff 📋 Mathlib.AlgebraicGeometry.Sites.Pretopology
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {R : CategoryTheory.Presieve X} : R ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
• CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C} {X : C} {E : CategoryTheory.PreZeroHypercover X} : E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E
• CategoryTheory.Precoverage.preZeroHypercoverFamily_property 📋 Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
  {C : Type u} [CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) (X : C) (E : CategoryTheory.PreZeroHypercover X) : K.preZeroHypercoverFamily.property E = (E.presieve₀ ∈ K.coverings X)
• CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C} {X : C} {R : CategoryTheory.Presieve X} : R ∈ P.precoverage.coverings X ↔ ∃ E, P.property E ∧ R = E.presieve₀
• AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  {S : AlgebraicGeometry.Scheme} {E : CategoryTheory.PreZeroHypercover S} : E.presieve₀ ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings S ↔ AlgebraicGeometry.QuasiCompactCover E
• AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f] : CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings Y
• AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hf : P f) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f] : CategoryTheory.Presieve.singleton f ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings Y
• AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} {R : CategoryTheory.Presieve S} : R ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings S ↔ ∃ 𝒰, AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀
• AlgebraicGeometry.Scheme.bot_mem_qcPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X] : ⊥ ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings X
• AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.QuasiCompact
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X] : ⊥ ∈ (AlgebraicGeometry.Scheme.propQCPrecoverage P).coverings X
• AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.Fpqc
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.LocallyOfFinitePresentation f] : CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.fppfPrecoverage.coverings Y
• AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage 📋 Mathlib.AlgebraicGeometry.Sites.Fpqc
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f] : CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.fpqcPrecoverage.coverings Y
• CategoryTheory.MorphismProperty.exists_map_eq_of_presieve 📋 Mathlib.CategoryTheory.MorphismProperty.CommaSites
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) (H : K ≤ P.precoverage) {X : P.Over ⊤ S} {R : CategoryTheory.Presieve ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).obj X)} (hR : R ∈ (CategoryTheory.Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).obj X)) : ∃ T, CategoryTheory.Presieve.map (CategoryTheory.MorphismProperty.Over.forget P ⊤ S) T = R
• CategoryTheory.MorphismProperty.sourceLocalClosure.comp 📋 Mathlib.CategoryTheory.MorphismProperty.LocalClosure
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.MorphismProperty.sourceLocalClosure K P f) (R : CategoryTheory.Presieve X) (hR : R ∈ K.coverings X) {U : C} (g : U ⟶ X) : R g → CategoryTheory.MorphismProperty.sourceLocalClosure K P (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.MorphismProperty.sourceLocalClosure.of_presieve 📋 Mathlib.CategoryTheory.MorphismProperty.LocalClosure
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y) (R : CategoryTheory.Presieve X) (hR : R ∈ K.coverings X) (h : ∀ (U : C) (g : U ⟶ X), R g → CategoryTheory.MorphismProperty.sourceLocalClosure K P (CategoryTheory.CategoryStruct.comp g f)) : CategoryTheory.MorphismProperty.sourceLocalClosure K P f
• CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft 📋 Mathlib.CategoryTheory.MorphismProperty.LocalClosure
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] [P.RespectsLeft K.morphismProperty] [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] {X Y : C} {f : X ⟶ Y} : CategoryTheory.MorphismProperty.sourceLocalClosure K P f ↔ ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (CategoryTheory.CategoryStruct.comp g f)
• CategoryTheory.ObjectProperty.IsLocal.component 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) {Y : C} (f : Y ⟶ X) (hf : R f) : P X → P Y
• CategoryTheory.ObjectProperty.IsLocal.of_presieve 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [self : P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) (H : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y) : P X
• CategoryTheory.ObjectProperty.iff_of_presieve 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X) : P X ↔ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
• CategoryTheory.ObjectProperty.IsLocal.mk 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [toIsClosedUnderIsomorphisms : P.IsClosedUnderIsomorphisms] (component : ∀ {X : C} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → ∀ {Y : C} (f : Y ⟶ X), R f → P X → P Y) (of_presieve : ∀ {X : C} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y) → P X) : P.IsLocal K
• CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage 📋 Mathlib.CategoryTheory.Sites.Descent.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsPrestackFor R) : F.IsPrestack J.toGrothendieck
• CategoryTheory.Pseudofunctor.IsStack.of_precoverage 📋 Mathlib.CategoryTheory.Sites.Descent.Precoverage
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R) : F.IsStack J.toGrothendieck
• CategoryTheory.Precoverage.ofArrows_mem_finite 📋 Mathlib.CategoryTheory.Sites.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {ι : Type u_1} [Finite ι] (Y : ι → C) (f : (i : ι) → Y i ⟶ X) : CategoryTheory.Presieve.ofArrows Y f ∈ (CategoryTheory.Precoverage.finite C).coverings X
• CategoryTheory.Precoverage.mem_finite_iff 📋 Mathlib.CategoryTheory.Sites.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Presieve X} : s ∈ (CategoryTheory.Precoverage.finite C).coverings X ↔ s.uncurry.Finite
• CategoryTheory.Pretopology.ofArrows_mem_finite 📋 Mathlib.CategoryTheory.Sites.Finite
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {ι : Type u_1} [Finite ι] (Y : ι → C) (f : (i : ι) → Y i ⟶ X) : CategoryTheory.Presieve.ofArrows Y f ∈ (CategoryTheory.Pretopology.finite C).coverings X
• CategoryTheory.Precoverage.isSheafFor_subsheafify 📋 Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) {X : C} {R : CategoryTheory.Presieve X} (h : R ∈ K.coverings X) (h' : CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheafFor (K.subsheafify 𝒮).toFunctor R
• CategoryTheory.Precoverage.small_subsheafify_of_small 📋 Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)) : CategoryTheory.FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor
• CategoryTheory.Precoverage.SubsheafClosure.amalgamate 📋 Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z : C} {R : CategoryTheory.Presieve Z} (hR : R ∈ K.coverings Z) {y : CategoryTheory.Presieve.FamilyOfElements F R} (hy : y.Compatible) (hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), K.SubsheafClosure 𝒮 W (y r hr)) {t : F.obj (Opposite.op Z)} (ht : y.IsAmalgamation t) : K.SubsheafClosure 𝒮 Z t
• CategoryTheory.Precoverage.Generates.isSheaf_of_forall 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (h : K.Generates J) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheaf J F
• CategoryTheory.Precoverage.Generates.isSheaf_of_forall_max 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (self : K.Generates J) (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) (H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) : CategoryTheory.Presieve.IsSheaf J F
• CategoryTheory.Precoverage.Generates.isSheaf_type_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (H : K.Generates J) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} : CategoryTheory.Presieve.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R
• CategoryTheory.Precoverage.Generates.generate_mem 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (H : K.Generates J) {X : C} {R : CategoryTheory.Presieve X} (h : R ∈ K.coverings X) : CategoryTheory.Sieve.generate R ∈ J X
• CategoryTheory.Precoverage.Generates.mk 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (le_toPrecoverage : K ≤ J.toPrecoverage) (isSheaf_of_forall_max : ∀ (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) → CategoryTheory.Presieve.IsSheaf J F) : K.Generates J
• CategoryTheory.Precoverage.Generates.isSheaf_iff 📋 Mathlib.CategoryTheory.Sites.Precoverage.Generates
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {K : CategoryTheory.Precoverage C} {J : CategoryTheory.GrothendieckTopology C} (H : K.Generates J) {F : CategoryTheory.Functor Cᵒᵖ A} : CategoryTheory.Presheaf.IsSheaf J F ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, ∀ (M : A), CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M))) R

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c