Zulip Chat Archive

Stream: maths

Topic: gluing functions


view this post on Zulip 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 }

view this post on Zulip Johan Commelin (Jul 22 2019 at 00:59):

@Kenny Lau That looks great!!

view this post on Zulip 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]).

view this post on Zulip 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 }

view this post on Zulip 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,
  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

view this post on Zulip Kenny Lau (Jul 22 2019 at 05:24):

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

view this post on Zulip 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 }

view this post on Zulip 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 π

view this post on Zulip Johan Commelin (Jul 22 2019 at 05:42):

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

view this post on Zulip Kenny Lau (Jul 22 2019 at 05:43):

the large amount of unop required

view this post on Zulip Johan Commelin (Jul 22 2019 at 05:45):

@Scott Morrison Should we make a cv_functor?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 22 2019 at 05:49):

Do you see particular troubles on the road?

view this post on Zulip Kenny Lau (Jul 22 2019 at 05:49):

I dont know

view this post on Zulip Scott Morrison (Jul 22 2019 at 05:55):

cv_functor feels like we’d be unnecessarily multiplying entities.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 22 2019 at 05:56):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 22 2019 at 11:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 22 2019 at 12:53):

Sure, with the sheaf condition there might be trouble.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:56):

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

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:56):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 14:49):

Mathlib:

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 14:50):

But expands to your structure (up to contravariance).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 14:55):

Kenny just defined it to be a sheaf on X.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 14:55):

and then never used =

view this post on Zulip Johan Commelin (Jul 22 2019 at 14:57):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 14:59):

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 15:06):

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 15:06):

If you have that, I'll shut up.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 15:07):

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

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 15:07):

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

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 15:07):

(deleted)

view this post on Zulip Johan Commelin (Jul 22 2019 at 15:14):

I'm asking about sheaves.

view this post on Zulip Johan Commelin (Jul 22 2019 at 15:14):

But I think we want both.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 15:33):

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

view this post on Zulip 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?

view this post on Zulip 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? :-)

view this post on Zulip Johan Commelin (Jul 23 2019 at 04:23):

@Brendan Seamas Murphy Nice! Well done!

view this post on Zulip 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)

view this post on Zulip Brendan Seamas Murphy (Jul 23 2019 at 04:24):

I used the definition in the lean-schemes repo

view this post on Zulip Brendan Seamas Murphy (Jul 23 2019 at 04:24):

Copied the ring stuff and changed the type classes

view this post on Zulip Brendan Seamas Murphy (Jul 23 2019 at 04:24):

Thanks Johan!

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 23 2019 at 05:15):

@Kevin Buzzard I have "relative" sheafification

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 23 2019 at 09:59):

I would consult @Mario Carneiro

view this post on Zulip 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

view this post on Zulip 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 _ _ _ _ _ _ _ }

view this post on Zulip Kenny Lau (Jul 23 2019 at 14:35):

thanks for attending my "live" coding session

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:35):

:-)

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:35):

Did you PR to lean-scheme?

view this post on Zulip Kenny Lau (Jul 23 2019 at 14:35):

no

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:36):

I mean push

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:53):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:53):

Which sum?

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:53):

Sum of types?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:54):

yes

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:54):

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

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:54):

Does \oplus work?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:54):

Yep, that's done by type class inference.

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:54):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:55):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 14:55):

I don't know where to look for information

view this post on Zulip Johan Commelin (Jul 23 2019 at 15:00):

$ 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 15:00):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 15:57):

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 :-/

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:38):

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?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:39):

I want to glue open sets UiU_i over common open subsets UijU_{ij} which are morally UiUjU_i\cap U_j

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:41):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:41):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:51):

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.

view this post on Zulip Chris Hughes (Jul 23 2019 at 16:53):

pilft.down or something

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:54):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:54):

Is that a thing?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:54):

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

view this post on Zulip Chris Hughes (Jul 23 2019 at 16:55):

Yes

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 16:57):

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?

view this post on Zulip Chris Hughes (Jul 23 2019 at 16:58):

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

view this post on Zulip Chris Hughes (Jul 23 2019 at 16:59):

I forgot some nonempty.intro

view this post on Zulip Chris Hughes (Jul 23 2019 at 17:02):

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

view this post on Zulip 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.

view this post on Zulip 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)
-/

view this post on Zulip Chris Hughes (Jul 23 2019 at 17:05):

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

view this post on Zulip 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 ;-)

view this post on Zulip Chris Hughes (Jul 23 2019 at 17:06):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 17:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 17:31):

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

view this post on Zulip 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?

view this post on Zulip 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? :-(

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 17:49):

Do you think type class inference would do it?

view this post on Zulip Johan Commelin (Jul 23 2019 at 17:49):

No, because continuous is not a class.

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 17:49):

Oh! Why not?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 17:49):

I think we've had this discussion before

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 17:50):

So you are kind of elevating it to class status

view this post on Zulip Johan Commelin (Jul 23 2019 at 17:50):

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

view this post on Zulip Johan Commelin (Jul 23 2019 at 17:50):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 23 2019 at 17:59):

Stupid non-cumulative universes :wink:

view this post on Zulip 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.

view this post on Zulip 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 UUUU\cap U\to U is equal to the right inclusion.

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 20:29):

What am I supposed to say to that??

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 20:29):

They're definitely the same :-/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 20:47):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 24 2019 at 00:36):

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

view this post on Zulip 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