Multivariable loop spaces

[fredrik-bakke]

Co-authored-by: Mark Williams [email protected]

[VojtechStep]

Do you have a reference for this concept 👀? I'd like to see what the "variables" refer to, and why I should think about non-generalized loop spaces as "bivariable"

[fredrik-bakke]

@VojtechStep No, unfortunately I don't have a reference. This is original work and you can consider the name as merely a working name for now. I suppose part of the motivation is that one wants higher loop spaces to be captured by the same notion, so e.g. an 𝕊¹-ary loop should be a double loop, and that works with this definition of a higher-ary loop space.

[fredrik-bakke]

I can also draw the comparison to that the left-adjoint of loops, suspensions, is the colimit of the binary terminal span.

[VojtechStep]

This is original work and you can consider the name as merely a working name for now.

Are you open to workshopping it as part of the review process? I understand if you want to have this merged now and build on top if it, so in case you're not, I'd like you to add a note in the file stating that the naming is not standard and subject to change.

This concept feels much more like "indexed based path spaces" than "multivariable loop spaces" to me, since in the most basic cases of 0 and 1 "variables", you don't get loop spaces at all (and while I would expect the 0 case do degenerate somewhat, I wouldn't expect a "degenerate loop space of A" to be A).
"Multivariable loop spaces" sounds to me like I → ΩA, which you show corresponds to Ωᴵ⁺¹A

[fredrik-bakke]

Sure! There's no rush with this one, as it turns out it's probably not the most general thing for us to consider after all.

One thing that might be tripping up your instincts is that loop spaces are most naturally considered in the category of pointed spaces. There the booleans represent points, so maybe we shouldn't call it "binary" in this case, but rather unary. Also notice how, as soon as I is pointed, then loops I A is pointed equivalent to I ->* loops A, which is the formula you highlight just in pointed spaces.

[VojtechStep]

There the booleans represent points, so maybe we shouldn't call it "binary" in this case, but rather unary.

I think this is the missing piece for me. Could you add something to the Idea section about the pointed perspective?

[fredrik-bakke]

I've added an explanation now. Let me know if this is satisfactory, and thank you for leading me to a better explanation!

[VojtechStep]

I also recently saw Jon Sterling use the name "inward fan" for Σ (a : A). a = a* https://cl-l313.jonmsterling.com/01GY/

[fredrik-bakke]

That's a quirky term imo, although I get the motivation. For my purposes, the direction of the equality is not important.

[fredrik-bakke]

Would you suggest calling the present term "fan with multiplicity" or something?

[fredrik-bakke]

In this paper https://arxiv.org/pdf/2404.07854 he calls them fans and co-fans btw, I believe.

[VojtechStep]

I was thinking something along the lines of "indexed fans", but I'm having a hard time convincing even myself of this name

[fredrik-bakke]

I believe "indexed fans" would have a dependent over I. The present notion is more like a multiplicity of the fan

[VojtechStep]

The section headers are uncharacteristically terse compared to the usual style, e.g. "Characterizing equality/identifications of multivariable loop spaces". Is that intentional?

[fredrik-bakke]

In my opinion shorter section headers make the right-hand bar more usable, since it otherwise looks more like a word soup than a table of contents. The added context presented by

Suggested change

	### Characterizing equality
	### Characterizing equality in `I`-ary loop spaces

should already be inferable.

[VojtechStep]

I think this would benefit from a small comment, as it might not be entirely obvious how one "inverts" a based path

[fredrik-bakke]

let me know if this is what you had in mind:

### The multiplicative inverse

Given `i∗ : I` and `a∗ : A`, then any `I`-ary loop `(a , p)` has a
multiplicative inverse given by `(a∗ , (i ↦ (p i)⁻¹ ∙ p i∗))`.

[VojtechStep]

Not left-inv-mul-multivar-Ω for "left inverse of multiplication"?

[fredrik-bakke]

Whoops

[fredrik-bakke]

Oh, I was reading this name as "left multiplication by the inverse", which seemed neat because it can also be interpreted as "the inverse to left multiplication" which still is correct. Thought this entry was about the left inverse law first.