ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor D E<VAR>R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.functorPushforward (F.comp G) R = CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPushforward F R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>Monotone (CategoryTheory.Sieve.functorPullback F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>Monotone (CategoryTheory.Sieve.functorPushforward F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Sieve X<GOAL>R ≤ CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F R)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Sieve (F.obj X)<GOAL>CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.functorPullback F R) ≤ R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>S R : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.functorPushforward F (S ⊔ R) = CategoryTheory.Sieve.functorPushforward F S ⊔ CategoryTheory.Sieve.functorPushforward F R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>S R : CategoryTheory.Sieve (F.obj X)<GOAL>CategoryTheory.Sieve.functorPullback F (S ⊔ R) = CategoryTheory.Sieve.functorPullback F S ⊔ CategoryTheory.Sieve.functorPullback F R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>S R : CategoryTheory.Sieve (F.obj X)<GOAL>CategoryTheory.Sieve.functorPullback F (S ⊓ R) = CategoryTheory.Sieve.functorPullback F S ⊓ CategoryTheory.Sieve.functorPullback F R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>CategoryTheory.Sieve.functorPushforward F ⊥ = ⊥
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>CategoryTheory.Sieve.functorPushforward F ⊤ = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>CategoryTheory.Sieve.functorPullback F ⊥ = ⊥
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>CategoryTheory.Sieve.functorPullback F ⊤ = ⊤
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>R : CategoryTheory.Sieve X<VAR>V : C<VAR>f : V ⟶ X<VAR>h : R.arrows f<GOAL>(CategoryTheory.Sieve.functorPushforward F R).arrows (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>e : C ≌ D<GOAL>CategoryTheory.Sieve.functorPushforward e.functor S = CategoryTheory.Sieve.functorPullback e.inverse (CategoryTheory.Sieve.pullback (e.unitInv.app X) S)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : C<VAR>Y : D<VAR>S : CategoryTheory.Sieve X<VAR>e : C ≌ D<VAR>f : Y ⟶ e.functor.obj X<GOAL>(CategoryTheory.Sieve.functorPushforward e.functor S).arrows f ↔ S.arrows (CategoryTheory.CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : D<VAR>S : CategoryTheory.Sieve X<VAR>e : C ≌ D<GOAL>CategoryTheory.Sieve.functorPushforward e.inverse S = CategoryTheory.Sieve.functorPullback e.functor (CategoryTheory.Sieve.pullback (e.counit.app X) S)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Y : C<VAR>X : D<VAR>S : CategoryTheory.Sieve X<VAR>e : C ≌ D<VAR>f : Y ⟶ e.inverse.obj X<GOAL>(CategoryTheory.Sieve.functorPushforward e.inverse S).arrows f ↔ S.arrows (CategoryTheory.CategoryStruct.comp (e.functor.map f) (e.counit.app X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (g : { g // S.arrows g }), ↑(S.functor.map f g) = CategoryTheory.CategoryStruct.comp f.unop ↑g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>Y : Cᵒᵖ<GOAL>S.functor.obj Y = { g // S.arrows g }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S T : CategoryTheory.Sieve X<VAR>h : S ≤ T<VAR>Y : Cᵒᵖ<VAR>f : S.functor.obj Y<GOAL>↑((CategoryTheory.Sieve.natTransOfLe h).app Y f) = ↑f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>Y : Cᵒᵖ<VAR>f : S.functor.obj Y<GOAL>S.functorInclusion.app Y f = ↑f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S T : CategoryTheory.Sieve X<VAR>h : S ≤ T<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.natTransOfLe h) T.functorInclusion = S.functorInclusion
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>R : CategoryTheory.Functor Cᵒᵖ (Type v₁)<VAR>f : R ⟶ CategoryTheory.yoneda.obj X<VAR>Y : C<VAR>g : Y ⟶ X<GOAL>(CategoryTheory.Sieve.sieveOfSubfunctor f).arrows g = ∃ t, f.app (Opposite.op Y) t = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Sieve.sieveOfSubfunctor S.functorInclusion = S
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c : C<VAR>x y : c ⟶ c<GOAL>x * y = CategoryTheory.CategoryStruct.comp x y
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c : C<GOAL>∀ (a : c ⟶ c), a⁻¹ = CategoryTheory.Groupoid.inv a
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c : C<GOAL>1 = CategoryTheory.CategoryStruct.id c
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c : C<VAR>γ : c ⟶ c<GOAL>γ⁻¹ = CategoryTheory.inv γ
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>δ : d ⟶ d<GOAL>(CategoryTheory.Groupoid.vertexGroupIsomOfMap f).symm δ = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp δ (CategoryTheory.Groupoid.inv f))
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>γ : c ⟶ c<GOAL>(CategoryTheory.Groupoid.vertexGroupIsomOfMap f) γ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) (CategoryTheory.CategoryStruct.comp γ f)
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>D : Type v<VAR>CategoryTheory.Groupoid D<VAR>φ : CategoryTheory.Functor C D<VAR>c : C<GOAL>∀ (a : c ⟶ c), (CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup φ c) a = φ.map a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>Y : CategoryTheory.Over X<GOAL>(CategoryTheory.Sieve.overEquiv Y) ⊤ = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>Y : CategoryTheory.Over X<GOAL>(CategoryTheory.Sieve.overEquiv Y).symm ⊤ = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>Y₁ Y₂ : CategoryTheory.Over X<VAR>f : Y₁ ⟶ Y₂<VAR>S : CategoryTheory.Sieve Y₂<GOAL>(CategoryTheory.Sieve.overEquiv Y₁) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f.left ((CategoryTheory.Sieve.overEquiv Y₂) S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>Y : CategoryTheory.Over X<VAR>S : CategoryTheory.Sieve Y.left<VAR>Z : CategoryTheory.Over X<VAR>f : Z ⟶ Y<GOAL>((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f ↔ S.arrows f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>Y : CategoryTheory.Over X<VAR>S : CategoryTheory.Sieve Y<VAR>Z : C<VAR>f : Z ⟶ Y.left<GOAL>((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : CategoryTheory.Over X<VAR>S : CategoryTheory.Sieve Z.left<GOAL>CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map f) ((CategoryTheory.Sieve.overEquiv Z).symm S) = (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.map f).obj Z)).symm S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>Y : CategoryTheory.Over X<VAR>S : CategoryTheory.Sieve Y<GOAL>S ∈ (J.over X).sieves Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J.sieves Y.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>Y : CategoryTheory.Over X<VAR>S : CategoryTheory.Sieve Y.left<VAR>hS : S ∈ J.sieves Y.left<GOAL>(CategoryTheory.Sieve.overEquiv Y).symm S ∈ (J.over X).sieves Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<GOAL>CategoryTheory.CoverPreserving (J.over X) J (CategoryTheory.Over.forget X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<GOAL>CategoryTheory.CompatiblePreserving J (CategoryTheory.Over.forget X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CoverPreserving (J.over X) (J.over Y) (CategoryTheory.Over.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CompatiblePreserving (J.over Y) (CategoryTheory.Over.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>z₁ z₂ : CategoryTheory.Equalizer.FirstObj P R<VAR>h : ∀ (Y : C) (f : Y ⟶ X) (hf : R f), CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>t : CategoryTheory.Equalizer.FirstObj P R<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : R f<GOAL>(CategoryTheory.Equalizer.firstObjEqFamily P R).hom t f hf = CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>∀ (a : CategoryTheory.Presieve.FamilyOfElements P R), (CategoryTheory.Equalizer.firstObjEqFamily P R).inv a = CategoryTheory.Limits.Pi.lift (fun f x => x ↑f.snd ⋯) a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S<VAR>h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ = CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows) (CategoryTheory.Equalizer.Sieve.firstMap P S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P S.arrows) (CategoryTheory.Equalizer.Sieve.secondMap P S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>x : CategoryTheory.Equalizer.FirstObj P S.arrows<GOAL>((CategoryTheory.Equalizer.firstObjEqFamily P S.arrows).hom x).Compatible ↔ CategoryTheory.Equalizer.Sieve.firstMap P S x = CategoryTheory.Equalizer.Sieve.secondMap P S x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>R.hasPullbacks<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P R) (CategoryTheory.Equalizer.Presieve.firstMap P R) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.forkMap P R) (CategoryTheory.Equalizer.Presieve.secondMap P R)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>R.hasPullbacks<VAR>x : CategoryTheory.Equalizer.FirstObj P R<GOAL>((CategoryTheory.Equalizer.firstObjEqFamily P R).hom x).Compatible ↔ CategoryTheory.Equalizer.Presieve.firstMap P R x = CategoryTheory.Equalizer.Presieve.secondMap P R x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>R.hasPullbacks<GOAL>CategoryTheory.Presieve.IsSheafFor P R ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P R) ⋯))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>I : Type<VAR>X : I → C<VAR>z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X<VAR>h : ∀ (i : I), CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i z₁ = CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<VAR>z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π<VAR>h : ∀ (ij : I × I), CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij z₁ = CategoryTheory.Limits.Pi.π (fun ij => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))) ij z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) (CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) (CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<VAR>x : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X<GOAL>CategoryTheory.Presieve.Arrows.Compatible P π ((CategoryTheory.Limits.Types.productIso fun i => P.obj (Opposite.op (X i))).hom x) ↔ CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π x = CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>(CategoryTheory.Presieve.ofArrows X π).hasPullbacks<GOAL>CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) = CategoryTheory.Sieve.generateSingleton f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : Y ⟶ X<GOAL>(CategoryTheory.Presieve.singleton f).EffectiveEpimorphic ↔ CategoryTheory.EffectiveEpi f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows X π) = CategoryTheory.Sieve.generateFamily X π
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>(CategoryTheory.Presieve.ofArrows X π).EffectiveEpimorphic ↔ CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f : S.arrows.categoryᵒᵖ<GOAL>((CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E).symm x).app f = ↑x (Opposite.unop f).obj.hom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>E : Aᵒᵖ<VAR>π : (S.arrows.diagram.op.comp P).cones.obj E<VAR>Y : C<VAR>f : Y ⟶ X<VAR>h : S.arrows f<GOAL>↑((CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily P S E) π) f h = π.app (Opposite.op { obj := CategoryTheory.Over.mk f, property := h })
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>(∀ (E : A), CategoryTheory.Presieve.IsSeparated J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) ↔ ∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, ∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>R : CategoryTheory.Presieve X<GOAL>Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>K : CategoryTheory.Pretopology C<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>E : A<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>S : J.Cover X<VAR>x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y)<VAR>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)<VAR>I : S.Arrow<GOAL>CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>E : A<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>S : J.Cover X<VAR>e₁ e₂ : E ⟶ P.obj (Opposite.op X)<VAR>h : ∀ (I : S.Arrow), CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)<GOAL>e₁ = e₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : CategoryTheory.Sieve.ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x y : E ⟶ P.obj (Opposite.op S)<VAR>h : ∀ (i : I), CategoryTheory.CategoryStruct.comp x (P.map (f i).op) = CategoryTheory.CategoryStruct.comp y (P.map (f i).op)<GOAL>x = y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : CategoryTheory.Sieve.ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x : (i : I) → E ⟶ P.obj (Opposite.op (X i))<VAR>hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) → CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)<GOAL>∃! g, ∀ (i : I), CategoryTheory.CategoryStruct.comp g (P.map (f i).op) = x i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : CategoryTheory.Sieve.ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x : (i : I) → E ⟶ P.obj (Opposite.op (X i))<VAR>hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j), CategoryTheory.CategoryStruct.comp a (f i) = CategoryTheory.CategoryStruct.comp b (f j) → CategoryTheory.CategoryStruct.comp (x i) (P.map a.op) = CategoryTheory.CategoryStruct.comp (x j) (P.map b.op)<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (hP.amalgamateOfArrows f hf x hx) (P.map (f i).op) = x i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P P' : CategoryTheory.Functor Cᵒᵖ A<VAR>e : P ≅ P'<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J P'