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 (Presheaf C X) C
Stalks are functorial with respect to morphisms of presheaves over a fixed X.
Equations
Instances For
def
TopCat.Presheaf.stalk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : 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
Instances For
@[simp]
theorem
TopCat.Presheaf.stalkFunctor_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(ℱ : Presheaf C X)
(x : ↑X)
:
def
TopCat.Presheaf.germ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
:
The germ of a section of a presheaf over an open at a point of that open.
Equations
Instances For
def
TopCat.Presheaf.Γgerm
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
(x : ↑X)
:
The germ of a global section of a presheaf at a point.
Equations
Instances For
theorem
TopCat.Presheaf.germ_res
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(i : U ⟶ V)
(x : ↑X)
(hx : x ∈ U)
:
theorem
TopCat.Presheaf.germ_res_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : 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 : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(i : Opposite.op V ⟶ Opposite.op U)
(x : ↑X)
(hx : x ∈ U)
:
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 : 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 : Presheaf C X)
{U : TopologicalSpace.Opens ↑X}
{i : U ⟶ ⊤}
(x : ↑X)
(hx : x ∈ U)
:
theorem
TopCat.Presheaf.map_germ_eq_Γgerm_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : 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}
{FC : C → C → Type u_1}
{CC : C → Type u_2}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
(F : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(i : U ⟶ V)
(x : ↑X)
(hx : x ∈ U)
[CategoryTheory.ConcreteCategory C FC]
(s : CC (F.obj (Opposite.op V)))
:
(CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) s) = (CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type u_2}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
(F : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(i : Opposite.op V ⟶ Opposite.op U)
(x : ↑X)
(hx : x ∈ U)
[CategoryTheory.ConcreteCategory C FC]
(s : CC (F.obj (Opposite.op V)))
:
(CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i)) s) = (CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type u_2}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
(F : Presheaf C X)
{U : TopologicalSpace.Opens ↑X}
{i : U ⟶ ⊤}
(x : ↑X)
(hx : x ∈ U)
[CategoryTheory.ConcreteCategory C FC]
(s : CC (F.obj (Opposite.op ⊤)))
:
(CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) s) = (CategoryTheory.ConcreteCategory.hom (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 : 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₂)
:
A morphism from the stalk of F at x to some object Y is completely determined by its
composition with the germ morphisms.
theorem
TopCat.Presheaf.stalk_hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{F : Presheaf C X}
{x : ↑X}
{Y : C}
{f₁ f₂ : F.stalk x ⟶ Y}
:
f₁ = f₂ ↔ ∀ (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₂
@[simp]
theorem
TopCat.Presheaf.stalkFunctor_map_germ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{F G : Presheaf C X}
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
(f : F ⟶ G)
:
CategoryTheory.CategoryStruct.comp (F.germ U x hx) ((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 : Presheaf C X}
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
(f : F ⟶ G)
{Z : C}
(h : (stalkFunctor C x).obj G ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.germ U x hx) (CategoryTheory.CategoryStruct.comp ((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}
{FC : C → C → Type u_1}
{CC : C → Type u_2}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[CategoryTheory.ConcreteCategory C FC]
{F G : Presheaf C X}
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
(f : F ⟶ G)
(s : CC (F.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f))
((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom (G.germ U x hx))
((CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type u_2}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[CategoryTheory.ConcreteCategory C FC]
{F G : Presheaf C X}
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
(f : F ⟶ G)
(s : CC (F.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f))
((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom (G.germ U x hx))
((CategoryTheory.ConcreteCategory.hom (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 : Presheaf C X)
(x : ↑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
Instances For
@[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 : Presheaf C X)
(U : TopologicalSpace.Opens ↑Y)
(x : ↑X)
(hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U)
:
CategoryTheory.CategoryStruct.comp (((pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom f) x) hx)
(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 : Presheaf C X)
(U : TopologicalSpace.Opens ↑Y)
(x : ↑X)
(hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U)
{Z : C}
(h : F.stalk x ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom f) x) hx)
(CategoryTheory.CategoryStruct.comp (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 : Presheaf C X)
(U : TopologicalSpace.Opens ↑Y)
(x : ↑X)
(hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ U)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : CategoryTheory.ConcreteCategory C F✝]
(x✝ : CategoryTheory.ToType (((pushforward C f).obj F).obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (stalkPushforward C f F x))
((CategoryTheory.ConcreteCategory.hom
(((pushforward C f).obj F).germ U ((CategoryTheory.ConcreteCategory.hom 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}
(ℱ : Presheaf C X)
(x : ↑X)
:
stalkPushforward C (CategoryTheory.CategoryStruct.id X) ℱ x = (stalkFunctor C x).map (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}
(ℱ : Presheaf C X)
(f : X ⟶ Y)
(g : Y ⟶ Z)
(x : ↑X)
:
stalkPushforward C (CategoryTheory.CategoryStruct.comp f g) ℱ x = CategoryTheory.CategoryStruct.comp
(stalkPushforward C g ((pushforward C f).obj ℱ) ((CategoryTheory.ConcreteCategory.hom f) x))
(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 ⇑(CategoryTheory.ConcreteCategory.hom f))
(F : Presheaf C X)
(x : ↑X)
:
CategoryTheory.IsIso (stalkPushforward C f F x)
def
TopCat.Presheaf.stalkPullbackHom
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X Y : TopCat}
(f : X ⟶ Y)
(F : Presheaf C Y)
(x : ↑X)
:
The morphism ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ that factors through (f_*f⁻¹ℱ)_{f x}.
Equations
Instances For
@[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 : Presheaf C Y)
(x : ↑X)
(U : TopologicalSpace.Opens ↑Y)
(hU : (CategoryTheory.ConcreteCategory.hom f) x ∈ U)
:
CategoryTheory.CategoryStruct.comp (F.germ U ((CategoryTheory.ConcreteCategory.hom f) x) hU)
(stalkPullbackHom C f F x) = CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op U))
(((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 : Presheaf C Y)
(x : ↑X)
(U : TopologicalSpace.Opens ↑Y)
(hU : (CategoryTheory.ConcreteCategory.hom f) x ∈ U)
{Z : C}
(h : ((pullback C f).obj F).stalk x ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.germ U ((CategoryTheory.ConcreteCategory.hom f) x) hU)
(CategoryTheory.CategoryStruct.comp (stalkPullbackHom C f F x) h) = CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op U))
(CategoryTheory.CategoryStruct.comp (((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 : Presheaf C Y)
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
:
The morphism (f⁻¹ℱ)(U) ⟶ ℱ_{f(x)} for some U ∋ x.
Equations
Instances For
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 : Presheaf C Y}
(U : (TopologicalSpace.Opens ↑X)ᵒᵖ)
{φ ψ : ((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 (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) = CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) ψ))
:
theorem
TopCat.Presheaf.pullback_obj_obj_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X Y : TopCat}
{Z : C}
{f : X ⟶ Y}
{F : Presheaf C Y}
{U : (TopologicalSpace.Opens ↑X)ᵒᵖ}
{φ ψ : ((pullback C f).obj F).obj U ⟶ Z}
:
φ = ψ ↔ ∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V),
CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) = CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((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 : 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 (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).map (CategoryTheory.homOfLE hV).op)
(germToPullbackStalk C f F U x hx)) = F.germ V ((CategoryTheory.ConcreteCategory.hom 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 : 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 ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app (Opposite.op V))
(CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).map (CategoryTheory.homOfLE hV).op)
(CategoryTheory.CategoryStruct.comp (germToPullbackStalk C f F U x hx) h)) = CategoryTheory.CategoryStruct.comp (F.germ V ((CategoryTheory.ConcreteCategory.hom 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 : Presheaf C Y)
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
:
CategoryTheory.CategoryStruct.comp (germToPullbackStalk C f F U x hx) (stalkPullbackHom C f F x) = ((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 : Presheaf C Y)
(U : TopologicalSpace.Opens ↑X)
(x : ↑X)
(hx : x ∈ U)
{Z : C}
(h : ((pullback C f).obj F).stalk x ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (germToPullbackStalk C f F U x hx)
(CategoryTheory.CategoryStruct.comp (stalkPullbackHom C f F x) h) = CategoryTheory.CategoryStruct.comp (((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 : Presheaf C Y)
(V : (TopologicalSpace.Opens ↑Y)ᵒᵖ)
(x : ↑X)
(hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ Opposite.unop V)
:
CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app V)
(germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) = F.germ (Opposite.unop V) ((CategoryTheory.ConcreteCategory.hom 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 : Presheaf C Y)
(V : (TopologicalSpace.Opens ↑Y)ᵒᵖ)
(x : ↑X)
(hx : (CategoryTheory.ConcreteCategory.hom f) x ∈ Opposite.unop V)
{Z : C}
(h : F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((pushforwardPullbackAdjunction C f).unit.app F).app V)
(CategoryTheory.CategoryStruct.comp
(germToPullbackStalk C f F ((TopologicalSpace.Opens.map f).obj (Opposite.unop V)) x hx) h) = CategoryTheory.CategoryStruct.comp (F.germ (Opposite.unop V) ((CategoryTheory.ConcreteCategory.hom 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 : Presheaf C Y)
(x : ↑X)
:
The morphism (f⁻¹ℱ)ₓ ⟶ ℱ_{f(x)}.
Equations
Instances For
@[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 : Presheaf C Y)
(x : ↑X)
(V : TopologicalSpace.Opens ↑X)
(hV : x ∈ V)
:
CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).germ V x hV) (stalkPullbackInv C f F x) = 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 : Presheaf C Y)
(x : ↑X)
(V : TopologicalSpace.Opens ↑X)
(hV : x ∈ V)
{Z : C}
(h : F.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((pullback C f).obj F).germ V x hV)
(CategoryTheory.CategoryStruct.comp (stalkPullbackInv C f F x) h) = CategoryTheory.CategoryStruct.comp (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 : Presheaf C Y)
(x : ↑X)
:
The isomorphism ℱ_{f(x)} ≅ (f⁻¹ℱ)ₓ.
Equations
Instances For
noncomputable def
TopCat.Presheaf.stalkSpecializes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
{x y : ↑X}
(h : x ⤳ y)
:
If x specializes to y, then there is a natural map F.stalk y ⟶ F.stalk x.
Equations
Instances For
@[simp]
theorem
TopCat.Presheaf.germ_stalkSpecializes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
{U : TopologicalSpace.Opens ↑X}
{y : ↑X}
(hy : y ∈ U)
{x : ↑X}
(h : x ⤳ y)
:
@[simp]
theorem
TopCat.Presheaf.germ_stalkSpecializes_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : 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 : Presheaf C X)
{U : TopologicalSpace.Opens ↑X}
{y : ↑X}
(hy : y ∈ U)
{x : ↑X}
(h : x ⤳ y)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : CategoryTheory.ConcreteCategory C F✝]
(x✝ : CategoryTheory.ToType (F.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
((CategoryTheory.ConcreteCategory.hom (F.germ U y hy)) x✝) = (CategoryTheory.ConcreteCategory.hom (F.germ U x ⋯)) x✝
@[simp]
theorem
TopCat.Presheaf.stalkSpecializes_refl
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
(x : ↑X)
:
@[simp]
theorem
TopCat.Presheaf.stalkSpecializes_comp
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : 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_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
{x y z : ↑X}
(h : x ⤳ y)
(h' : y ⤳ z)
{Z : C}
(h✝ : F.stalk x ⟶ Z)
:
@[simp]
theorem
TopCat.Presheaf.stalkSpecializes_comp_apply
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
(F : Presheaf C X)
{x y z : ↑X}
(h : x ⤳ y)
(h' : y ⤳ z)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : CategoryTheory.ConcreteCategory C F✝]
(x✝ : CategoryTheory.ToType (F.stalk z))
:
(CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h')) x✝) = (CategoryTheory.ConcreteCategory.hom (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 : Presheaf C X}
(f : F ⟶ G)
{x y : ↑X}
(h : x ⤳ y)
:
CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) ((stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp ((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 : Presheaf C X}
(f : F ⟶ G)
{x y : ↑X}
(h : x ⤳ y)
{Z : C}
(h✝ : (stalkFunctor C x).obj G ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h)
(CategoryTheory.CategoryStruct.comp ((stalkFunctor C x).map f) h✝) = CategoryTheory.CategoryStruct.comp ((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 : Presheaf C X}
(f : F ⟶ G)
{x y : ↑X}
(h : x ⤳ y)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : CategoryTheory.ConcreteCategory C F✝]
(x✝ : CategoryTheory.ToType (F.stalk y))
:
(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f))
((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) x✝) = (CategoryTheory.CategoryStruct.comp ((stalkFunctor C y).map f) (G.stalkSpecializes h)) 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 : Presheaf C X)
{x y : ↑X}
(h : x ⤳ y)
:
CategoryTheory.CategoryStruct.comp (((pushforward C f).obj F).stalkSpecializes ⋯) (stalkPushforward C f F x) = CategoryTheory.CategoryStruct.comp (stalkPushforward C f F y) (F.stalkSpecializes h)
@[simp]
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 : Presheaf C X)
{x y : ↑X}
(h : x ⤳ y)
{Z : C}
(h✝ : F.stalk x ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (((pushforward C f).obj F).stalkSpecializes ⋯)
(CategoryTheory.CategoryStruct.comp (stalkPushforward C f F x) h✝) = CategoryTheory.CategoryStruct.comp (stalkPushforward C f F y)
(CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝)
@[simp]
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 : Presheaf C X)
{x y : ↑X}
(h : x ⤳ y)
{F✝ : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)}
[inst : CategoryTheory.ConcreteCategory C F✝]
(x✝ : CategoryTheory.ToType (((pushforward C f).obj F).stalk ((Hom.hom f) y)))
:
(CategoryTheory.ConcreteCategory.hom (stalkPushforward C f F x))
((CategoryTheory.ConcreteCategory.hom (((pushforward C f).obj F).stalkSpecializes ⋯)) x✝) = (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
((CategoryTheory.ConcreteCategory.hom (stalkPushforward C f F y)) x✝)
def
TopCat.Presheaf.stalkCongr
{X : TopCat}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
(F : Presheaf C X)
{x y : ↑X}
(e : Inseparable x y)
:
The stalks are isomorphic on inseparable points
Equations
Instances For
@[simp]
theorem
TopCat.Presheaf.stalkCongr_inv
{X : TopCat}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
(F : Presheaf C X)
{x y : ↑X}
(e : Inseparable x y)
:
@[simp]
theorem
TopCat.Presheaf.stalkCongr_hom
{X : TopCat}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasColimits C]
(F : Presheaf C X)
{x y : ↑X}
(e : Inseparable x y)
:
theorem
TopCat.Presheaf.germ_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
(F : 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.ToType (F.obj (Opposite.op U))}
{sV : CategoryTheory.ToType (F.obj (Opposite.op V))}
(ih : (CategoryTheory.ConcreteCategory.hom (F.map iWU.op)) sU = (CategoryTheory.ConcreteCategory.hom (F.map iWV.op)) sV)
:
(CategoryTheory.ConcreteCategory.hom (F.germ U x hxU)) sU = (CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
(F : Presheaf C X)
(x : ↑X)
(t : CategoryTheory.ToType (F.stalk x))
:
∃ (U : TopologicalSpace.Opens ↑X) (m : x ∈ U) (s : CategoryTheory.ToType (F.obj (Opposite.op U))),
(CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
(F : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(x : ↑X)
(mU : x ∈ U)
(mV : x ∈ V)
(s : CategoryTheory.ToType (F.obj (Opposite.op U)))
(t : CategoryTheory.ToType (F.obj (Opposite.op V)))
(h : (CategoryTheory.ConcreteCategory.hom (F.germ U x mU)) s = (CategoryTheory.ConcreteCategory.hom (F.germ V x mV)) t)
:
∃ (W : TopologicalSpace.Opens ↑X) (_ : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V),
(CategoryTheory.ConcreteCategory.hom (F.map iU.op)) s = (CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
{F G : Presheaf C X}
{f : F ⟶ G}
(h :
∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))))
(x : ↑X)
:
theorem
TopCat.Presheaf.germ_exist_of_isBasis
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
{B : Set (TopologicalSpace.Opens ↑X)}
(hB : TopologicalSpace.Opens.IsBasis B)
(F : Presheaf C X)
(x : ↑X)
(t : CategoryTheory.ToType (F.stalk x))
:
∃ (U : TopologicalSpace.Opens ↑X) (m : x ∈ U) (_ : U ∈ B) (s : CategoryTheory.ToType (F.obj (Opposite.op U))),
(CategoryTheory.ConcreteCategory.hom (F.germ U x m)) s = t
theorem
TopCat.Presheaf.germ_eq_of_isBasis
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
{B : Set (TopologicalSpace.Opens ↑X)}
(hB : TopologicalSpace.Opens.IsBasis B)
(F : Presheaf C X)
{U V : TopologicalSpace.Opens ↑X}
(x : ↑X)
(mU : x ∈ U)
(mV : x ∈ V)
{s : CategoryTheory.ToType (F.obj (Opposite.op U))}
{t : CategoryTheory.ToType (F.obj (Opposite.op V))}
(h : (CategoryTheory.ConcreteCategory.hom (F.germ U x mU)) s = (CategoryTheory.ConcreteCategory.hom (F.germ V x mV)) t)
:
∃ (W : TopologicalSpace.Opens ↑X) (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hWU).op)) s = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hWV).op)) t
theorem
TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
{B : Set (TopologicalSpace.Opens ↑X)}
(hB : TopologicalSpace.Opens.IsBasis B)
{F G : Presheaf C X}
{α : F ⟶ G}
(hα : ∀ U ∈ B, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))))
(x : ↑X)
:
theorem
TopCat.Presheaf.section_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
(F : Sheaf C X)
(U : TopologicalSpace.Opens ↑X)
(s t : CategoryTheory.ToType (F.val.obj (Opposite.op U)))
(h :
∀ (x : ↑X) (hx : x ∈ U),
(CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (CategoryTheory.ConcreteCategory.hom (F.presheaf.germ U x hx)) 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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F : Sheaf C X}
{G : Presheaf C X}
(f : F.val ⟶ G)
(U : TopologicalSpace.Opens ↑X)
(h : ∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f)))
:
theorem
TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F : Sheaf C X}
{G : Presheaf C X}
(f : F.val ⟶ G)
:
(∀ (x : ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f))) ↔ ∀ (U : TopologicalSpace.Opens ↑X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
(x : ↑X)
:
((Sheaf.forget C X).comp (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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
[CategoryTheory.Mono f]
(x : ↑X)
:
CategoryTheory.Mono ((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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
[∀ (x : ↑X), CategoryTheory.Mono ((stalkFunctor C x).map f.val)]
:
theorem
TopCat.Presheaf.mono_iff_stalk_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
:
theorem
TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
(U : TopologicalSpace.Opens ↑X)
(hinj : ∀ x ∈ U, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f.val)))
(hsurj :
∀ (t : CC (G.val.obj (Opposite.op U))),
∀ x ∈ U,
∃ (V : TopologicalSpace.Opens ↑X) (_ : x ∈ V) (iVU : V ⟶ U) (s :
CategoryTheory.ToType (F.val.obj (Opposite.op V))),
(CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op V))) s = (CategoryTheory.ConcreteCategory.hom (G.val.map iVU.op)) t)
:
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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
(U : TopologicalSpace.Opens ↑X)
(h : ∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f.val)))
:
theorem
TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
(U : TopologicalSpace.Opens ↑X)
(h : ∀ x ∈ U, Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map f.val)))
:
theorem
TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasColimits C]
{X : TopCat}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
(U : TopologicalSpace.Opens ↑X)
[∀ (x : ↥U), CategoryTheory.IsIso ((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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
[∀ (x : ↑X), CategoryTheory.IsIso ((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 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}
{FC : C → C → Type u_1}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[instCC : CategoryTheory.ConcreteCategory C FC]
[CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[(CategoryTheory.forget C).ReflectsIsomorphisms]
{F G : Sheaf C X}
(f : F ⟶ G)
:
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.