C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F ↔ IsSheafPreservesLimitPairwiseIntersections F
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheaf F ↔ IsSheafPreservesLimitPairwiseIntersections F
rw [isSheaf_iff_isSheafPairwiseIntersections]
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F → IsSheafPreservesLimitPairwiseIntersections F

case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPreservesLimitPairwiseIntersections F → IsSheafPairwiseIntersections F
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F ↔ IsSheafPreservesLimitPairwiseIntersections F
constructor
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (PreservesLimit (Functor.op (Pairwise.diagram U)) F)
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPairwiseIntersections F → IsSheafPreservesLimitPairwiseIntersections F
intro h ι U
no goals
case mp
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (PreservesLimit (Functor.op (Pairwise.diagram U)) F)
exact ⟨preservesLimitOfPreservesLimitCone (Pairwise.coconeIsColimit U).op (h U).some⟩
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
⊢ IsSheafPreservesLimitPairwiseIntersections F → IsSheafPairwiseIntersections F
intro h ι U
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Functor.op (Pairwise.diagram U)) F
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
haveI := (h U).some
no goals
case mpr
C : Type u
inst✝ : Category C
X : TopCat
F : Presheaf C X
h : IsSheafPreservesLimitPairwiseIntersections F
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Functor.op (Pairwise.diagram U)) F
⊢ Nonempty (IsLimit (F.mapCone (Cocone.op (Pairwise.cocone U))))
exact ⟨PreservesLimit.preserves (Pairwise.coconeIsColimit U).op⟩