English
Definition: chainSupCarrier(c) is the union of the carriers of all elements of the chain c.
Русский
Определение: chainSupCarrier(c) есть объединение множеств носителей всех элементов цепи c.
LaTeX
$$$\operatorname{chainSupCarrier}(c) = \bigcup_{v\in c} \operatorname{carrier}(v)$$$
Lean4
theorem app_isIso_of_stalkFunctor_map_iso {F G : Sheaf C X} (f : F ⟶ G) (U : Opens X)
[∀ x : U, IsIso ((stalkFunctor C x.val).map f.1)] : IsIso (f.1.app (op U)) := by
-- Since the forgetful functor of `C` reflects isomorphisms, it suffices to see that the
-- underlying map between types is an isomorphism, i.e. bijective.
suffices IsIso ((forget C).map (f.1.app (op U))) by exact isIso_of_reflects_iso (f.1.app (op U)) (forget C)
rw [isIso_iff_bijective]
apply app_bijective_of_stalkFunctor_map_bijective
intro x hx
apply (isIso_iff_bijective _).mp
exact Functor.map_isIso (forget C) ((stalkFunctor C (⟨x, hx⟩ : U).1).map f.1)
