C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ Covers J R f
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g) → Covers J R f
intro k
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ sieves J Y_1
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ Covers J R f
apply J.transitive h
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ sieves J Z
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ sieves J Y_1
intro Z g hg
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ sieves J Z
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ sieves J Z
rw [← Sieve.pullback_comp]
no goals
case h
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ sieves J Z
apply k (g ≫ f) hg