@[reducible, inline]
abbrev
SheafDefinitions.Presheaf
(J : Type u_1)
[CategoryTheory.Category.{u_3, u_1} J]
(C : Type u_2)
[CategoryTheory.Category.{u_4, u_2} C]
:
Type (max u_3 u_4 u_1 u_2)
A presheaf on a category J with values in C is a contravariant functor
Jᵒᵖ ⥤ C.
Instances For
def
SheafDefinitions.pushforwardPresheaf
{J : Type u_1}
{K : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_5, u_2} K]
{C : Type u_3}
[CategoryTheory.Category.{u_6, u_3} C]
(u : CategoryTheory.Functor J K)
(F : Presheaf K C)
:
Presheaf J C
Pushforward of a presheaf along a covariant functor u : J ⥤ K: precompose
with u.op to obtain a presheaf on J from one on K.
Instances For
@[implicit_reducible]
noncomputable instance
SheafDefinitions.presheafAbelian
(C : Type u_1)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
:
The category of presheaves with values in an abelian category is abelian.
def
SheafDefinitions.IsLocallyFree
{X : Type u_1}
[TopologicalSpace X]
(O : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ CommRingCat)
(M : TopologicalSpace.Opens X → Type u_2)
[(U : TopologicalSpace.Opens X) → AddCommGroup (M U)]
[(U : TopologicalSpace.Opens X) → Module (↑(O.obj (Opposite.op U))) (M U)]
(n : ℕ)
:
An O-module is locally free of rank n if there is an open cover
{U_i} of X such that each restriction M(U_i) is a free O(U_i)-module of
rank n.
Instances For
theorem
SheafDefinitions.free_isLocallyFree
{X : Type u_1}
[TopologicalSpace X]
(O : CategoryTheory.Functor (TopologicalSpace.Opens X)ᵒᵖ CommRingCat)
(M : TopologicalSpace.Opens X → Type u_2)
[(U : TopologicalSpace.Opens X) → AddCommGroup (M U)]
[(U : TopologicalSpace.Opens X) → Module (↑(O.obj (Opposite.op U))) (M U)]
(n : ℕ)
[hfree : Module.Free (↑(O.obj (Opposite.op ⊤))) (M ⊤)]
(hrank : Module.finrank (↑(O.obj (Opposite.op ⊤))) (M ⊤) = n)
:
IsLocallyFree O M n
A globally free sheaf of rank n is locally free of rank n: take the
trivial one-element cover by the whole space.