Stalks

For a presheaf F on a topological space X, valued in some category C, the stalk of F at the point x : X is defined as the colimit of the composition of the inclusion of categories (OpenNhds x)ᵒᵖ ⥤ (Opens X)ᵒᵖ and the functor F : (Opens X)ᵒᵖ ⥤ C. For an open neighborhood U of x, we define the map F.germ x : F.obj (op U) ⟶ F.stalk x as the canonical morphism into this colimit.

Taking stalks is functorial: For every point x : X we define a functor stalkFunctor C x, sending presheaves on X to objects of C. Furthermore, for a map f : X ⟶ Y between topological spaces, we define stalkPushforward as the induced map on the stalks (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x.

Some lemmas about stalks and germs only hold for certain classes of concrete categories. A basic property of forgetful functors of categories of algebraic structures (like MonCat, CommRingCat,...) is that they preserve filtered colimits. Since stalks are filtered colimits, this ensures that the stalks of presheaves valued in these categories behave exactly as for Type-valued presheaves. For example, in germ_exist we prove that in such a category, every element of the stalk is the germ of a section.

Furthermore, if we require the forgetful functor to reflect isomorphisms and preserve limits (as is the case for most algebraic structures), we have access to the unique gluing API and can prove further properties. Most notably, in is_iso_iff_stalk_functor_map_iso, we prove that in such a category, a morphism of sheaves is an isomorphism if and only if all of its stalk maps are isomorphisms.

See also the definition of "algebraic structures" in the stacks project: https://stacks.math.columbia.edu/tag/007L

def TopCat.Presheaf.stalkFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (x : ↑X) : CategoryTheory.Functor (TopCat.Presheaf C X) C

Stalks are functorial with respect to morphisms of presheaves over a fixed X.

Equations

• One or more equations did not get rendered due to their size.

def TopCat.Presheaf.stalk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (x : ↑X) : C

The stalk of a presheaf F at a point x is calculated as the colimit of the functor nbhds x ⥤ opens F.X ⥤ C

Equations

• ℱ.stalk x = (TopCat.Presheaf.stalkFunctor C x).obj ℱ

@[simp]

theorem TopCat.Presheaf.stalkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (x : ↑X) : (TopCat.Presheaf.stalkFunctor C x).obj ℱ = ℱ.stalk x

def TopCat.Presheaf.germ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) : F.obj (Opposite.op U) ⟶ F.stalk x

The germ of a section of a presheaf over an open at a point of that open.

Equations

• F.germ U x hx = CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp F) (Opposite.op { obj := U, property := hx })

def TopCat.Presheaf.Γgerm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) (x : ↑X) : F.obj (Opposite.op ⊤) ⟶ F.stalk x

The germ of a global section of a presheaf at a point.

Equations

• F.Γgerm x = F.germ ⊤ x True.intro

theorem TopCat.Presheaf.germ_res {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (F.map i.op) (F.germ U x hx) = F.germ V x ⋯

theorem TopCat.Presheaf.germ_res_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) {Z : C} (h : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map i.op) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (F.germ V x ⋯) h

@[simp]

theorem TopCat.Presheaf.germ_res' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (F.map i) (F.germ U x hx) = F.germ V x ⋯

A variant of germ_res with op V ⟶ op U so that the LHS is more general and simp fires more easier.

@[simp]

theorem TopCat.Presheaf.germ_res'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U) {Z : C} (h : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map i) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (F.germ V x ⋯) h

theorem TopCat.Presheaf.map_germ_eq_Γgerm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (F.map i.op) (F.germ U x hx) = F.Γgerm x

theorem TopCat.Presheaf.map_germ_eq_Γgerm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U) {Z : C} (h : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map i.op) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (F.Γgerm x) h

theorem TopCat.Presheaf.germ_res_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) [CategoryTheory.ConcreteCategory C] (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))) : (F.germ U x hx) ((F.map i.op) s) = (F.germ V x ⋯) s

theorem TopCat.Presheaf.germ_res_apply' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U) [CategoryTheory.ConcreteCategory C] (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))) : (F.germ U x hx) ((F.map i) s) = (F.germ V x ⋯) s

theorem TopCat.Presheaf.Γgerm_res_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U) [CategoryTheory.ConcreteCategory C] (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op ⊤))) : (F.germ U x hx) ((F.map i.op) s) = (F.Γgerm x) s

theorem TopCat.Presheaf.stalk_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x : ↑X} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y} (ih : ∀ (U : TopologicalSpace.Opens ↑X) (hxU : x ∈ U), CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₁ = CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₂) : f₁ = f₂

A morphism from the stalk of F at x to some object Y is completely determined by its composition with the germ morphisms.

@[simp]

theorem TopCat.Presheaf.stalkFunctor_map_germ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) : CategoryTheory.CategoryStruct.comp (F.germ U x hx) ((TopCat.Presheaf.stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (G.germ U x hx)

@[simp]

theorem TopCat.Presheaf.stalkFunctor_map_germ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) {Z : C} (h : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.germ U x hx) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (G.germ U x hx) h)

theorem TopCat.Presheaf.stalkFunctor_map_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))) : ((TopCat.Presheaf.stalkFunctor C x).map f) ((F.germ U x hx) s) = (G.germ U x hx) ((f.app (Opposite.op U)) s)

@[simp]

theorem TopCat.Presheaf.stalkFunctor_map_germ_apply' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G) (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))) : ((TopCat.Presheaf.stalkFunctor C x).map f) ((F.germ U x hx) s) = (G.germ U x hx) ((f.app (Opposite.op U)) s)

def TopCat.Presheaf.stalkPushforward (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) (x : ↑X) : ((TopCat.Presheaf.pushforward C f).obj F).stalk (f x) ⟶ F.stalk x

For a presheaf F on a space X, a continuous map f : X ⟶ Y induces a morphisms between the stalk of f _ * F at f x and the stalk of F at x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.stalkPushforward_germ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X) (hx : f x ∈ U) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).germ U (f x) hx) (TopCat.Presheaf.stalkPushforward C f F x) = F.germ ((TopologicalSpace.Opens.map f).obj U) x hx

@[simp]

theorem TopCat.Presheaf.stalkPushforward_germ_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X) (hx : f x ∈ U) {Z : C} (h : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).germ U (f x) hx) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F x) h) = CategoryTheory.CategoryStruct.comp (F.germ ((TopologicalSpace.Opens.map f).obj U) x hx) h

@[simp]

theorem TopCat.Presheaf.stalkPushforward_germ_apply (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) (x : ↑X) (hx : f x ∈ U) [inst : CategoryTheory.ConcreteCategory C] (x✝ : (CategoryTheory.forget C).obj (((TopCat.Presheaf.pushforward C f).obj F).obj (Opposite.op U))) : (TopCat.Presheaf.stalkPushforward C f F x) ((((TopCat.Presheaf.pushforward C f).obj F).germ U (f x) hx) x✝) = (F.germ ((TopologicalSpace.Opens.map f).obj U) x hx) x✝

@[simp]

theorem TopCat.Presheaf.stalkPushforward.id (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (x : ↑X) : TopCat.Presheaf.stalkPushforward C (CategoryTheory.CategoryStruct.id X) ℱ x = (TopCat.Presheaf.stalkFunctor C x).map (TopCat.Presheaf.Pushforward.id ℱ).hom

@[simp]

theorem TopCat.Presheaf.stalkPushforward.comp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y Z : TopCat} (ℱ : TopCat.Presheaf C X) (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : TopCat.Presheaf.stalkPushforward C (CategoryTheory.CategoryStruct.comp f g) ℱ x = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C g ((TopCat.Presheaf.pushforward C f).obj ℱ) (f x)) (TopCat.Presheaf.stalkPushforward C f ℱ x)

theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑f) (F : TopCat.Presheaf C X) (x : ↑X) : CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)

@[deprecated TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing]

theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isOpenEmbedding (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑f) (F : TopCat.Presheaf C X) (x : ↑X) : CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)

Alias of TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing.

@[deprecated TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing]

theorem TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_openEmbedding (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑f) (F : TopCat.Presheaf C X) (x : ↑X) : CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)

Alias of TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing.

def TopCat.Presheaf.stalkPullbackHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) : F.stalk (f x) ⟶ ((TopCat.Presheaf.pullback C f).obj F).stalk x

The morphism ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ that factors through (f_*f⁻¹ℱ)_{f x}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.germ_stalkPullbackHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y) (hU : f x ∈ U) : CategoryTheory.CategoryStruct.comp (F.germ U (f x) hU) (TopCat.Presheaf.stalkPullbackHom C f F x) = CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op U)) (((TopCat.Presheaf.pullback C f).obj F).germ ((TopologicalSpace.Opens.map f).obj U) x hU)

@[simp]

theorem TopCat.Presheaf.germ_stalkPullbackHom_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y) (hU : f x ∈ U) {Z : C} (h : ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.germ U (f x) hU) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackHom C f F x) h) = CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ ((TopologicalSpace.Opens.map f).obj U) x hU) h)

def TopCat.Presheaf.germToPullbackStalk (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) : ((TopCat.Presheaf.pullback C f).obj F).obj (Opposite.op U) ⟶ F.stalk (f x)

The morphism (f⁻¹ℱ)(U) ⟶ ℱ_{f(x)} for some U ∋ x.

Equations

• One or more equations did not get rendered due to their size.

theorem TopCat.Presheaf.pullback_obj_obj_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {Z : C} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) {φ ψ : ((TopCat.Presheaf.pullback C f).obj F).obj U ⟶ Z} (h : ∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V), CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) = CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) ψ)) : φ = ψ

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (V : TopologicalSpace.Opens ↑Y) (hV : U ≤ (TopologicalSpace.Opens.map f).obj V) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) (TopCat.Presheaf.germToPullbackStalk C f F U x hx)) = F.germ V (f x) ⋯

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (V : TopologicalSpace.Opens ↑Y) (hV : U ≤ (TopologicalSpace.Opens.map f).obj V) {Z : C} (h : F.stalk (f x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx) h)) = CategoryTheory.CategoryStruct.comp (F.germ V (f x) ⋯) h

@[simp]

theorem TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx) (TopCat.Presheaf.stalkPullbackHom C f F x) = ((TopCat.Presheaf.pullback C f).obj F).germ U x hx

@[simp]

theorem TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) {Z : C} (h : ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F U x hx) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackHom C f F x) h) = CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ U x hx) h

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (V : (TopologicalSpace.Opens ↑Y)ᵒᵖ) (x : ↑X) (hx : f x ∈ Opposite.unop V) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app V) (TopCat.Presheaf.germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) = F.germ (Opposite.unop V) (f x) hx

@[simp]

theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (V : (TopologicalSpace.Opens ↑Y)ᵒᵖ) (x : ↑X) (hx : f x ∈ Opposite.unop V) {Z : C} (h : F.stalk (f x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforwardPullbackAdjunction C f).unit.app F).app V) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) h) = CategoryTheory.CategoryStruct.comp (F.germ (Opposite.unop V) (f x) hx) h

def TopCat.Presheaf.stalkPullbackInv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) : ((TopCat.Presheaf.pullback C f).obj F).stalk x ⟶ F.stalk (f x)

The morphism (f⁻¹ℱ)ₓ ⟶ ℱ_{f(x)}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.germ_stalkPullbackInv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (V : TopologicalSpace.Opens ↑X) (hV : x ∈ V) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ V x hV) (TopCat.Presheaf.stalkPullbackInv C f F x) = TopCat.Presheaf.germToPullbackStalk C f F V x hV

@[simp]

theorem TopCat.Presheaf.germ_stalkPullbackInv_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (V : TopologicalSpace.Opens ↑X) (hV : x ∈ V) {Z : C} (h : F.stalk (f x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj F).germ V x hV) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPullbackInv C f F x) h) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germToPullbackStalk C f F V x hV) h

def TopCat.Presheaf.stalkPullbackIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) : F.stalk (f x) ≅ ((TopCat.Presheaf.pullback C f).obj F).stalk x

The isomorphism ℱ_{f(x)} ≅ (f⁻¹ℱ)ₓ.

Equations

• TopCat.Presheaf.stalkPullbackIso C f F x = { hom := TopCat.Presheaf.stalkPullbackHom C f F x, inv := TopCat.Presheaf.stalkPullbackInv C f F x, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def TopCat.Presheaf.stalkSpecializes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) : F.stalk y ⟶ F.stalk x

If x specializes to y, then there is a natural map F.stalk y ⟶ F.stalk x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.germ_stalkSpecializes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.germ U y hy) (F.stalkSpecializes h) = F.germ U x ⋯

@[simp]

theorem TopCat.Presheaf.germ_stalkSpecializes_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.germ U y hy) (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (F.germ U x ⋯) h✝

theorem TopCat.Presheaf.germ_stalkSpecializes_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) [inst : CategoryTheory.ConcreteCategory C] (x✝ : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))) : (F.stalkSpecializes h) ((F.germ U y hy) x✝) = (F.germ U x ⋯) x✝

@[deprecated TopCat.Presheaf.germ_stalkSpecializes]

theorem TopCat.Presheaf.germ_stalkSpecializes' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.germ U y hy) (F.stalkSpecializes h) = F.germ U x ⋯

Alias of TopCat.Presheaf.germ_stalkSpecializes.

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_refl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) (x : ↑X) : F.stalkSpecializes ⋯ = CategoryTheory.CategoryStruct.id (F.stalk x)

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (F.stalkSpecializes h) = F.stalkSpecializes ⋯

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (F.stalkSpecializes ⋯) h✝

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_comp_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) [inst : CategoryTheory.ConcreteCategory C] (x✝ : (CategoryTheory.forget C).obj (F.stalk z)) : (F.stalkSpecializes h) ((F.stalkSpecializes h') x✝) = (F.stalkSpecializes ⋯) x✝

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_stalkFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) ((TopCat.Presheaf.stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (G.stalkSpecializes h)

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {Z : C} (h✝ : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h✝) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (CategoryTheory.CategoryStruct.comp (G.stalkSpecializes h) h✝)

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) [inst : CategoryTheory.ConcreteCategory C] (x✝ : (CategoryTheory.forget C).obj (F.stalk y)) : ((TopCat.Presheaf.stalkFunctor C x).map f) ((F.stalkSpecializes h) x✝) = (G.stalkSpecializes h) (((TopCat.Presheaf.stalkFunctor C y).map f) x✝)

@[simp]

theorem TopCat.Presheaf.stalkSpecializes_stalkPushforward {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯) (TopCat.Presheaf.stalkPushforward C f F x) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y) (F.stalkSpecializes h)

theorem TopCat.Presheaf.stalkSpecializes_stalkPushforward_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F x) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y) (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝)

theorem TopCat.Presheaf.stalkSpecializes_stalkPushforward_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) [inst : CategoryTheory.ConcreteCategory C] (x✝ : (CategoryTheory.forget C).obj (((TopCat.Presheaf.pushforward C f).obj F).stalk (f y))) : (TopCat.Presheaf.stalkPushforward C f F x) ((((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯) x✝) = (F.stalkSpecializes h) ((TopCat.Presheaf.stalkPushforward C f F y) x✝)

def TopCat.Presheaf.stalkCongr {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y) : F.stalk x ≅ F.stalk y

The stalks are isomorphic on inseparable points

Equations

• F.stalkCongr e = { hom := F.stalkSpecializes ⋯, inv := F.stalkSpecializes ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TopCat.Presheaf.stalkCongr_hom {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y) : (F.stalkCongr e).hom = F.stalkSpecializes ⋯

@[simp]

theorem TopCat.Presheaf.stalkCongr_inv {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X) {x y : ↑X} (e : Inseparable x y) : (F.stalkCongr e).inv = F.stalkSpecializes ⋯

theorem TopCat.Presheaf.germ_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} {x : ↑X} {hxU : x ∈ U} {hxV : x ∈ V} (W : TopologicalSpace.Opens ↑X) (hxW : x ∈ W) (iWU : W ⟶ U) (iWV : W ⟶ V) {sU : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))} {sV : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))} (ih : (F.map iWU.op) sU = (F.map iWV.op) sV) : (F.germ U x hxU) sU = (F.germ V x hxV) sV

theorem TopCat.Presheaf.germ_exist {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) (x : ↑X) (t : (CategoryTheory.forget C).obj (F.stalk x)) : ∃ (U : TopologicalSpace.Opens ↑X) (m : x ∈ U) (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))), (F.germ U x m) s = t

For presheaves valued in a concrete category whose forgetful functor preserves filtered colimits, every element of the stalk is the germ of a section.

theorem TopCat.Presheaf.germ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (x : ↑X) (mU : x ∈ U) (mV : x ∈ V) (s : (CategoryTheory.forget C).obj (F.obj (Opposite.op U))) (t : (CategoryTheory.forget C).obj (F.obj (Opposite.op V))) (h : (F.germ U x mU) s = (F.germ V x mV) t) : ∃ (W : TopologicalSpace.Opens ↑X) (_ : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V), (F.map iU.op) s = (F.map iV.op) t

theorem TopCat.Presheaf.stalkFunctor_map_injective_of_app_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {F G : TopCat.Presheaf C X} (f : F ⟶ G) (h : ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(f.app (Opposite.op U))) (x : ↑X) : Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f)

theorem TopCat.Presheaf.section_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] (F : TopCat.Sheaf C X) (U : TopologicalSpace.Opens ↑X) (s t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op U))) (h : ∀ (x : ↑X) (hx : x ∈ U), (F.presheaf.germ U x hx) s = (F.presheaf.germ U x hx) t) : s = t

Let F be a sheaf valued in a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then two sections who agree on every stalk must be equal.

theorem TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.val ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f)) : Function.Injective ⇑(f.app (Opposite.op U))

theorem TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F : TopCat.Sheaf C X} {G : TopCat.Presheaf C X} (f : F.val ⟶ G) : (∀ (x : ↑X), Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f)) ↔ ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(f.app (Opposite.op U))

instance TopCat.Presheaf.stalkFunctor_preserves_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] (x : ↑X) : ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x)).PreservesMonomorphisms

theorem TopCat.Presheaf.stalk_mono_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [CategoryTheory.Mono f] (x : ↑X) : CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)

theorem TopCat.Presheaf.mono_of_stalk_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)] : CategoryTheory.Mono f

theorem TopCat.Presheaf.mono_iff_stalk_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) : CategoryTheory.Mono f ↔ ∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.val)

theorem TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (hinj : ∀ x ∈ U, Function.Injective ⇑((TopCat.Presheaf.stalkFunctor C x).map f.val)) (hsurj : ∀ (t : (CategoryTheory.forget C).obj (G.val.obj (Opposite.op U))), ∀ x ∈ U, ∃ (V : TopologicalSpace.Opens ↑X) (_ : x ∈ V) (iVU : V ⟶ U) (s : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))), (f.val.app (Opposite.op V)) s = (G.val.map iVU.op) t) : Function.Surjective ⇑(f.val.app (Opposite.op U))

For surjectivity, we are given an arbitrary section t and need to find a preimage for it. We claim that it suffices to find preimages locally. That is, for each x : U we construct a neighborhood V ≤ U and a section s : F.obj (op V)) such that f.app (op V) s and t agree on V.

theorem TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Bijective ⇑((TopCat.Presheaf.stalkFunctor C x).map f.val)) : Function.Surjective ⇑(f.val.app (Opposite.op U))

theorem TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) (h : ∀ x ∈ U, Function.Bijective ⇑((TopCat.Presheaf.stalkFunctor C x).map f.val)) : Function.Bijective ⇑(f.val.app (Opposite.op U))

theorem TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) (U : TopologicalSpace.Opens ↑X) [∀ (x : ↥U), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C ↑x).map f.val)] : CategoryTheory.IsIso (f.val.app (Opposite.op U))

theorem TopCat.Presheaf.isIso_of_stalkFunctor_map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)] : CategoryTheory.IsIso f

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 TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {F G : TopCat.Sheaf C X} (f : F ⟶ G) : CategoryTheory.IsIso f ↔ ∀ (x : ↑X), CategoryTheory.IsIso ((TopCat.Presheaf.stalkFunctor C x).map f.val)

Let F and G be sheaves valued in a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then a morphism f : F ⟶ G is an isomorphism if and only if all of its stalk maps are isomorphisms.