case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) ≤ Sieve.pullback f (close J₁ S)

case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (close J₁ S) ≤ close J₁ (Sieve.pullback f S)
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) = Sieve.pullback f (close J₁ S)
apply le_antisymm
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ IsClosed J₁ (Sieve.pullback f (close J₁ S))
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) ≤ Sieve.pullback f (close J₁ S)
refine' J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) _
no goals
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ IsClosed J₁ (Sieve.pullback f (close J₁ S))
apply J₁.isClosed_pullback _ _ (J₁.close_isClosed _)
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ (close J₁ (Sieve.pullback f S)).arrows g
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (close J₁ S) ≤ close J₁ (Sieve.pullback f S)
intro Z g hg
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ sieves J₁ Z
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ (close J₁ (Sieve.pullback f S)).arrows g
change _ ∈ J₁ _
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J₁ Z
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ sieves J₁ Z
rw [← Sieve.pullback_comp]
no goals
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J₁ Z
apply hg