Objects with no canonical definition

Stream: maths

[Eric Wieser]

What should mathlib do about objects for which the literature provides multiple incompatible definitions? Do we pick one arbitrarily and declare it mathlib-canonical? Do we provide all the definitions with numbered names and docstrings to disambiguate them?

[Eric Wieser]

The context here is formalizing the Pin group, $\operatorname{Pin}(V, q)$, for which apparently there are at least three different definitions (MathOverflow) that disagree on what sign to associate with the "spinor norm", or whether to consider its absolute value

[Johan Commelin]

I think if all three concepts are useful for mathlib, and they are not even canonically isomorphic, then we should maybe have 3 different names?

[Johan Commelin]

In other cases, we just pick one thing as the defn, and the rest become theorems (typically disguised as defs)

[Eric Wieser]

I guess "does nat include 0" is an example where we just picked a definition

[Damiano Testa]

I would argue that the choice made for nat is way more controversial of which choice we could make for the Pin groups...

[Kyle Miller]

I guess there's a $\operatorname{Pin}_+(V,q)$ and a $\operatorname{Pin}_-(V,q)$ group, both "the" Pin group but not isomorphic, and related by negating the quadratic form. Maybe what's going on is that there's an additional piece of data that's being chosen arbitrarily in each of these conventions? Is there some space that naturally parameterizes the pin groups?

[Eric Wieser]

Can you point me to a definition of those $+$ and $-$ subscripts? Where I've seen them elsewhere (as $\operatorname{Pin}^{+}(n)$), my initial reading was that they just encoded information about $q$ when it was omitted

[Kyle Miller]

My understanding is that in general there are two possible non-isomorphic double covers of O(V,q), but they're both also double covers of O(V,-q). I think the idea is just that, depending on your convention, the + one is the one you'd associate to O(V,q), but based on my limited understanding it seems that the different conventions sort of amount to randomly swapping between the two depending on what the dimension of V is (mod 4 maybe?) I don't really know anything about Pin groups other than what I gleaned from Wikipedia and nlab.

[Eric Wieser]

(note that wikipedia and nlab do a bad job of defining $\operatorname{Spin}$ too)

[Wrenna Robson]

Eric Wieser said:

I guess "does nat include 0" is an example where we just picked a definition

If nat didn't include zero, it wouldn't be an additive monoid... so I guess the real question is "are the naturals a monoid or just a semigroup"?

[Kevin Buzzard]

I think that's the same question but just rather obfuscated.

[Eric Wieser]

@Kyle Miller, I think you're right, and that the difference between the two conventions originate from representing $\operatorname{Pin}(n)$ with $Cl(n)$, with the difference being whether you intend this shortened notation to mean $Q(v_i) = 1, i ∈ [0, n)$ or $Q(v_i) = -1, i ∈ [0, n)$.

[Eric Wieser]

(which are the $q$ and $-q$ cases you mention)

[Wrenna Robson]

@Kevin Buzzard yeah maybe - but I'm not sure I would have realised that when I was less familiar with this stuff.