English
Equality relating chainSupCarrier to a union form.
Русский
Эквивалентность chainSupCarrier и объединения по индексу цепи.
LaTeX
$$$\operatorname{chainSupCarrier}(c) = \bigcup_{v\in c} \operatorname{carrier}(v)$$$
Lean4
/-- Let `F` and `G` be sheaves valued in a concrete category, whose forgetful functor reflects
isomorphisms, preserves limits and filtered colimits. Then if the stalk maps of a morphism
`f : F ⟶ G` are all isomorphisms, `f` must be an isomorphism.
-/
theorem isIso_of_stalkFunctor_map_iso {F G : Sheaf C X} (f : F ⟶ G) [∀ x : X, IsIso ((stalkFunctor C x).map f.1)] :
IsIso f := by
-- Since the inclusion functor from sheaves to presheaves is fully faithful, it suffices to
-- show that `f`, as a morphism between _presheaves_, is an isomorphism.
suffices IsIso ((Sheaf.forget C X).map f) by exact isIso_of_fully_faithful (Sheaf.forget C X) f
suffices ∀ U : (Opens X)ᵒᵖ, IsIso (f.1.app U) by exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this
intro U; induction U
apply app_isIso_of_stalkFunctor_map_iso
