## Stream: maths

### Topic: gluing functions

#### Kenny Lau (Jul 21 2019 at 06:50):

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 (Jul 22 2019 at 00:59):

@Kenny Lau That looks great!!

#### Johan Commelin (Jul 22 2019 at 01:01):

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 (Jul 22 2019 at 04:21):

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 (Jul 22 2019 at 05:04): 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,

end subsheaf


#### Kenny Lau (Jul 22 2019 at 05:27):

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 (Jul 22 2019 at 05:28):

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 (Jul 22 2019 at 05:42):

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

#### Kenny Lau (Jul 22 2019 at 05:43):

the large amount of unop required

#### Johan Commelin (Jul 22 2019 at 05:45):

@Scott Morrison Should we make a cv_functor?

#### Johan Commelin (Jul 22 2019 at 05:49):

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

#### Johan Commelin (Jul 22 2019 at 05:49):

Do you see particular troubles on the road?

I dont know

#### Scott Morrison (Jul 22 2019 at 05:55):

cv_functor feels like we’d be unnecessarily multiplying entities.

#### Scott Morrison (Jul 22 2019 at 05:56):

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 (Jul 22 2019 at 05:56):

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

#### Johan Commelin (Jul 22 2019 at 06:11):

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 (Jul 22 2019 at 11:10):

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 (Jul 22 2019 at 11:13):

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

#### Kevin Buzzard (Jul 22 2019 at 12:46):

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 (Jul 22 2019 at 12:48):

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 (Jul 22 2019 at 12:49):

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

#### Johan Commelin (Jul 22 2019 at 12:53):

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 (Jul 22 2019 at 12:53):

Sure, with the sheaf condition there might be trouble.

#### Johan Commelin (Jul 22 2019 at 12:53):

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 (Jul 22 2019 at 12:55):

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 (Jul 22 2019 at 12:56):

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

#### Kevin Buzzard (Jul 22 2019 at 12:56):

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

#### Kevin Buzzard (Jul 22 2019 at 12:58):

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 (Jul 22 2019 at 13:00):

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

#### Johan Commelin (Jul 22 2019 at 13:02):

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

#### Johan Commelin (Jul 22 2019 at 13:02):

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

#### Johan Commelin (Jul 22 2019 at 13:03):

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 (Jul 22 2019 at 13:04):

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 (Jul 22 2019 at 14:10):

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 (Jul 22 2019 at 14:45):

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 (Jul 22 2019 at 14:46):

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 (Jul 22 2019 at 14:49):

Mathlib:

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


#### Johan Commelin (Jul 22 2019 at 14:50):

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

#### Kevin Buzzard (Jul 22 2019 at 14:52):

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

#### Kevin Buzzard (Jul 22 2019 at 14:53):

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

#### Kevin Buzzard (Jul 22 2019 at 14:54):

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 (Jul 22 2019 at 14:55):

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 (Jul 22 2019 at 14:55):

Kenny just defined it to be a sheaf on X.

#### Kevin Buzzard (Jul 22 2019 at 14:55):

and then never used =

#### Johan Commelin (Jul 22 2019 at 14:57):

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

#### Kevin Buzzard (Jul 22 2019 at 14:58):

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

#### Kevin Buzzard (Jul 22 2019 at 14:58):

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

#### Kevin Buzzard (Jul 22 2019 at 14:59):

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

#### Johan Commelin (Jul 22 2019 at 15:06):

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

#### Johan Commelin (Jul 22 2019 at 15:06):

If you have that, I'll shut up.

#### Kevin Buzzard (Jul 22 2019 at 15:07):

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

#### Kevin Buzzard (Jul 22 2019 at 15:07):

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

(deleted)

#### Johan Commelin (Jul 22 2019 at 15:14):

But I think we want both.

#### Johan Commelin (Jul 22 2019 at 15:16):

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 (Jul 22 2019 at 15:33):

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

#### Brendan Seamas Murphy (Jul 22 2019 at 20:44):

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

#### Kevin Buzzard (Jul 22 2019 at 21:46):

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 (Jul 23 2019 at 04:23):

@Brendan Seamas Murphy Nice! Well done!

#### Brendan Seamas Murphy (Jul 23 2019 at 04:24):

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 (Jul 23 2019 at 04:24):

I used the definition in the lean-schemes repo

#### Brendan Seamas Murphy (Jul 23 2019 at 04:24):

Copied the ring stuff and changed the type classes

Thanks Johan!

#### Johan Commelin (Jul 23 2019 at 04:40):

@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 (Jul 23 2019 at 05:15):

@Kevin Buzzard I have "relative" sheafification

#### Kevin Buzzard (Jul 23 2019 at 09:09):

@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 (Jul 23 2019 at 09:59):

I would consult @Mario Carneiro

#### Kenny Lau (Jul 23 2019 at 14:34):

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 (Jul 23 2019 at 14:35):

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 (Jul 23 2019 at 14:35):

thanks for attending my "live" coding session

:-)

#### Kevin Buzzard (Jul 23 2019 at 14:35):

Did you PR to lean-scheme?

no

I mean push

#### Kevin Buzzard (Jul 23 2019 at 14:36):

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

#### Johan Commelin (Jul 23 2019 at 14:53):

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

#### Kevin Buzzard (Jul 23 2019 at 14:53):

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

#### Johan Commelin (Jul 23 2019 at 14:53):

Which sum?

Sum of types?

yes

#### Kevin Buzzard (Jul 23 2019 at 14:54):

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

#### Johan Commelin (Jul 23 2019 at 14:54):

Does \oplus work?

#### Kevin Buzzard (Jul 23 2019 at 14:54):

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

#### Johan Commelin (Jul 23 2019 at 14:54):

Yep, that's done by type class inference.

#### Johan Commelin (Jul 23 2019 at 14:54):

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

#### Kevin Buzzard (Jul 23 2019 at 14:55):

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

#### Kevin Buzzard (Jul 23 2019 at 14:55):

I don't know where to look for information

#### Chris Hughes (Jul 23 2019 at 16:59):

I forgot some nonempty.intro

#### Chris Hughes (Jul 23 2019 at 17:02):

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

#### Kevin Buzzard (Jul 23 2019 at 17:03):

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 (Jul 23 2019 at 17:05):

#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 (Jul 23 2019 at 17:05):

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

#### Kevin Buzzard (Jul 23 2019 at 17:05):

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 (Jul 23 2019 at 17:06):

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

#### Kevin Buzzard (Jul 23 2019 at 17:11):

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 (Jul 23 2019 at 17:11): my "live" coding session can be found in https://github.com/kckennylau/Lean/blob/master/sheaf_fundamental.lean #### Kevin Buzzard (Jul 23 2019 at 17:12): 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 (Jul 23 2019 at 17:14):

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

#### Kenny Lau (Jul 23 2019 at 17:14):

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 (Jul 23 2019 at 17:14):

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

#### Kevin Buzzard (Jul 23 2019 at 17:14):

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

#### Kevin Buzzard (Jul 23 2019 at 17:15):

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 (Jul 23 2019 at 17:15):

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

#### Johan Commelin (Jul 23 2019 at 17:30):

@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 (Jul 23 2019 at 17:31):

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

#### Kevin Buzzard (Jul 23 2019 at 17:44):

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 (Jul 23 2019 at 17:46):

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 (Jul 23 2019 at 17:46):

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

#### Johan Commelin (Jul 23 2019 at 17:48):

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

#### Johan Commelin (Jul 23 2019 at 17:48):

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

#### Kevin Buzzard (Jul 23 2019 at 17:49):

Do you think type class inference would do it?

#### Johan Commelin (Jul 23 2019 at 17:49):

No, because continuous is not a class.

Oh! Why not?

#### Kevin Buzzard (Jul 23 2019 at 17:49):

I think we've had this discussion before

#### Kevin Buzzard (Jul 23 2019 at 17:50):

So you are kind of elevating it to class status

#### Johan Commelin (Jul 23 2019 at 17:50):

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

#### Johan Commelin (Jul 23 2019 at 17:50):

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

#### Chris Hughes (Jul 23 2019 at 17:57):

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 (Jul 23 2019 at 17:59):

Stupid non-cumulative universes :wink:

#### Johan Commelin (Jul 23 2019 at 18:02):

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

#### Kevin Buzzard (Jul 23 2019 at 20:28):

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 (Jul 23 2019 at 20:29):

What am I supposed to say to that??

#### Kevin Buzzard (Jul 23 2019 at 20:29):

They're definitely the same :-/

#### Kevin Buzzard (Jul 23 2019 at 20:30):

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 (Jul 23 2019 at 20:41):

@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 (Jul 23 2019 at 20:47):

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 (Jul 23 2019 at 20:47):

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

#### Kevin Buzzard (Jul 23 2019 at 21:44):

@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 (Jul 23 2019 at 22:19):

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 (Jul 24 2019 at 00:36):

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

#### Kevin Buzzard (Jul 24 2019 at 07:40):

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

Last updated: May 06 2021 at 18:20 UTC