Zulip Chat Archive
Stream: general
Topic: sigma type mismatch
Kevin Buzzard (Mar 26 2018 at 09:59):
stalk2 below doesn't typecheck:
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), ℕ
Kevin Buzzard (Mar 26 2018 at 10:00):
red squiggle is on the sigma in stalk2
Kevin Buzzard (Mar 26 2018 at 10:00):
error is
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)
Kevin Buzzard (Mar 26 2018 at 10:01):
I think that I would rather work with stalk2 rather than stalk1
Kevin Buzzard (Mar 26 2018 at 10:01):
because I tend to avoid subtypes if I can
Kevin Buzzard (Mar 26 2018 at 10:02):
I am still a bit scared of all the up-arrows
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 ]
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.
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.
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:
Kevin Buzzard (Mar 26 2018 at 11:02):
definition stalk2 (x : X) (U : set X) (Hx : x ∈ U) := Σ (PU : P U), ℕ
Kevin Buzzard (Mar 26 2018 at 11:03):
and I don't really understand why.
Kevin Buzzard (Mar 26 2018 at 11:03):
But at the end of the day
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.
Kevin Buzzard (Mar 26 2018 at 11:05):
Are you suggesting I stick with the stalk1 approach?
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?
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.
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!
Kenny Lau (Mar 26 2018 at 15:17):
@Kevin Buzzard have you tried it? (if not, i’ll do it)
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
Kenny Lau (Mar 26 2018 at 15:24):
I’ll do it when i get back home then
Kenny Lau (Mar 26 2018 at 15:24):
which will happen in 15 minutes
Kevin Buzzard (Mar 26 2018 at 15:26):
I pushed as far as I got. Thanks.
Last updated: Dec 20 2023 at 11:08 UTC