case a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}

case a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ toGrothendieck C K = sInf {J | K ≤ ofGrothendieck C J}
apply le_antisymm
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ ∀ (b : GrothendieckTopology C), b ∈ {J | K ≤ ofGrothendieck C J} → toGrothendieck C K ≤ b
case a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}
apply le_sInf
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
⊢ toGrothendieck C K ≤ J
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ ∀ (b : GrothendieckTopology C), b ∈ {J | K ≤ ofGrothendieck C J} → toGrothendieck C K ≤ b
intro J hJ
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
⊢ toGrothendieck C K ≤ J
intro X S hS
no goals
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves (toGrothendieck C K) X
⊢ S ∈ GrothendieckTopology.sieves J X
induction hS with
| of X S hS => apply hJ ; assumption
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
case a.a.of.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering K X
case a.a.of
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ Sieve.generate S ∈ GrothendieckTopology.sieves J X
apply hJ
no goals
case a.a.of.a
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering K X
assumption
no goals
case a.a.top
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ GrothendieckTopology.sieves J X✝
apply J.top_mem
no goals
case a.a.transitive
C : Type u_1
inst✝ : Category C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : saturate K X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → saturate K Y (Sieve.pullback f S)
H1 : R ∈ GrothendieckTopology.sieves J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ GrothendieckTopology.sieves J Y
⊢ S ∈ GrothendieckTopology.sieves J X
exact J.transitive H1 _ H2
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ toGrothendieck C K ∈ {J | K ≤ ofGrothendieck C J}
case a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K
apply sInf_le
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering (ofGrothendieck C (toGrothendieck C K)) X
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
⊢ toGrothendieck C K ∈ {J | K ≤ ofGrothendieck C J}
intro X S hS
no goals
case a.a
C : Type u_1
inst✝ : Category C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ covering K X
⊢ S ∈ covering (ofGrothendieck C (toGrothendieck C K)) X
apply saturate.of _ _ hS