C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf (Pretopology.toGrothendieck C K) (P ⋙ coyoneda.obj E.op)) ↔
    ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ Pretopology.coverings K X → Nonempty (IsLimit (P.mapCone (Cocone.op (cocone (generate R).arrows))))
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf (Pretopology.toGrothendieck C K) P ↔
    ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ Pretopology.coverings K X → Nonempty (IsLimit (P.mapCone (Cocone.op (cocone (generate R).arrows))))
dsimp [IsSheaf]
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A) {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor (P ⋙ coyoneda.obj E.op) R) ↔
    ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ Pretopology.coverings K X → Nonempty (IsLimit (P.mapCone (Cocone.op (cocone (generate R).arrows))))
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf (Pretopology.toGrothendieck C K) (P ⋙ coyoneda.obj E.op)) ↔
    ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ Pretopology.coverings K X → Nonempty (IsLimit (P.mapCone (Cocone.op (cocone (generate R).arrows))))
simp_rw [isSheaf_pretopology]
no goals
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A) {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor (P ⋙ coyoneda.obj E.op) R) ↔
    ∀ ⦃X : C⦄ (R : Presieve X),
      R ∈ Pretopology.coverings K X → Nonempty (IsLimit (P.mapCone (Cocone.op (cocone (generate R).arrows))))
exact
  ⟨fun h X R hR => (isLimit_iff_isSheafFor_presieve P R).2 fun E => h E.unop R hR,
    fun h E X R hR => (isLimit_iff_isSheafFor_presieve P R).1 (h R hR) (op E)⟩