[GOAL]
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) = U
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ ∀ (i : (V : Opens ↑X) × { f // R f }), coveringOfPresieve U R i ≤ U
[PROOFSTEP]
intro f
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
f : (V : Opens ↑X) × { f // R f }
⊢ coveringOfPresieve U R f ≤ U
[PROOFSTEP]
exact f.2.1.le
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)
[PROOFSTEP]
intro x hxU
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup (coveringOfPresieve U R))
[PROOFSTEP]
rw [Opens.coe_iSup, Set.mem_iUnion]
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)
[PROOFSTEP]
obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)
[PROOFSTEP]
exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩
[GOAL]
X : TopCat
Y : Opens ↑X
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
[PROOFSTEP]
funext Z
[GOAL]
case h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
[PROOFSTEP]
ext f
[GOAL]
case h.h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y ↔ f ∈ R
[PROOFSTEP]
exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩
[GOAL]
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
x✝ : f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y
f' : Z ⟶ Y
h : R f'
⊢ f ∈ R
[PROOFSTEP]
rwa [Subsingleton.elim f f']
[GOAL]
X : TopCat
ι : Type v
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCovering U) ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
[PROOFSTEP]
intro x hx
[GOAL]
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx
[GOAL]
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
[PROOFSTEP]
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩
[GOAL]
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔ Opens.IsBasis (Set.range B.obj)
[PROOFSTEP]
rw [Opens.isBasis_iff_nbhd]
[GOAL]
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
constructor
[GOAL]
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B →
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
intro hd U x hx
[GOAL]
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩
[GOAL]
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑X
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac✝ : f₁ ≫ f₂ = f
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩
[GOAL]
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
intro hb
[GOAL]
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
constructor
[GOAL]
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
[PROOFSTEP]
intro U x hx
[GOAL]
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
[PROOFSTEP]
rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩
[GOAL]
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx✝ : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
[PROOFSTEP]
exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ↑f))
[PROOFSTEP]
haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.inj
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ↑f))
[PROOFSTEP]
apply compatiblePreservingOfDownwardsClosed
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
⊢ {c : Opens ↑X} →
    {d : Opens ↑Y} →
      (d ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c) →
        (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c' ≅ d)
[PROOFSTEP]
intro U V i
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
⊢ (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c' ≅ V)
[PROOFSTEP]
refine' ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ _⟩
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range fun x => ↑f x
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := i.le h
[GOAL]
case hF.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
w✝ : (forget TopCat).obj X
left✝ : w✝ ∈ ↑U
h : ↑f w✝ ∈ V.1
⊢ ↑f w✝ ∈ Set.range fun x => ↑f x
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) (functor hf)
[PROOFSTEP]
constructor
[GOAL]
case cover_preserve
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward (functor hf) S ∈
        GrothendieckTopology.sieves (Opens.grothendieckTopology ↑Y) ((functor hf).obj U)
[PROOFSTEP]
rintro U S hU _ ⟨x, hx, rfl⟩
[GOAL]
case cover_preserve.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ ↑f x ∈ U_1
[PROOFSTEP]
obtain ⟨V, i, hV, hxV⟩ := hU x hx
[GOAL]
case cover_preserve.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ ↑f x ∈ U_1
[PROOFSTEP]
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F✝ : Presheaf C X
F' : Sheaf C X
h✝ : Opens.IsBasis (Set.range B)
F : Sheaf C X
U : Opens ↑X
h : U = ⊥
⊢ Limits.IsTerminal (F.val.obj (op U))
[PROOFSTEP]
convert F.isTerminalOfEmpty
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h) α) (op (B i)) = NatTrans.app α (op i)
[PROOFSTEP]
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h) α) (op (B i)) =
    NatTrans.app (Equiv.invFun (restrictHomEquivHom F F' h) (Equiv.toFun (restrictHomEquivHom F F' h) α)) (op i)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
⊢ α = β
[PROOFSTEP]
apply (restrictHomEquivHom F F' h).symm.injective
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
⊢ ↑(restrictHomEquivHom F F' h).symm α = ↑(restrictHomEquivHom F F' h).symm β
[PROOFSTEP]
ext i
[GOAL]
case a.w.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h).symm α) i = NatTrans.app (↑(restrictHomEquivHom F F' h).symm β) i
[PROOFSTEP]
exact he i.unop
