[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
obtain rfl | hne := eq_or_ne U ⊥
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
intro _ _
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x✝ t
[PROOFSTEP]
rw [@exists_unique_iff_exists _ ⟨fun _ _ => _⟩]
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃ x, Presieve.FamilyOfElements.IsAmalgamation x✝ x
[PROOFSTEP]
refine' ⟨it.from _, fun U hU hs => IsTerminal.hom_ext _ _ _⟩
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs✝ : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
U : TopologicalSpace.Opens ↑X
hU : U ⟶ ⊥
hs : s.arrows hU
⊢ IsTerminal (F.obj (op U))
[PROOFSTEP]
rwa [le_bot_iff.1 hU.le]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1
[PROOFSTEP]
apply it.hom_ext
[GOAL]
case inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
convert Presieve.isSheafFor_top_sieve (F ⋙ coyoneda.obj (@op C c))
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s = ⊤
[PROOFSTEP]
rw [← Sieve.id_mem_iff_eq_top]
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
[PROOFSTEP]
have := (U.eq_bot_or_top hind).resolve_left hne
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
this : U = ⊤
⊢ s.arrows (𝟙 U)
[PROOFSTEP]
subst this
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
[GOAL]
case h.e'_5.h.h.e'_4.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
U : TopologicalSpace.Opens ↑X
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain rfl | rfl := U.eq_bot_or_top hind
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
cases hm
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
convert hf
