Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I would like to understand the following question in an -topos / in homotopy type theory:
Given an object with an action by a group , and given another object . How can we naturally construct , the quotient of the space of maps by acting by precomposition?
This seems basic, but I am being a bit dense, maybe.
I am suspecting that this object is . At least this exbits some -action, so if it’s not the one I am after then a second question I have: which action is this?
The -action on is exhibited by a fiber sequence
Similarly we get the fiber sequence
where is the stand-in notation for whatever the fiber of the morphism on the right is. This exhibits an action of on Q.
What is ?
So I can say what is, the discrete type of global points of , by this line of reasoning:
That matches my initial guess that .
I am currently hesitant as to how to proceed in the first step above without the s. It seems clear, but I need to think about it more.
But so it looks like this gives a canonical construction of a -action on . Can we also check that indeed it is the expected action by pre-composition with the -action on ?
I thought of this consistency check here:
For a -action on , its invariants are . So maybe I can check what is. I compute:
which is the right answer, I suppose, the maps that are invariant under precomposing the -action on .
That’s how far I got for the moment. Will further mull over this. Beware that there might be major blunders in the above, these thoughts are only about as old as it took to type this post.
Can’t you just use the fact that fibers preserve exponentials? I assume that by you mean the exponential in the slice , so that then denotes taking the total space. Since taking fibers preserves this exponential, the fiber of this space over is , since is the fiber of and is the fiber of .
Ah, thanks! I wasn’t actively aware of this statement that taking fibers preserves the exponential.
Phew, that’s awesome.
You know, I found this statement rather curious, that homming out of in the slice gives one . It’s remarkable, because the naive hom out of it gives just the invariants, wich is entirely unlike So then it took me a bit to realize that it is the right answer if regarded as the global sections over . It’s kind of magic that it all works out so nicely in the slice.
By the way, this is important for doing not just gauge theory, but gravitational gauge theory in cohesive homotopy type theory. There the configuration type (the “integrated off-shell BRST complex”) is not , as for -Yang-Mills theory, but is .
Next I want to understand “multisymplectic BRST” in cohesive HoTT. For that I need to understand as the space of sections of a bundle over .
A comment on that aspect of “multisymplectic BRST”, just for the record, on the off-chance that anyone reading this here cares about it:
So from the above I am thinking: for a worldvolume and a target space, the “integrated extended BRST phase space” of the relativistic -model on seems to want to be the dual jet bundle of
in , where is the étale geometric morphism.
The graded coordinates on the -piece would be the diffeomorphism ghosts in the exended multisymplectic picture. Passing to the space of global sections would give the ordinary (unextended) off-shell BRST phase space .
It’s kind of magic that it all works out so nicely in the slice.
Yes, I agree!
I have started making a brief note on this at infinity-action.
I have added a bit more to infinity-action meant to serve as exposition of the cartesian closed structure on --actions:
brief remark on the trivial action and inverse images of étale geometric morphisms, just so that we can point to it;
elementary discussion of cartesian closure of discrete 0-group -actions aka -sets in Conjugation actions (for completeness)
brief remark on the above-mentioned case, which I find deserves to be named General covariance
I had wanted to expand on that. But those Zombie-processes kept me from doing more.
1 to 7 of 7