Sheaves and Lean

X
functions glue uniquely

A presheaf F is a rule that assigns

such that

def presheaf (X : Top) := opens(X)ᵒᵖ  Type
class category (obj : Type u) : Type (max u (v+1)) :=
(hom : obj obj Type v) (infixr ` `:10 := hom)
(id : Π X : obj, X X) (notation `𝟙` := id)
(comp : Π {X Y Z : obj}, (X Y) (Y Z) (X Z)) (infixr ` `:80 := comp)
(id_comp' : {X Y : obj} (f : X Y), 𝟙 X f = f . obviously) (comp_id' : {X Y : obj} (f : X Y), f 𝟙 Y = f . obviously) (assoc' : {W X Y Z : obj} (f : W X) (g : X Y) (h : Y Z), (f g) h = f (g h) . obviously)
structure functor (C : Type u₁) [category.{v₁} C]
                  (D : Type u₂) [category.{v₂} D] :
  Type (max u₁ v₁ u₂ v₂) :=
(obj       : C  D)
(map       : Π {X Y : C}, (X  Y)  ((obj X)  (obj Y)))
(map_id'   :  (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' :  {X Y Z : C} (f : X  Y) (g : Y  Z),
             map (f  g) = (map f)  (map g) . obviously)
instance types : large_category (Type u) :=
{ hom     := λ a b, (a  b),
  id      := λ a, id,
  comp    := λ _ _ _ f g, g  f }
variables {C : Type u₁} [𝒞 : category.{v₁} C]
include 𝒞

def yoneda : C  ((Cᵒᵖ)  (Type v₁)) := 
{ obj := λ X,
  { obj := λ Y : C, Y  X,
    map := λ Y Y' f g, f  g,
    map_comp' :=
    begin
      intros X_1 Y Z f g,
      ext1, dsimp at *,
      erw [category.assoc]
    end,
    map_id' :=
    begin
      intros X_1,
      ext1, dsimp at *,
      erw [category.id_comp]
    end },
map := λ X X' f, { app := λ Y g, g  f } }
def yoneda_2 : C  ((Cᵒᵖ)  (Type v₁)) := 
{ obj := λ X,
  { obj := λ Y : C, Y  X,
    map := λ Y Y' f g, f  g },
  map := λ X X' f, { app := λ Y g, g  f } }
def yoneda_3 : C  ((Cᵒᵖ)  (Type v₁)) := ƛ X, ƛ Y : C, Y  X.

So, what is a sheaf?

Let U_i ⊆ X be open sets that cover U ⊆ X.

Consider the following set

F'(U) = { s  Π_i F(U_i) | r(s_i) = r(s_j),  i,j }

There is a canonical map F(U) F'(U)

A presheaf F is called a sheaf if this canonical map is bijective for every U ⊆ X and every cover of U.

sheaves of (commutative) groups/rings
topologies on categories
def covering_family (U : X) : Type u := set (over.{u} U)
structure coverage :=
(covers   : Π (U : X), set (covering_family U))
(property :  {U V : X} (g : V  U),
             f  covers U,  h  covers V,
             Vj  (h : set _),  (Ui  f),
            nonempty $ ((over.map g).obj Vj)  Ui)
class site (X : Type u) extends category.{u} X :=
(coverage : coverage X)
def sheaf (X : Type u) [𝒳 : site X] :=
{ F : presheaf X // nonempty (site.sheaf_condition F) }
https://github.com/leanprover-community/mathlib/tree/sheaf-2