Zulip Chat Archive

Stream: general

Topic: sigma type mismatch


view this post on Zulip Kevin Buzzard (Mar 26 2018 at 09:59):

stalk2 below doesn't typecheck:

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:00):

universe u
variables (X : Type u) (P : set (set X))

definition  stalk1 (x : X) :=
Σ U : {U : set X // x ∈ U ∧ P U}, ℕ

definition  stalk2 (x : X) :=
Σ (U : set X) (Hx : x ∈ U) (PU : P U), ℕ

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:00):

red squiggle is on the sigma in stalk2

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:00):

error is

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:00):

type mismatch at application
  Σ (PU : P U), ℕ
term
  λ (PU : P U), ℕ
has type
  P U → Type : Type 1
but is expected to have type
  ?m_1 → Type : Type (max ? 1)

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:01):

I think that I would rather work with stalk2 rather than stalk1

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:01):

because I tend to avoid subtypes if I can

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:02):

I am still a bit scared of all the up-arrows

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 10:04):

[background : X is a topological space, P is a basis for the open sets, I'm defining the stalk of a presheaf https://stacks.math.columbia.edu/tag/009H just after 6.30.1; here's a special case https://stacks.math.columbia.edu/tag/0078 which in Lean currently looks like https://github.com/kbuzzard/lean-stacks-project/blob/16a88206397eaa664dd00cf917c78359b7119cb3/src/tag0078.lean#L9 ]

view this post on Zulip Chris Hughes (Mar 26 2018 at 10:36):

Sigma only takes two arguments. Also the type of nat doesn't depend on the set, so you may as well use prod.

view this post on Zulip Sebastian Ullrich (Mar 26 2018 at 10:42):

@Chris Hughes It's desugared to nested sigmas. But it still doesn't typecheck because P U does not live in Type _. I would suggest using structures in favor of nested anything.

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:02):

@Chris Hughes -- the actual type I want to make is more complex -- the nat was just a MWE of my problem. @Sebastian Ullrich I need to make a type because I am actually interested in a quotient of the type I'm trying to construct. Your observation is that this doesn't typecheck either:

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:02):

definition stalk2 (x : X) (U : set X) (Hx : x ∈ U) := Σ (PU : P U), ℕ

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:03):

and I don't really understand why.

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:03):

But at the end of the day

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:04):

I would like some sigma type so I can put an equivalence relation on it and form the quotient type.

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:05):

Are you suggesting I stick with the stalk1 approach?

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:06):

Presumably you prefer A -> B -> C to A and B -> C, i.e. here we avoid the structure [not subtype -- sorry] and prefer the "nested" approach?

view this post on Zulip Sebastian Ullrich (Mar 26 2018 at 11:07):

No, I'm suggesting

structure stalk3 (x : X) :=
(U : set X) (Hx : x ∈ U) (PU : P U) (n : ℕ)

so that you don't have to worry about every component whether it should be a sigma or a prod or a pprod or ... and on top of that you get projections with meaningful names.

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 11:55):

Oh, I see: and then this is still a type so I can still put an equivalence relation on it. I will try it this way! Thanks!

view this post on Zulip Kenny Lau (Mar 26 2018 at 15:17):

@Kevin Buzzard have you tried it? (if not, i’ll do it)

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 15:19):

No, I've been at meetings until recently and since then I've been talking to Chris about rings

view this post on Zulip Kenny Lau (Mar 26 2018 at 15:24):

I’ll do it when i get back home then

view this post on Zulip Kenny Lau (Mar 26 2018 at 15:24):

which will happen in 15 minutes

view this post on Zulip Kevin Buzzard (Mar 26 2018 at 15:26):

I pushed as far as I got. Thanks.


Last updated: May 10 2021 at 19:16 UTC