C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ s = t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
⊢ s = t
choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x)
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ U ≤ iSup V

case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (i₁ i).op) s = (forget C).map (F.val.map (i₁ i).op) t
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ s = t
apply F.eq_of_locally_eq' V U i₁
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ U ≤ iSup V
intro x hxU
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)
erw [Opens.mem_iSup]
no goals
case hcover
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i
exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : { x // x ∈ U }
⊢ (forget C).map (F.val.map (i₁ x).op) s = (forget C).map (F.val.map (i₁ x).op) t
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
⊢ ∀ (i : { x // x ∈ U }), (forget C).map (F.val.map (i₁ i).op) s = (forget C).map (F.val.map (i₁ i).op) t
intro x
no goals
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
U : Opens ↑X
s t : (forget C).obj (F.val.obj U.op)
h : ∀ (x : { x // x ∈ U }), (forget C).map (germ (Sheaf.presheaf F) x) s = (forget C).map (germ (Sheaf.presheaf F) x) t
V : { x // x ∈ U } → Opens ↑X
m : ∀ (x : { x // x ∈ U }), ↑x ∈ V x
i₁ i₂ : (x : { x // x ∈ U }) → V x ⟶ U
heq :
  ∀ (x : { x // x ∈ U }),
    (forget C).map ((Sheaf.presheaf F).map (i₁ x).op) s = (forget C).map ((Sheaf.presheaf F).map (i₂ x).op) t
x : { x // x ∈ U }
⊢ (forget C).map (F.val.map (i₁ x).op) s = (forget C).map (F.val.map (i₁ x).op) t
rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]