case a
C : Type u
inst✝ : Category C
X : TopCat
ι : Type ?u.35577
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (B i).op = β.app (B i).op
⊢ ↑(restrictHomEquivHom F F' h).symm α = ↑(restrictHomEquivHom F F' h).symm β
C : Type u
inst✝ : Category C
X : TopCat
ι : Type ?u.35577
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (B i).op = β.app (B i).op
⊢ α = β
apply (restrictHomEquivHom F F' h).symm.injective
case a.w.h
C : Type u
inst✝ : Category C
X : TopCat
ι : Type ?u.35577
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (B i).op = β.app (B i).op
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ (↑(restrictHomEquivHom F F' h).symm α).app i = (↑(restrictHomEquivHom F F' h).symm β).app i
case a
C : Type u
inst✝ : Category C
X : TopCat
ι : Type ?u.35577
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (B i).op = β.app (B i).op
⊢ ↑(restrictHomEquivHom F F' h).symm α = ↑(restrictHomEquivHom F F' h).symm β
ext i
no goals
case a.w.h
C : Type u
inst✝ : Category C
X : TopCat
ι : Type ?u.35577
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), α.app (B i).op = β.app (B i).op
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ (↑(restrictHomEquivHom F F' h).symm α).app i = (↑(restrictHomEquivHom F F' h).symm β).app i
exact he i.unop