case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf (Pretopology.toGrothendieck C K) P →
    ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R

case mpr
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R) →
    IsSheaf (Pretopology.toGrothendieck C K) P
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf (Pretopology.toGrothendieck C K) P ↔
    ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
constructor
case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf (Pretopology.toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ Pretopology.coverings K X
⊢ IsSheafFor P R
case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf (Pretopology.toGrothendieck C K) P →
    ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
intro PJ X R hR
case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf (Pretopology.toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ Pretopology.coverings K X
⊢ IsSheafFor P (generate R).arrows
case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf (Pretopology.toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ Pretopology.coverings K X
⊢ IsSheafFor P R
rw [isSheafFor_iff_generate]
no goals
case mp
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf (Pretopology.toGrothendieck C K) P
X : C
R : Presieve X
hR : R ∈ Pretopology.coverings K X
⊢ IsSheafFor P (generate R).arrows
apply PJ (Sieve.generate R) ⟨_, hR, le_generate R⟩
case mpr.intro.intro
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
⊢ IsSheafFor P S.arrows
case mpr
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R) →
    IsSheaf (Pretopology.toGrothendieck C K) P
rintro PK X S ⟨R, hR, RS⟩
case mpr.intro.intro
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ IsSheafFor P S.arrows
case mpr.intro.intro
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
⊢ IsSheafFor P S.arrows
have gRS : ⇑(generate R) ≤ S := by
  apply giGenerate.gc.monotone_u
  rwa [sets_iff_generate]
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (generate R)).arrows
case mpr.intro.intro
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ IsSheafFor P S.arrows
apply isSheafFor_subsieve P gRS _
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f (generate R)).arrows
intro Y f
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (pullbackArrows f R)
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows
rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]
no goals
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (pullbackArrows f R)
exact PK (pullbackArrows f R) (K.pullbacks f R hR)
case a
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
⊢ generate R ≤ S
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
⊢ (generate R).arrows ≤ S.arrows
apply giGenerate.gc.monotone_u
no goals
case a
C : Type u₁
inst✝¹ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y : C
S✝ : Sieve X✝
R✝ : Presieve X✝
J J₂ : GrothendieckTopology C
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C} (R : Presieve X), R ∈ Pretopology.coverings K X → IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ Pretopology.coverings K X
RS : R ≤ S.arrows
⊢ generate R ≤ S
rwa [sets_iff_generate]