gluing functions

Stream: maths

[Kenny Lau]

import topology.opens

universes v u
open topological_space lattice

variables (X : Type u) [topological_space X]

set_option old_structure_cmd true

structure presheaf : Type (max u (v+1)) :=
(F : ∀ U : opens X, Type v)
(res : Π U V : opens X, V ≤ U → F U → F V)
(res_self : ∀ U x, res U U (le_refl U) x = x)
(res_res : ∀ U V W HWV HVU x, res V W HWV (res U V HVU x) = res U W (le_trans HWV HVU) x)

variables {X}
structure covering (U : opens X) : Type (u+1) :=
(ι : Type u)
(map : ι → opens X)
(map_le : ∀ i, map i ≤ U)
(exists_of_mem : ∀ x ∈ U, ∃ i, x ∈ map i)
variables (X)

structure sheaf extends presheaf.{v} X : Type (max u (v+1)) :=
(locality : ∀ U : opens X, ∀ s t : F U, ∀ OC : covering U,
  (∀ i : OC.ι, res U (OC.map i) (OC.map_le i) s = res U (OC.map i) (OC.map_le i) t) → s = t)
(gluing : ∀ U : opens X, ∀ OC : covering U, ∀ S : Π i : OC.ι, F (OC.map i),
  (∀ i j : OC.ι, res (OC.map i) (OC.map i ⊓ OC.map j) inf_le_left (S i) =
    res (OC.map j) (OC.map i ⊓ OC.map j) inf_le_right (S j)) →
  ∃ s : F U, ∀ i : OC.ι, res U (OC.map i) (OC.map_le i) s = S i)

def Func (Y : Type v) : sheaf.{(max u v) u} X :=
{ F := λ U, U → Y,
  res := λ U V HVU s v, s ⟨v.1, HVU v.2⟩,
  res_self := λ _ _, funext $ λ ⟨_, _⟩, rfl,
  res_res := λ _ _ _ _ _ _, rfl,
  locality := λ U s t OC H, funext $ λ ⟨u, hu⟩,
    let ⟨i, hui⟩ := OC.exists_of_mem u hu in
    have _ := congr_fun (H i) ⟨u, hui⟩, this,
  gluing := λ U OC S H, ⟨λ u, S (classical.some $ OC.exists_of_mem u.1 u.2)
      ⟨u.1, classical.some_spec $ OC.exists_of_mem u.1 u.2⟩,
    λ i, funext $ λ ⟨u, hu⟩, have _ := congr_fun (H i $ classical.some $ OC.exists_of_mem u $ OC.map_le i hu)
      ⟨u, hu, classical.some_spec $ OC.exists_of_mem u $ OC.map_le i hu⟩, this.symm⟩ }

[Johan Commelin]

@Kenny Lau That looks great!!

[Johan Commelin]

Maybe we should forget about sites for the moment. I do want to use functors though. I don't see any reason why you would handroll your own presheaves if their definition is defeq to functors (up to iota/eta for records [I always forget which Greek letter I need to invoke]).

[Kenny Lau]

namespace opens
def covering_res (U V : opens X) (H : V ⊆ U) (OC : covering U) : covering V :=
{ ι := OC.ι,
  map := λ i : OC.ι, V ⊓ OC.map i,
  map_le := λ _, inf_le_left,
  exists_of_mem := λ x hxV, let ⟨i, hi⟩ := OC.exists_of_mem _ (H hxV) in ⟨i, hxV, hi⟩ }
end opens

structure subpresheaf (F : presheaf.{v} X) : Type (max u v) :=
(to_set : Π U : opens X, set (F U))
(res_mem_to_set : ∀ {U V : opens X} (HVU : V ⊆ U) {s : F U}, s ∈ to_set U → F.res U V HVU s ∈ to_set V)

namespace subpresheaf

instance (F : presheaf.{v} X) : has_coe_to_fun (subpresheaf F) :=
⟨_, to_set⟩

instance (F : presheaf.{v} X) : partial_order (subpresheaf F) :=
partial_order.lift to_set (λ ⟨x, hx⟩ ⟨y, hy⟩, mk.inj_eq.mpr) infer_instance

def to_subsheaf {F : presheaf.{v} X} (S : subpresheaf F) : subpresheaf F :=
{ to_set := λ U, { x | ∃ OC : covering.{u} U, ∀ i : OC.ι, F.res U (OC.map i) (OC.map_le i) x ∈ S (OC.map i) },
  res_mem_to_set := λ U V HVU x ⟨OC, hx⟩, ⟨opens.covering_res U V HVU OC,
    λ i, have _ ∈ S ((opens.covering_res U V HVU OC).map i) := S.res_mem_to_set (set.inter_subset_right _ _) (hx i),
    by rwa F.res_res at this ⊢⟩ }

theorem le_to_subsheaf {F : presheaf.{v} X} (S : subpresheaf F) : S ≤ S.to_subsheaf :=
λ U x hx, ⟨{ ι := punit, map := λ _, U, map_le := λ _, le_refl U, exists_of_mem := λ x hxU, ⟨punit.star, hxU⟩ },
λ i, by rwa F.res_self⟩

def to_presheaf {F : presheaf.{v} X} (S : subpresheaf F) : presheaf X :=
{ F := λ U, S U,
  res := λ U V HVU x, ⟨F.res U V HVU x.1, S.2 HVU x.2⟩,
  res_self := λ U x, subtype.eq $ F.res_self U x.1,
  res_res := λ U V W HWV HVU x, subtype.eq $ F.res_res U V W HWV HVU x.1 }

end subpresheaf

structure subsheaf (F : presheaf.{v} X) extends subpresheaf F :=
(mem_of_res_mem : ∀ {U : opens X}, ∀ {s : F U}, ∀ OC : covering.{u} U,
  (∀ i : OC.ι, F.res U (OC.map i) (OC.map_le i) s ∈ to_set (OC.map i)) → s ∈ to_set U)

namespace subsheaf

def to_sheaf {F : sheaf.{v} X} (S : subsheaf F.to_presheaf) : sheaf X :=
{ locality := λ U ⟨s, hs⟩ ⟨t, ht⟩ OC H, subtype.eq $ F.locality U s t OC $ λ i,
    have _ := congr_arg subtype.val (H i), this,
  gluing := λ U OC ss H, let ⟨s, hs⟩ := F.gluing U OC (λ i, (ss i).1)
      (λ i j, have _ := congr_arg subtype.val (H i j), this) in
    ⟨⟨s, S.mem_of_res_mem OC (λ i, show F.res _ _ _ _ ∈ _, by rw hs; exact (ss i).2)⟩,
    λ i, subtype.eq $ (hs i)⟩,
  .. S.to_subpresheaf.to_presheaf }

end subsheaf

def continuous_subsheaf (Y : Type v) [topological_space Y] : subsheaf (Func X Y).to_presheaf :=
{ to_set := λ U, { f | continuous f },
  res_mem_to_set := λ U V HVU s hs, hs.comp $ continuous_induced_rng continuous_induced_dom,
  mem_of_res_mem := λ U s OC H, continuous_iff_continuous_at.2 $ λ ⟨x, hxU⟩,
    let ⟨i, hi⟩ := OC.exists_of_mem x hxU in λ V HV,
    let ⟨t, htV, ⟨u, hu, hut⟩, hxt⟩ := mem_nhds_sets_iff.1 (continuous_iff_continuous_at.1 (H i) ⟨x, hi⟩ HV) in
    mem_nhds_sets_iff.2 ⟨subtype.val ⁻¹' (subtype.val '' t),
      by rintros ⟨y, hy⟩ ⟨z, hzt, hzy⟩; dsimp only at hzy; subst hzy; exact htV hzt,
      ⟨u ∩ OC.map i, is_open_inter hu (OC.map i).2, by rw [← hut, subtype.image_preimage_val]; refl⟩,
      ⟨x, hi⟩, hxt, rfl⟩ }

[Kenny Lau]

namespace subpresheaf

variables {X} (F : presheaf X)

instance : has_sup (subpresheaf F) :=
⟨λ S T, ⟨λ U, S U ∪ T U, λ U V HVU s, or.imp (S.2 HVU) (T.2 HVU)⟩⟩

instance : has_inf (subpresheaf F) :=
⟨λ S T, ⟨λ U, S U ∩ T U, λ U V HVU s, and.imp (S.2 HVU) (T.2 HVU)⟩⟩

instance : has_Sup (subpresheaf F) :=
⟨λ SS, ⟨λ U, ⋃ S ∈ SS, to_set S U, λ U V HVU s hs,
let ⟨S, HS, hsS⟩ := set.mem_bUnion_iff.1 hs in set.mem_bUnion_iff.2 ⟨S, HS, S.2 HVU hsS⟩⟩⟩

instance : has_Inf (subpresheaf F) :=
⟨λ SS, ⟨λ U, ⋂ S ∈ SS, to_set S U, λ U V HVU s hs,
set.mem_bInter $ λ S HS, S.2 HVU $ set.mem_bInter_iff.1 hs S HS⟩⟩

instance : has_top (subpresheaf F) :=
⟨⟨λ U, set.univ, λ U V HVU s _, trivial⟩⟩

instance : has_bot (subpresheaf F) :=
⟨⟨λ U, ∅, λ U V HVU s, false.elim⟩⟩

instance subpresheaf.complete_lattice (F : presheaf X) : complete_lattice (subpresheaf F) :=
{ le_sup_left := λ S T U, set.subset_union_left _ _,
  le_sup_right := λ S T U, set.subset_union_right _ _,
  sup_le := λ S1 S2 S3 H13 H23 U, set.union_subset (H13 U) (H23 U),
  inf_le_left := λ S T U, set.inter_subset_left _ _,
  inf_le_right := λ S T U, set.inter_subset_right _ _,
  le_inf := λ S1 S2 S3 H12 H13 U, set.subset_inter (H12 U) (H13 U),
  le_top := λ S U, set.subset_univ _,
  bot_le := λ S U, set.empty_subset _,
  le_Sup := λ SS S HS U, set.subset_bUnion_of_mem HS,
  Sup_le := λ SS S HS U, set.bUnion_subset $ λ T HT, HS T HT U,
  Inf_le := λ SS S HS U, set.bInter_subset_of_mem HS,
  le_Inf := λ SS S HS U, set.subset_bInter $ λ T HT, HS T HT U,
  .. subpresheaf.partial_order F,
  .. subpresheaf.lattice.has_sup F,
  .. subpresheaf.lattice.has_inf F,
  .. subpresheaf.lattice.has_Sup F,
  .. subpresheaf.lattice.has_Inf F,
  .. subpresheaf.lattice.has_top F,
  .. subpresheaf.lattice.has_bot F }

end subpresheaf

[Kenny Lau]

namespace subsheaf

variables {X} (F : presheaf X)

instance (F : presheaf.{v} X) : has_coe_to_fun (subsheaf F) :=
⟨_, to_set⟩

instance (F : presheaf.{v} X) : partial_order (subsheaf F) :=
partial_order.lift to_set (λ ⟨x, hx1, hx2⟩ ⟨y, hy1, hy2⟩, mk.inj_eq.mpr) infer_instance

instance : has_inf (subsheaf F) :=
⟨λ S T, ⟨λ U, S U ∩ T U, λ U V HVU s, and.imp (S.2 HVU) (T.2 HVU),
  λ U s OC H, ⟨S.3 OC $ λ i, (H i).1, T.3 OC $ λ i, (H i).2⟩⟩⟩

instance : has_Inf (subsheaf F) :=
⟨λ SS, ⟨λ U, ⋂ S ∈ SS, to_set S U, λ U V HVU s hs,
set.mem_bInter $ λ S HS, S.2 HVU $ set.mem_bInter_iff.1 hs S HS,
λ U s OC H, set.mem_bInter $ λ S HS, S.3 OC $ λ i, set.mem_bInter_iff.1 (H i) S HS⟩⟩

instance : has_top (subsheaf F) :=
⟨⟨λ U, set.univ, λ U V HVU s _, trivial, λ _ _ _ _, trivial⟩⟩

instance subsheaf.semilattice_inf_top (F : presheaf X) : semilattice_inf_top (subsheaf F) :=
{ inf_le_left := λ S T U, set.inter_subset_left _ _,
  inf_le_right := λ S T U, set.inter_subset_right _ _,
  le_inf := λ S1 S2 S3 H12 H13 U, set.subset_inter (H12 U) (H13 U),
  le_top := λ S U, set.subset_univ _,
  .. subsheaf.partial_order F,
  .. subsheaf.lattice.has_inf F,
  .. subsheaf.lattice.has_Inf F,
  .. subsheaf.lattice.has_top F }

theorem Inf_le (SS : set (subsheaf F)) (S : subsheaf F) (HS : S ∈ SS) : Inf SS ≤ S :=
λ U, set.bInter_subset_of_mem HS

theorem le_Inf (SS : set (subsheaf F)) (S : subsheaf F) (HS : ∀ b ∈ SS, S ≤ b) : S ≤ Inf SS :=
λ U, set.subset_bInter $ λ T HT, HS T HT U

end subsheaf

[Kenny Lau]

def section_subsheaf (Y : Type v) (π : Y → X) : subsheaf (Func X Y).to_presheaf :=
{ to_set := λ U, { s | ∀ u : U, π (s u) = u.1 },
  res_mem_to_set := λ U V HVU s hs ⟨v, hv⟩, hs ⟨v, _⟩,
  mem_of_res_mem := λ U s OC H ⟨u, hu⟩, let ⟨i, hi⟩ := OC.exists_of_mem u hu in H i ⟨u, hi⟩ }

[Kenny Lau]

def continuous_section_subsheaf (Y : Type v) [topological_space Y] (π : Y → X) : subsheaf (Func X Y).to_presheaf :=
continuous_subsheaf Y ⊓ section_subsheaf Y π

[Johan Commelin]

@Kenny Lau What is your objection against using functors on (opens X)^op?

[Kenny Lau]

the large amount of unop required

[Johan Commelin]

@Scott Morrison Should we make a cv_functor?

[Johan Commelin]

@Kenny Lau Given that you already have this covering class. How hard do you think it is to generalise to sites?

[Johan Commelin]

Do you see particular troubles on the road?

[Kenny Lau]

I dont know

[Scott Morrison]

cv_functor feels like we’d be unnecessarily multiplying entities.

[Scott Morrison]

I’m not so sure there is so much unopened required. This is certainly the way I felt at first when you guys insists I couldn’t just define opens X as what is now (opens X)^op`, but it never got particularly bad.

[Scott Morrison]

I don’t like essentially redefining functors here. It’s a recipe for duplication and confusion.

[Johan Commelin]

Is there a coordinated approach to navigate ourselves out of this mess? We've been talking about sheafy things for more than a year, and mathlib still doesn't have them.
I'm fine with ignoring sites for the moment. There is loads of interesting stuff to say about sheaves on topological spaces.

[Kenny Lau]

structure germ (F : presheaf X) (x : X) :=
(U : opens X)
(hxU : x ∈ U)
(s : F U)

namespace germ

variables (F : presheaf X) (x : X)

instance : setoid (germ F x) :=
{ r := λ g1 g2, ∃ U : opens X, x ∈ U ∧ ∃ H1 : U ≤ g1.U, ∃ H2 : U ≤ g2.U, F.res g1.U U H1 g1.s = F.res g2.U U H2 g2.s,
  iseqv := ⟨λ g1, ⟨g1.U, g1.2, le_refl _, le_refl _, rfl⟩,
    λ g1 g2 ⟨U, hx, H1, H2, H3⟩, ⟨U, hx, H2, H1, H3.symm⟩,
    λ g1 g2 g3 ⟨U, hxU, H1, H2, H3⟩ ⟨V, hxV, H4, H5, H6⟩,
      ⟨U ⊓ V, ⟨hxU, hxV⟩, le_trans inf_le_left H1, le_trans inf_le_right H5,
      calc  F.res g1.U (U ⊓ V) (le_trans inf_le_left H1) g1.s
          = F.res U (U ⊓ V) inf_le_left (F.res g1.U U H1 g1.s) : by rw F.res_res
      ... = F.res U (U ⊓ V) inf_le_left (F.res g2.U U H2 g2.s) : by rw H3
      ... = F.res V (U ⊓ V) inf_le_right (F.res g2.U V H4 g2.s) : by rw [F.res_res, F.res_res]
      ... = F.res V (U ⊓ V) inf_le_right (F.res g3.U V H5 g3.s) : by rw H6
      ... = F.res g3.U (U ⊓ V) (le_trans inf_le_right H5) g3.s : by rw F.res_res⟩⟩ }

end germ

def stalk (F : presheaf X) (x : X) :=
quotient (germ.setoid F x)

def to_stalk (F : presheaf X) (x : X) (U : opens X) (hxU : x ∈ U) (s : F U) : stalk F x :=
⟦⟨U, hxU, s⟩⟧

theorem to_stalk_res (F : presheaf X) (x : X) (U V : opens X) (hxV : x ∈ V) (HVU : V ≤ U) (s : F U) :
  to_stalk F x V hxV (F.res U V HVU s) = to_stalk F x U (HVU hxV) s :=
quotient.sound ⟨V, hxV, le_refl V, HVU, F.res_res _ _ _ _ _ _⟩

def espace_etale (F : presheaf X) : Type (max u v) :=
Σ x : X, stalk F x

instance (F : presheaf X) : topological_space (espace_etale F) :=
{ is_open := λ S, ∀ x ∈ S, ∃ U : opens X, ∃ hxU : sigma.fst x ∈ U, ∃ s : F U, to_stalk F x.1 U hxU s = x.2 ∧
    ∀ p : X, ∀ hpU : p ∈ U, (⟨p, to_stalk F p U hpU s⟩ : espace_etale F) ∈ S,
  is_open_univ := λ ⟨p, g⟩ _, quotient.induction_on g $ λ ⟨U, hpU, s⟩, ⟨U, hpU, s, rfl, λ _ _, trivial⟩,
  is_open_inter := λ S T HS HT x hxST, let ⟨U, hxU, s, hsx, hs⟩ := HS x hxST.1,
    ⟨V, hxV, t, htx, ht⟩ := HT x hxST.2, ⟨W, hxW, HWU, HWV, h⟩ := quotient.exact (hsx.trans htx.symm) in
    ⟨W, hxW, F.res U W HWU s, by rw to_stalk_res; exact hsx,
    λ q hqW, ⟨by rw to_stalk_res; apply hs, by rw [h, to_stalk_res]; apply ht⟩⟩,
  is_open_sUnion := λ SS H x hx, let ⟨t, htSS, hxt⟩ := set.mem_sUnion.1 hx,
    ⟨U, hxU, s, hsx, hs⟩ := H t htSS x hxt in ⟨U, hxU, s, hsx, λ p hpU, set.mem_sUnion_of_mem (hs p hpU) htSS⟩ }

def of_espace_etale (F : presheaf X) (x : espace_etale F) : X :=
x.1

theorem continuous_of_espace_etale (F : presheaf X) : continuous (of_espace_etale F) :=
λ U HU ⟨p, g⟩ hpU, quotient.induction_on g $ λ ⟨V, hpV, s⟩,
⟨⟨U, HU⟩ ⊓ V, ⟨hpU, hpV⟩, F.res V _ inf_le_right s, to_stalk_res _ _ _ _ _ _ _, λ q hqUV, hqUV.1⟩

[Johan Commelin]

Kenny, you realise that presheaves and stalks are already in mathlib?

[Kevin Buzzard]

But are those presheaves usable? Kenny has glued sheaves of rings and proved the universal property. Last time I talked to Scott he was still trying to work out the best way to define a sheaf. The schemes project has a definition of presheaf which is not the same as the one in mathlib but we are miles ahead of mathlib and it is my firm belief that because the mathlib definition is not the best way of doing sheaves in dependent type theory, that gap is only set to grow.

[Kevin Buzzard]

To define products of schemes we do it in the affine case and then glue the top space and glue the sheaves of rings. We need products and pullbacks etc to define cohomology. We have a system that works and is moving fast. You have a definition of a presheaf. Some serious decisions need to be made.

[Kevin Buzzard]

I tried to state the construction of glueing presheaves of types using the mathlib language and it was a nightmare.

[Johan Commelin]

I really don't understand this. Your definition of a presheaf is a special case of a contravariant functor. The mathlib definition is the same. I cannot see where the trouble lies.

[Johan Commelin]

Sure, with the sheaf condition there might be trouble.

[Johan Commelin]

I would very much like to see PR's going from the schemes project to mathlib. But I haven't seen any PR's apart from a 20 line thingy on kernels of ring morphisms.

[Johan Commelin]

And I'm not saying that we have to use the category lib per se. But (i) avoiding duplication seems a good thing, and (ii) we'll need categorical machinery to build machines for cohomology theories. Unless we don't want those machines.

[Kevin Buzzard]

I agree that we'll have to the the categorical language in the end.

[Kevin Buzzard]

@Kenny Lau are you going to PR glueing sheaves of rings?

[Kevin Buzzard]

Sure, with the sheaf condition there might be trouble.

We had no trouble at all with the sheaf condition. What is the trouble you are having? You say your presheaves are "the same" as ours but then sheaves might be trouble for you, and not for us?

[Johan Commelin]

I mean that if you want to state the sheaf condition using categorical language, saying that some diagram is an equalizer.

[Johan Commelin]

Kenny said he didn't like the unops that our definition gave. Ok, I understand that. But that's life.

[Johan Commelin]

We have lot's of annoying little things popping up in our goals that you can't see in maths.

[Johan Commelin]

I don't like all the to_additive statements in mathlib. They are complete stupid. But it is the best solution we have.

[Johan Commelin]

Kenny and Mario did a wonderful job with the gluing of sheaves thing. Now it should go to mathlib, instead of rot away on a Zulip thread.

[Kevin Buzzard]

But they use a different definition of presheaf to the one in mathlib. I am not clear about how you want to take this forward.

[Johan Commelin]

Is it different from the one Kenny is using in this thread? Because the one in this thread is only syntactically different from the one in mathlib.

[Kevin Buzzard]

structure presheaf (α : Type u) [topological_space α] :=
(F     : opens α → Type v)
(res   : ∀ (U V) (HVU : V ⊆ U), F U → F V)
(Hid   : ∀ (U), res U U (set.subset.refl U) = id)
(Hcomp : ∀ (U V W) (HWV : W ⊆ V) (HVU : V ⊆ U),
  res U W (set.subset.trans HWV HVU) = res V W HWV ∘ res U V HVU)

[Kevin Buzzard]

Mathlib:

def presheaf (X : Top.{v}) := (opens X)ᵒᵖ ⥤ C

[Johan Commelin]

But ⥤ expands to your structure (up to contravariance).

[Kevin Buzzard]

so ours is slightly better for this use case because we don't have the op issues.

[Kevin Buzzard]

I don't know how serious they are to deal with though, I have never used categories seriously.

[Kevin Buzzard]

I can see Kenny's point of view though, he made what he needed in the simplest way and he knows how to work with it.

[Kevin Buzzard]

The issue that was holding me back was another one, namely the question on how to define a sheaf on an open subset of X.

[Kevin Buzzard]

Kenny just defined it to be a sheaf on X.

[Kevin Buzzard]

and then never used =

[Johan Commelin]

Sure, but that is orthogonal to whether you use the category library.

[Kevin Buzzard]

Kenny is just using the definition which is most convenient for doing what it is he wants to do

[Kevin Buzzard]

The category theory library offers this slightly more bundled experience and the added inconvenience of the ops.

[Kevin Buzzard]

I can see why he's chosen to do it this way.

[Johan Commelin]

Do you already have the adjunction between ^* and _*?

[Johan Commelin]

If you have that, I'll shut up.

[Kevin Buzzard]

We only have pullback along an open map because we don't have sheafification.

[Kevin Buzzard]

Wait -- are you asking about presheaves or sheaves? We don't define presheaf pullback

[Kevin Buzzard]

(deleted)

[Johan Commelin]

I'm asking about sheaves.

[Johan Commelin]

But I think we want both.

[Johan Commelin]

I'm not married to the category library. It's just that there's a bunch of general purpose tools there that I feel we are now duplicating. I think it might pay of to debug any problems that show up when using the category library. Because if we make the category lib usable, we can apply it in other situations as well.

[Kevin Buzzard]

We haven't defined pullback because we haven't defined sheafification.

[Brendan Seamas Murphy]

I have a working local implementation of sheafification (for presheaves abelian groups). Can I help out with this somehow?

[Kevin Buzzard]

Did you prove the adjointness? :-)

Here's the situation. Johan is concerned that an MSc student of mine came up with another definition of presheaf (following me, who defined a presheaf 18 months ago in Lean without knowing anything about how category theory worked in Lean). Now this is becoming an issue because there's another definition of presheaf in mathlib, but various Imperial students are just pushing ahead and developing a nice little theory of schemes mostly by themselves:

https://github.com/ramonfmir/lean-scheme

The initial purpose of that repo was an MSc project, which is now done. Johan is concerned that if the work doesn't get PR'ed to mathlib it will bitrot; however it is using an incompatible definition of presheaf. It would not surprise me if Kenny Lau was interested in your sheafification stuff. Which definition of presheaf did you use? :-)

[Johan Commelin]

@Brendan Seamas Murphy Nice! Well done!

[Brendan Seamas Murphy]

Oh I haven't got the adjointness down (well I was planning on doing the universal property but I think that's the same thing)

[Brendan Seamas Murphy]

I used the definition in the lean-schemes repo

[Brendan Seamas Murphy]

Copied the ring stuff and changed the type classes

[Brendan Seamas Murphy]

Thanks Johan!

[Johan Commelin]

@Kevin Buzzard @Kenny Lau Let me stress that in the end I don't really care about the shape and form of the solution. I would be very happy to (i) reach some synthesis sooner than later, and (ii) see things moving towards mathlib.

[Kenny Lau]

@Kevin Buzzard I have "relative" sheafification

[Kevin Buzzard]

@Kenny Lau do you believe this work on gluing schemes should be in mathlib and do you have an opinion on the two definitions of presheaf?

[Kenny Lau]

I would consult @Mario Carneiro

[Kenny Lau]

theorem to_stalk_res (F : presheaf X) (x : X) (U V : opens X) (hxV : x ∈ V) (HVU : V ≤ U) (s : F U) :
  to_stalk F x V hxV (F.res U V HVU s) = to_stalk F x U (HVU hxV) s :=
quotient.sound ⟨V, hxV, le_refl V, HVU, F.res_res _ _ _ _ _ _⟩

def espace_etale (F : presheaf X) : Type (max u v) :=
Σ x : X, stalk F x

def of_espace_etale (F : presheaf X) (x : espace_etale F) : X :=
x.1

def to_espace_etale (F : presheaf X) (U : opens X) (s : F U) (p : U) : espace_etale F :=
⟨p.1, to_stalk F p.1 U p.2 s⟩

instance (F : presheaf X) : topological_space (espace_etale F) :=
{ is_open := λ S, ∀ x ∈ S, ∃ U : opens X, ∃ hxU : sigma.fst x ∈ U, ∃ s : F U, to_stalk F x.1 U hxU s = x.2 ∧
    ∀ p : X, ∀ hpU : p ∈ U, (⟨p, to_stalk F p U hpU s⟩ : espace_etale F) ∈ S,
  is_open_univ := λ ⟨p, g⟩ _, quotient.induction_on g $ λ ⟨U, hpU, s⟩, ⟨U, hpU, s, rfl, λ _ _, trivial⟩,
  is_open_inter := λ S T HS HT x hxST, let ⟨U, hxU, s, hsx, hs⟩ := HS x hxST.1,
    ⟨V, hxV, t, htx, ht⟩ := HT x hxST.2, ⟨W, hxW, HWU, HWV, h⟩ := quotient.exact (hsx.trans htx.symm) in
    ⟨W, hxW, F.res U W HWU s, by rw to_stalk_res; exact hsx,
    λ q hqW, ⟨by rw to_stalk_res; apply hs, by rw [h, to_stalk_res]; apply ht⟩⟩,
  is_open_sUnion := λ SS H x hx, let ⟨t, htSS, hxt⟩ := set.mem_sUnion.1 hx,
    ⟨U, hxU, s, hsx, hs⟩ := H t htSS x hxt in ⟨U, hxU, s, hsx, λ p hpU, set.mem_sUnion_of_mem (hs p hpU) htSS⟩ }

theorem continuous_of_espace_etale (F : presheaf X) : continuous (of_espace_etale F) :=
λ U HU ⟨p, g⟩ hpU, quotient.induction_on g $ λ ⟨V, hpV, s⟩,
⟨⟨U, HU⟩ ⊓ V, ⟨hpU, hpV⟩, F.res V _ inf_le_right s, to_stalk_res _ _ _ _ _ _ _, λ q hqUV, hqUV.1⟩

theorem continuous_to_espace_etale (F : presheaf X) (U : opens X) (s : F U) : continuous (to_espace_etale F U s) :=
λ S HS, is_open_iff_forall_mem_open.2 $ λ q hq, let ⟨V, hqV, t, hts, ht⟩ := HS _ hq,
⟨W, hqW, HWV, HWU, HW⟩ := quotient.exact hts in
⟨subtype.val ⁻¹' W.1,
λ p hpW, show (⟨_, _⟩ : espace_etale F) ∈ S, by erw [← to_stalk_res F p.1 U W hpW HWU, ← HW, to_stalk_res]; apply ht,
continuous_subtype_val _ W.2, hqW⟩

def espace_etale.basic (F : presheaf X) (U : opens X) (s : F U) : opens (espace_etale F) :=
⟨{ x | ∃ hxU : x.1 ∈ U, to_stalk F x.1 U hxU s = x.2 },
λ x ⟨hxU, hx⟩, ⟨U, hxU, s, hx, λ p hpU, ⟨hpU, rfl⟩⟩⟩

structure presheaf.hom (F : presheaf X) (G : presheaf X) :=
(to_fun : Π U : opens X, F U → G U)
(to_fun_res : ∀ U V : opens X, ∀ HVU : V ≤ U, ∀ s : F U, to_fun V (F.res U V HVU s) = G.res U V HVU (to_fun U s))

structure presheaf.equiv (F : presheaf X) (G : presheaf X) :=
(to_fun : Π U : opens X, F U → G U)
(inv_fun : Π U : opens X, G U → F U)
(left_inv : ∀ U : opens X, ∀ s : F U, inv_fun U (to_fun U s) = s)
(right_inv : ∀ U : opens X, ∀ s : G U, to_fun U (inv_fun U s) = s)
(to_fun_res : ∀ U V : opens X, ∀ HVU : V ≤ U, ∀ s : F U, to_fun V (F.res U V HVU s) = G.res U V HVU (to_fun U s))

theorem sheaf.locality' (F : sheaf X) {U : opens X} {s t : F.to_presheaf U}
  (H : ∀ x ∈ U, ∃ V : opens X, ∃ HVU : V ≤ U, x ∈ V ∧ F.res U V HVU s = F.res U V HVU t) :
  s = t :=
F.locality U s t ⟨U, λ p, classical.some $ H p.1 p.2, λ p, classical.some $ classical.some_spec $ H p.1 p.2,
  λ p hp, ⟨⟨p, hp⟩, (classical.some_spec $ classical.some_spec $ H p hp).1⟩⟩ $
λ p, (classical.some_spec $ classical.some_spec $ H p.1 p.2).2

theorem sheaf.locality'' (F : sheaf X) {U : opens X} {s t : F.to_presheaf U}
  (H : ∀ x ∈ U, to_stalk F.to_presheaf x U H s = to_stalk F.to_presheaf x U H t) :
  s = t :=
F.locality' $ λ x hxU, let ⟨V, hxV, HVU, HVU', hv⟩ := quotient.exact (H x hxU) in ⟨V, HVU, hxV, hv⟩

theorem germ.eta (F : presheaf X) (x : X) (g : germ F x) (H) :
  (⟨g.1, H, g.3⟩ : germ F x) = g :=
by cases g; refl

noncomputable def sheaf.glue (F : sheaf X) (U : opens X) (OC : covering U) (S : Π i : OC.ι, F.to_presheaf (OC.map i))
  (H : ∀ i j : OC.ι, F.res (OC.map i) (OC.map i ⊓ OC.map j) inf_le_left (S i) =
    F.res (OC.map j) (OC.map i ⊓ OC.map j) inf_le_right (S j)) :
  F.to_presheaf U :=
classical.some $ F.gluing U OC S H

theorem res_glue (F : sheaf X) (U : opens X) (OC : covering U) (S H i) :
  F.res U (OC.map i) (OC.map_le i) (F.glue U OC S H) = S i :=
classical.some_spec (F.gluing U OC S H) i

theorem glue_eq (F : sheaf X) (U : opens X) (OC : covering U) (S : Π i : OC.ι, F.to_presheaf (OC.map i)) (H s)
  (H2 : ∀ i, F.res U (OC.map i) (OC.map_le i) s = S i) :
  F.glue U OC S H = s :=
F.locality _ _ _ OC $ λ i, by rw [res_glue, H2]

theorem to_stalk_glue (F : sheaf X) {U : opens X} {OC : covering U} {S : Π i : OC.ι, F.to_presheaf (OC.map i)}
  {H p} (i) (H2 : p ∈ OC.map i) :
  to_stalk F.to_presheaf p U (OC.map_le i H2) (F.glue U OC S H) = to_stalk F.to_presheaf p (OC.map i) H2 (S i) :=
by rw ← to_stalk_res; congr' 1; apply res_glue

[Kenny Lau]

Fundamental theorem of sheaf theory:

noncomputable def equiv_continuous_section_espace_etale (F : sheaf X) :
  F.to_presheaf.equiv (continuous_section_subsheaf (espace_etale F.to_presheaf) (of_espace_etale F.to_presheaf)).to_sheaf.to_presheaf :=
{ to_fun := λ U s, ⟨to_espace_etale F.to_presheaf U s, continuous_to_espace_etale F.to_presheaf U s, λ p, rfl⟩,
  inv_fun := λ U s, F.glue U
    ⟨U, λ p, ⟨subtype.val '' (s.1 ⁻¹' (espace_etale.basic F.to_presheaf (quotient.out (s.1 p).2).1 (quotient.out (s.1 p).2).3).1),
        let ⟨V, hv1, hv2⟩ := s.2.1 (espace_etale.basic F.to_presheaf (quotient.out (s.1 p).2).1 (quotient.out (s.1 p).2).3).1
          (espace_etale.basic F.to_presheaf (quotient.out (s.1 p).2).1 (quotient.out (s.1 p).2).3).2 in
        by rw [← hv2, subtype.image_preimage_val]; exact is_open_inter hv1 U.2⟩,
      λ p q ⟨r, hr, hrq⟩, hrq ▸ r.2,
      λ p hpU, ⟨⟨p, hpU⟩, ⟨p, hpU⟩, ⟨(quotient.out (s.1 ⟨p, hpU⟩).2).2,
        by dsimp only [to_stalk]; rw germ.eta; exact quotient.out_eq _⟩, rfl⟩⟩
    (λ p, F.res (quotient.out (s.1 p).2).1 _ (λ q ⟨r, ⟨hsr1, hsr2⟩, hrq⟩, hrq ▸ s.2.2 r ▸ hsr1) (quotient.out (s.1 p).2).3)
    (λ p q, F.locality'' $ λ r ⟨⟨u, ⟨hsu1, hsu2⟩, hur⟩, ⟨v, ⟨hsv1, hsv2⟩, hvr⟩⟩,
      have huv : u = v, from subtype.eq $ hur.trans hvr.symm,
      have hsu : (s.1 u).1 = u.1, from s.2.2 u,
      begin
        clear_, iterate 4 { erw to_stalk_res }; substs huv hur; cases u with u hu; dsimp only at *,
        generalize : equiv_continuous_section_espace_etale._match_3 F U s p u _ = h1,
        generalize : equiv_continuous_section_espace_etale._match_3 F U s q u _ = h2,
        revert h1 h2, rw ← hsu, intros, erw [hsu2, hsv2]
      end),
  left_inv := λ U s, glue_eq _ _ _ _ _ _ $ λ p, F.locality'' $ λ q ⟨u, ⟨hsu1, hsu2⟩, huq⟩,
    by clear_; erw [to_stalk_res, to_stalk_res]; subst huq; exact hsu2.symm,
  right_inv := λ U s, subtype.eq $ funext $ λ p, sigma.eq (s.2.2 p).symm $ begin
    dsimp only [to_espace_etale],
    generalize : to_espace_etale._proof_1 U p = h1,
    generalize : (s.2.2 p).symm = h2,
    revert h1 h2, rw ← s.2.2 p, intros, dsimp only,
    erw to_stalk_glue F, swap 3, exact p, swap,
    { refine ⟨p, ⟨(quotient.out (s.1 p).2).2, _⟩, (s.2.2 p).symm⟩,
      dsimp only [to_stalk], rw [germ.eta, quotient.out_eq] },
    erw to_stalk_res, dsimp only [to_stalk], rw [germ.eta, quotient.out_eq]
  end,
  to_fun_res := λ U V HVU s, subtype.eq $ funext $ λ p, sigma.eq rfl $ to_stalk_res _ _ _ _ _ _ _ }

[Kenny Lau]

thanks for attending my "live" coding session

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Did you PR to lean-scheme?

[Kenny Lau]

no

[Kevin Buzzard]

I mean push

[Kevin Buzzard]

I would like to amalgamate this with the extra power of bundled top spaces at some point

[Johan Commelin]

@Kenny Lau Thanks for sharing your coding session with us :stuck_out_tongue_wink:

[Kevin Buzzard]

What's the notation for sum? I don't know how to work it out without asking

[Johan Commelin]

Which sum?

[Johan Commelin]

Sum of types?

[Kevin Buzzard]

yes

[Kevin Buzzard]

disjoint union. I'm making a category, I think

[Johan Commelin]

Does \oplus work?

[Kevin Buzzard]

Well, I'm making a partially ordered set. I'm assuming I can get a category from it.

[Johan Commelin]

Yep, that's done by type class inference.

[Johan Commelin]

Once you've imported the right files, of course.

[Kevin Buzzard]

Do I just import the same files as in Scott's tutorial?

[Kevin Buzzard]

I don't know where to look for information

[Johan Commelin]

$ git grep preorder | grep category_theory
src/category_theory/category.lean:namespace preorder
src/category_theory/category.lean:instance small_category [preorder α] : small_category α :=
src/category_theory/category.lean:end preorder

[Johan Commelin]

So, it's in the most basic file, and you'll be fine.

[Kevin Buzzard]

Are there any special functions for dealing with Prop-valued diagrams? I only care about maps from partial orders to Top and I'm having trouble defining functors because inductive props can't eliminate into type :-/

[Kevin Buzzard]

If I want to do a simple diagram like one with three objects U, V, and U intersect V, and maps corresponding to inclusions, because I want to take a colimit, should I make the diagram category using props as homs or subsingletons?

[Kevin Buzzard]

I want to glue open sets $U_i$ over common open subsets $U_{ij}$ which are morally $U_i\cap U_j$

[Kevin Buzzard]

Trying to define the functor I am stuck with goals like

1 goal
A B C : Type,
h : A = B ∨ A = C,
b : B,
c : C
⊢ A

[Kevin Buzzard]

so I have to use classical.some in a situation where I don't feel like I need classicality.

[Kevin Buzzard]

What do I do with a term of type plift h where h is a proposition? I want to do cases on it without dropping into Prop world.

[Chris Hughes]

pilft.down or something

[Kevin Buzzard]

example (A B C : Type) (h : plift (A = B ∨ A = C)) : plift (A = B) ⊕ plift (A = C) := sorry

[Kevin Buzzard]

Is that a thing?

[Kevin Buzzard]

I'll have classical, noncomputable, anything you like.

[Chris Hughes]

Yes

[Kevin Buzzard]

I've always found the definition of up and down rather beautiful.

/-- Universe lifting operation from Sort to Type -/
structure plift (α : Sort u) : Type u :=
up :: (down : α)

(that's it). Is it proved to be a subsingleton?

[Chris Hughes]

classical.choice $ h.down.elim (sum.inl \circ plift.up) (sum.inr \circ plift.up) I think

[Chris Hughes]

I forgot some nonempty.intro

[Chris Hughes]

Why do you need plift? I believe proofs as homs are allowed these days.

[Kevin Buzzard]

I thought I let type class inference turn my poset into a category and that's what I got. Let me check this again.

[Kevin Buzzard]

#check ∀ (X : Type u) [preorder X] (x y : X), x ⟶ y
/-
Π (X : Type u) [_inst_3 : preorder X] (x y : X), x ⟶ y : Type (u+1)
-/

[Chris Hughes]

Maybe the library hasn't been updated to take advantage of this yet.

[Kevin Buzzard]

I'm on Xena, that's usually bleeding edge because I don't care if it doesn't compile any more. Future explorers can just see which commit of mathlib I was using at the time ;-)

[Chris Hughes]

Maybe the preorder to category instance in bleeding edge hasn't been uodated

[Kevin Buzzard]

noncomputable example (A B C : Type) (h : plift (A = B ∨ A = C)) : plift (A = B) ⊕ plift (A = C) :=
classical.choice $ h.down.elim (nonempty.intro ∘ sum.inl ∘ plift.up) (nonempty.intro ∘ sum.inr ∘ plift.up)

[Kenny Lau]

my "live" coding session can be found in https://github.com/kckennylau/Lean/blob/master/sheaf_fundamental.lean

[Kevin Buzzard]

noncomputable example (P Q : Prop) (h : plift (P ∨ Q)) : plift P ⊕ plift Q :=
classical.choice $ h.down.elim (nonempty.intro ∘ sum.inl ∘ plift.up) (nonempty.intro ∘ sum.inr ∘ plift.up)

Now I formalise the correct statement, and Chris' proof is so beautiful that the same proof proves the correct theorem

[Kevin Buzzard]

Kenny I really think you should consider writing a lot of this in the language of lattices.

[Kenny Lau]

attribute [instance] classical.prop_decidable
noncomputable example (p q : Prop) (h : plift (p ∨ q)) : plift p ⊕ plift q :=
or.by_cases h.1 (sum.inl ∘ plift.up) (sum.inr ∘ plift.up)

[Kevin Buzzard]

When you bundled ideals, you really wanted to use lattices and I was quite anti the idea.

[Kevin Buzzard]

But now I've started to use lattices I think it's a really good idea.

[Kevin Buzzard]

The fact that mathematicians want to see a different symbol should not be the problem of the code designer. This is some translation issue which is coming later.

[Kevin Buzzard]

These issues should be solved using controlled natural language stuff leaving Lean to be as latticey as it wants to be.

[Johan Commelin]

@Kevin Buzzard Chris is right. This line should be changed: https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category.lean#L137

[Johan Commelin]

Changing it might break some other parts of mathlib, but the refactor should make things easier (-;

[Kevin Buzzard]

Every time Patrick or I try something, there's always some issue. You guys need to do some recruitment. I thought Australians were experts at category theory?

[Kevin Buzzard]

I can't refactor a library I've barely used. I am still staring at

def cylinder (X : Top) : Top := limit (pair X I)
-- To define a map to the cylinder, we give a map to each factor.
-- `binary_fan.mk` is a helper method for constructing a `cone` over `pair X Y`.
def cylinder_0 (X : Top) : X ⟶ cylinder X :=
limit.lift (pair X I) (binary_fan.mk (𝟙 X) (to_pt X ≫ I_0))

and thinking "that's how you do example (b : B) : A -> A \prod B := \lam a, (a, b) now is it? :-(

[Johan Commelin]

The last time I tried to do modular forms in mathlib I had loads of issues (-; There was really nothing at all.

[Johan Commelin]

Well, to be honest, in the example you give, you also have to include the fact that your easy definition is continuous.

[Johan Commelin]

If you do that, I think the total count of characters won't be too far away from Scott's example.

[Kevin Buzzard]

Do you think type class inference would do it?

[Johan Commelin]

No, because continuous is not a class.

[Kevin Buzzard]

Oh! Why not?

[Kevin Buzzard]

I think we've had this discussion before

[Kevin Buzzard]

So you are kind of elevating it to class status

[Johan Commelin]

Ooh, and snap... ulift $ plift stuff for preorder cats is there to make the category small )-;

[Johan Commelin]

I have no idea why continuous is not a class. But it was never done.

[Chris Hughes]

I tried fixing the preorder.category, but Prop homs aren't small categories any more, so the limit stuff doesn't work because that is all on small categories.

[Johan Commelin]

Stupid non-cumulative universes :wink:

[Johan Commelin]

I guess we'll have to live with uplift... taking non-small limits comes with its own bucket of headaches.

[Kevin Buzzard]

I'm trying to prove that my homsets are subsingletons and Lean is asking me whether the left inclusion $U\cap U\to U$ is equal to the right inclusion.

[Kevin Buzzard]

What am I supposed to say to that??

[Kevin Buzzard]

They're definitely the same :-/

[Kevin Buzzard]

I think I mustn't implement the hom sets as abstract types. I think I actually need to think about them as explicit functions and then I can extensionality.

[Kevin Buzzard]

@Scott Morrison @Johan Commelin I don't know how to steer the category theory library. All I want to do is glue a bunch of unbundled top spaces together. I need to make the appropriate category. The objects I can make. For the morphisms I tried first making a partial order on the objects and then making the associated small category, and I was forever having to deal with goals like plift (X or Y) not being able to decompose easily. I'm now trying to build the morphisms but I can't prove that hom sets are subsingletons and I don't know whether I should be trying to do that or not.

[Kevin Buzzard]

import topology.Top.limits
import category_theory.limits.shapes
import topology.instances.real

-- Want to create X from an open cover U_i, as a colimit.
-- So we're given the U_i for i in an index type I, and
-- also the "glue"

-- unbundled data

universes u i
variable (I : Type i) -- index type
variables (Ui : I → Type u) [∀ i, topological_space (Ui i)]
variables (Uij : I → I → Type u) [∀ i j, topological_space (Uij i j)]
variables (inc_l : ∀ {i j}, Uij i j → Ui i) (inc_l_cts : ∀ i j : I, continuous (@inc_l i j))
variables (inc_r : ∀ {i j}, Uij i j → Ui j) (inc_r_cts : ∀ i j : I, continuous (@inc_r i j))

inductive J (I : Type i)
| of_I : I → J
| of_glue : I → I → J

namespace J

-- In general, things are easier if homs are props.
-- But in category theory I had problems defining maps
-- from a proppyhom category because I was always having
-- to solve goals of the form plift (X ∨ Y) -> plift X ⊕ plift Y.
-- So I gave up on
/-
inductive le : J I → J I → Prop
| refl (j : J I) : le j j
| res_l (i₁ i₂ : I) : le (of_I i₁) (of_glue i₁ i₂)
| res_r (i₁ i₂ : I) : le (of_I i₂) (of_glue i₁ i₂)
-/

-- and went for homs in Type u.

inductive hom : J I → J I → Type i
| id (j : J I) : hom j j
| res_l (i₁ i₂ : I) : hom (of_I i₁) (of_glue i₁ i₂)
| res_r (i₁ i₂ : I) : hom (of_I i₂) (of_glue i₁ i₂)

open hom

def hom.comp : Π (X Y Z : J I) (f : hom I X Y) (g : hom I Y Z), hom I X Z
  | _ _ _ (id _) h := h
  | _ _ _ h (id _) := h
  -- these next lines should match the line above, right?
  | (of_I _) (of_glue _ _) (of_glue _ _) (res_l _ _) (id (of_glue i₁ i₂)) := res_l i₁ i₂
  | (of_I _) (of_glue _ _) (of_glue _ _) (res_r _ _) (id (of_glue i₁ i₂)) := res_r _ _

open category_theory

instance category_struct : category_struct (J I) :=
{ hom  := hom I,
  id   := hom.id,
  comp := hom.comp I }

instance (X Y : J I) : subsingleton (X ⟶ Y) := begin
  split,
  intros a b,
  cases a,
  cases b,
  refl,
  -- wait this might not actually be true. Is res_l i i equal to res_r i i?
  sorry,sorry,
end

Do I care about subsingletons?

[Kevin Buzzard]

Is $U\cap U=U$ abstractly or not?

[Kevin Buzzard]

@Reid Barton if I just want to mimic taking the union of some subspaces of a topological space as a colimit, what diagram should I use?

[Mario Carneiro]

Making hom live in Type like that is actually a big difference than making it live in Prop and applying plift to the result. hom is not a subsingleton; your statement in the comment is false

[Scott Morrison]

It's just not true; the category you're defining does not have subsingleton homsets.

[Kevin Buzzard]

Do I care? Maybe I just decide not to care at this point