Loogle!

Result

Found 74 declarations mentioning CategoryTheory.GrothendieckTopology.Cover.Arrow.Y.

• CategoryTheory.GrothendieckTopology.Cover.Arrow.Y 📋 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) : C
• CategoryTheory.GrothendieckTopology.Cover.Arrow.f 📋 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) : self.Y ⟶ X
• CategoryTheory.GrothendieckTopology.Cover.bind 📋 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) : J.Cover X
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : S.Arrow
• CategoryTheory.GrothendieckTopology.Cover.Arrow.middle 📋 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) : C
• CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle 📋 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.Arrow
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precomp g).Relation I
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp_Y 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precomp g).Y = Z
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂) : self.Z ⟶ I₁.Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂) : self.Z ⟶ I₂.Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom 📋 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) : I.middle ⟶ X
• CategoryTheory.GrothendieckTopology.Cover.bindToBase 📋 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) : S.bind T ⟶ S
• CategoryTheory.GrothendieckTopology.Cover.Arrow.base_Y 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : J.Cover X} (I : (S.pullback f).Arrow) : I.base.Y = I.Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddle 📋 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).Arrow
• CategoryTheory.GrothendieckTopology.Cover.index_left 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D) (I : S.shape.L) : (S.index P).left I = P.obj (Opposite.op I.Y)
• CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom 📋 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) : I.Y ⟶ I.middle
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_Z 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precompRelation g).Z = (I.precomp g).Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₂ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precompRelation g).g₂ = g
• 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.Cover.Arrow.map_Y 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S T : J.Cover X} (I : S.Arrow) (f : S ⟶ T) : (I.map f).Y = I.Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precomp_f 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precomp g).f = CategoryTheory.CategoryStruct.comp g I.f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.map_f 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S T : J.Cover X} (I : S.Arrow) (f : S ⟶ T) : (I.map f).f = I.f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.ext 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {x y : S.Arrow} (Y : x.Y = y.Y) (f : x.f ≍ y.f) : x = y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.ext_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {x y : S.Arrow} : x = y ↔ x.Y = y.Y ∧ x.f ≍ y.f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.from_middle_condition 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow) : (↑S).arrows I.fromMiddleHom
• CategoryTheory.GrothendieckTopology.Cover.Arrow.base_f 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : J.Cover X} (I : (S.pullback f).Arrow) : I.base.f = CategoryTheory.CategoryStruct.comp I.f f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₁ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y) : (I.precompRelation g).g₁ = CategoryTheory.CategoryStruct.id (I.precomp g).Y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec 📋 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) : CategoryTheory.CategoryStruct.comp I.toMiddleHom I.fromMiddleHom = I.f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.mk 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} (Z : C) (g₁ : Z ⟶ I₁.Y) (g₂ : Z ⟶ I₂.Y) (w : CategoryTheory.CategoryStruct.comp g₁ I₁.f = CategoryTheory.CategoryStruct.comp g₂ I₂.f := by cat_disch) : I₁.Relation I₂
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂) : CategoryTheory.CategoryStruct.comp self.g₁ I₁.f = CategoryTheory.CategoryStruct.comp self.g₂ I₂.f
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map_g₁ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S T : J.Cover X} {I₁ I₂ : S.Arrow} (r : I₁.Relation I₂) (f : S ⟶ T) : (r.map f).g₁ = r.g₁
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map_g₂ 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S T : J.Cover X} {I₁ I₂ : S.Arrow} (r : I₁.Relation I₂) (f : S ⟶ T) : (r.map f).g₂ = r.g₂
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w_assoc 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.g₁ (CategoryTheory.CategoryStruct.comp I₁.f h) = CategoryTheory.CategoryStruct.comp self.g₂ (CategoryTheory.CategoryStruct.comp I₂.f h)
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.ext 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} {x y : I₁.Relation I₂} (Z : x.Z = y.Z) (g₁ : x.g₁ ≍ y.g₁) (g₂ : x.g₂ ≍ y.g₂) : x = y
• CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.ext_iff 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : J.Cover X} {I₁ I₂ : S.Arrow} {x y : I₁.Relation I₂} : x = y ↔ x.Z = y.Z ∧ x.g₁ ≍ y.g₁ ∧ x.g₂ ≍ y.g₂
• 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.Cover.index_fst 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D) (I : S.shape.R) : (S.index P).fst I = P.map I.r.g₁.op
• CategoryTheory.GrothendieckTopology.Cover.index_snd 📋 Mathlib.CategoryTheory.Sites.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D) (I : S.shape.R) : (S.index P).snd I = P.map I.r.g₂.op
• CategoryTheory.Presheaf.IsSheaf.hom_ext 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (Opposite.op X)) (h : ∀ (I : S.Arrow), CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) : e₁ = e₂
• CategoryTheory.Presheaf.IsSheaf.amalgamate 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) : E ⟶ P.obj (Opposite.op X)
• CategoryTheory.Presheaf.IsSheaf.amalgamate_map 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) (I : S.Arrow) : CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I
• CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y)) (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) = CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)) (I : S.Arrow) {Z : A} (h : P.obj (Opposite.op I.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (CategoryTheory.CategoryStruct.comp (P.map I.f.op) h) = CategoryTheory.CategoryStruct.comp (x I) h
• CategoryTheory.GrothendieckTopology.diagramNatTrans_app 📋 Mathlib.CategoryTheory.Sites.Plus
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (X : C) (W : (J.Cover X)ᵒᵖ) : (J.diagramNatTrans η X).app W = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun x => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) x) (η.app (Opposite.op x.Y))) ⋯
• CategoryTheory.Meq.instCoeFunForallToTypeObjOppositeOpY 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X) : CoeFun (CategoryTheory.Meq P S) fun x => (I : S.Arrow) → CategoryTheory.ToType (P.obj (Opposite.op I.Y))
• CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) : CategoryTheory.Presheaf.IsSheaf J (J.plusObj P)
• CategoryTheory.GrothendieckTopology.Plus.exists_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) : ∃ t, CategoryTheory.Meq.mk S t = s
• CategoryTheory.GrothendieckTopology.Plus.sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C} (P : CategoryTheory.Functor Cᵒᵖ D) (S : J.Cover X) (x y : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))) (h : ∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y) : x = y
• CategoryTheory.GrothendieckTopology.Plus.inj_of_sep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X)))
• CategoryTheory.Meq.mk_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.ToType (P.obj (Opposite.op X))) (I : S.Arrow) : ↑(CategoryTheory.Meq.mk S x) I = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x
• CategoryTheory.Meq.equiv_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer (S.index P))) (I : S.Arrow) : ↑((CategoryTheory.Meq.equiv P S) x) I = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I)) x
• CategoryTheory.Meq.equiv_symm_eq_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} [CategoryTheory.Limits.HasMultiequalizer (S.index P)] (x : CategoryTheory.Meq P S) (I : S.Arrow) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I)) ((CategoryTheory.Meq.equiv P S).symm x) = ↑x I
• CategoryTheory.GrothendieckTopology.Plus.toPlus_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (S : J.Cover X) (x : CategoryTheory.Meq P S) (I : S.Arrow) : (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op I.Y))) (↑x I) = (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (CategoryTheory.GrothendieckTopology.Plus.mk x)
• CategoryTheory.GrothendieckTopology.Plus.meqOfSep 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD] [∀ {X : C} (S : J.Cover X), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] (P : CategoryTheory.Functor Cᵒᵖ D) (hsep : ∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))), (∀ (I : S.Arrow), (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x = (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) → x = y) (X : C) (S : J.Cover X) (s : CategoryTheory.Meq (J.plusObj P) S) (T : (I : S.Arrow) → J.Cover I.Y) (t : (I : S.Arrow) → CategoryTheory.Meq P (T I)) (ht : ∀ (I : S.Arrow), ↑s I = CategoryTheory.GrothendieckTopology.Plus.mk (t I)) : CategoryTheory.Meq P (S.bind T)
• CategoryTheory.Meq.ext 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x y : CategoryTheory.Meq P S) (h : ∀ (I : S.Arrow), ↑x I = ↑y I) : x = y
• CategoryTheory.Meq.ext_iff 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} {x y : CategoryTheory.Meq P S} : x = y ↔ ∀ (I : S.Arrow), ↑x I = ↑y I
• CategoryTheory.Meq.refine_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S T : J.Cover X} (x : CategoryTheory.Meq P T) (e : S ⟶ T) (I : S.Arrow) : ↑(x.refine e) I = ↑x { Y := I.Y, f := I.f, hf := ⋯ }
• CategoryTheory.Meq.congr_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) {Y : C} {f g : Y ⟶ X} (h : f = g) (hf : (↑S).arrows f) : ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := g, hf := ⋯ }
• CategoryTheory.Meq.condition 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (I : S.Relation) : (CategoryTheory.ConcreteCategory.hom (P.map I.r.g₁.op)) (↑x (S.shape.fst I)) = (CategoryTheory.ConcreteCategory.hom (P.map I.r.g₂.op)) (↑x (S.shape.snd I))
• CategoryTheory.Meq.pullback_apply 📋 Mathlib.CategoryTheory.Sites.ConcreteSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] {Y X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X) (I : ((J.pullback f).obj S).Arrow) : ↑(x.pullback f) I = ↑x { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }
• CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) : CategoryTheory.Limits.Cone (F.comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op i.Y)))
• CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) : E.pt ⟶ (CategoryTheory.Limits.limit F).obj (Opposite.op i.Y)
• CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).pt = E.pt
• CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) (k : K) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).π.app k = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj k)) i)
• CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)
• CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc 📋 Mathlib.CategoryTheory.Sites.LeftExact
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{t, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type s} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) {Z : D} (h : (F.obj k).obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)) h
• CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (f : S.Arrow) : S.preOneHypercover.X f = f.Y
• CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (f : S.Arrow) : S.preOneHypercover.f f = f.f
• CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) : S.preOneHypercover.p₁ r = r.g₁
• CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) : S.preOneHypercover.p₂ r = r.g₂
• CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : J.Cover X) (f₁ f₂ : S.Arrow) {W : C} (p₁ : W ⟶ f₁.Y) (p₂ : W ⟶ f₂.Y) (w : CategoryTheory.CategoryStruct.comp p₁ f₁.f = CategoryTheory.CategoryStruct.comp p₂ f₂.f) : S.preOneHypercover.sieve₁ p₁ p₂ = ⊤
• CategoryTheory.RanIsSheafOfIsCocontinuous.fac 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i
• CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A} {f g : W ⟶ R.obj (Opposite.op X)} (h : ∀ (i : S.Arrow), CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) : f = g
• CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) {Z : A} (h : R.obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) = CategoryTheory.CategoryStruct.comp (s.ι i) h
• CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y) (w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))

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