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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ IsIso ((forget C).map (f.val.app U.op))
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ IsIso (f.val.app U.op)
suffices IsIso ((forget C).map (f.1.app (op U))) by
  exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ Function.Bijective ((forget C).map (f.val.app U.op))
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ IsIso ((forget C).map (f.val.app U.op))
rw [isIso_iff_bijective]
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ ∀ (x : { x // x ∈ U }), Function.Bijective ((forget C).map ((stalkFunctor C ↑x).map f.val))
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ Function.Bijective ((forget C).map (f.val.app U.op))
apply app_bijective_of_stalkFunctor_map_bijective
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
x : { x // x ∈ U }
⊢ Function.Bijective ((forget C).map ((stalkFunctor C ↑x).map f.val))
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
⊢ ∀ (x : { x // x ∈ U }), Function.Bijective ((forget C).map ((stalkFunctor C ↑x).map f.val))
intro x
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
x : { x // x ∈ U }
⊢ IsIso ((forget C).map ((stalkFunctor C ↑x).map f.val))
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
x : { x // x ∈ U }
⊢ Function.Bijective ((forget C).map ((stalkFunctor C ↑x).map f.val))
apply (isIso_iff_bijective _).mp
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
x : { x // x ∈ U }
⊢ IsIso ((forget C).map ((stalkFunctor C ↑x).map f.val))
exact Functor.map_isIso (forget C) ((stalkFunctor C x.1).map f.1)
no goals
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : { x // x ∈ U }), IsIso ((stalkFunctor C ↑x).map f.val)
this : IsIso ((forget C).map (f.val.app U.op))
⊢ IsIso (f.val.app U.op)
exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)