Peter LeFanu Lumsdaine

less info
3,351 reputation
1230
bio website mathstat.dal.ca/…
location Halifax, Canada
age 31
visits member for 4 years, 4 months
seen 8 hours ago

math.LO/math.CT, currently at the Institute for Advanced Study, Princeton, lately of Dalhousie University, Nova Scotia, and Carnegie Mellon University, Pittsburgh.


11h
comment For which Millennium Problems does undecidable -> true?
@ChristianRemling: “The truth of a conjecture can’t make a set $\Pi^0_1$ if it wasn't so to start with.” Sure, but the $\Pi^0_1$-ness of a set can be implied by (or even equivalent to) some conjecture. A proof of the conjecture can’t change whether the set is $\Pi^0_1$, but it can tell us whether or not it is.
Apr
7
revised Why is a braided left autonomous category also right autonomous?
expanded answer, attempted to fix latex, added disclaimer for unfixed parts.
Apr
7
answered Why is a braided left autonomous category also right autonomous?
Mar
28
revised On the Complement of a subgroup
fixed link (and grammar)
Mar
10
reviewed Approve suggested edit on self-dual representations
Mar
8
comment Intuitive crutches for higher dimensional thinking
@KConrad: your joke reminds me of a musical version I witnessed. Most musicians have at some point learned to play triplets against duplets — one of your hands plays 2 evenly spaced notes per beat, the other hand plays 3. 3-against-4 is also not uncommon, and in ≥C20th music, higher divisions also occur. At this particular dinner, one pianist marvelled that another could play a perfectly even 13-against-14 rhythm; a composer present was surprised at the surprise. “But it’s easy, isn’t it? You just set up one hand playing 13, and the other playing 14, and then you put them together!”
Mar
8
awarded  Notable Question
Feb
25
comment Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
@PietroMajer: that’s fascinating! Can you suggest any good sources for seeing the intermediate stages? Or, even better, any articles about this transition?
Feb
25
accepted Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
Feb
24
revised Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
added link to this question at the HoM Area 51 proposal
Feb
24
asked Historical quotation search: Equations/formulae in (Latin?) prose, before modern symbolic notation
Feb
15
comment Is Turing degree actually useful in real life?
@Noah: besides Andy Putman's reasons, I voted to close because "in real life" is extremely broad and subjective, and rarely leads to interesting content. And, indeed, the contentful parts of the answers so far are those that explicitly drop the "in real life" part of the question.
Jan
23
comment Why the term “monad” in homological algebra?
@ToddTrimble: I’d vote against making this CW. The answers so far are indeed speculative (though not equally so); but it’s easy to imagine a better answer coming along that was less speculative. (For instance, a reference to a paper from around when the term was introduced, giving an explanation or motivation for the term; or even a personal recollection like Sasha’s in comments, but with clearer attribution.)
Jan
22
comment Why the term “monad” in homological algebra?
One other mathematical usage of monad comes to mind: in logic, unary predicates (i.e. “X is a dog”, but not relations like “X loves Y”) are called monadic predicates, and predicate logic based just on monadic predicates is called monadic logic. The earliest use of this terminology I can find is 1956, when Halmos wrote a paper titled monadic Boolean algebras, but the study of such logics goes back a couple of decades further, and I suspect the terminology does as well, though my google-fu is failing me.
Jan
20
awarded  Custodian
Jan
20
reviewed Approve suggested edit on Characterisation for separable extension of a field
Jan
8
comment name for a subset of a binary relational structure which is “closed downward”?
Or just left–closed, to keep the wording slightly simpler.
Jan
5
comment Prospects for reverse mathematics in Homotopy Type Theory
@FrançoisG.Dorais: I’d take issue with your first paragraph (though I agree with the rest of your answer) — it conflates two uses of the word theorem. A theorem can mean either “a true/proven statement” or just “a statement”. Proof-relevance affects the first sense: one doesn’t talk about a theorem being true without presenting/positing a witness to it. But reverse mathematics uses the second sense; one can ask “what system is required to imply statement X?”, without referring to any particular proof of X, just as well in HoTT as classically.
Jan
5
answered How to characterize flasque sheaves in more functorial way?
Dec
24
revised Exact squares containing a cospan: what is known about this category?
corrected some mistakes