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.
One must be careful with transitive action about the empty set, but all is fine here? I guess any group acting on the empty set is a free action.
What’s the HoTT version of freeness? Something like $IsSet(\sum_{\ast: BG} V(\ast))$.
I would probably state it as: for any $x$, the type of $g$ such that $g x = x$ is contractible (or, equivalently, a proposition, since it’s always inhabited by $e$).
Typed up in the Sandbox the observation/proof that infinity-quotients of infinity-free actions in an infinity-topos are 0-truncated. But need to go offline right now. Will port and polish tomorrow.
[ thought I could weaken the assumptions of the prop, but maybe I can’t ]
What I was after in #7 does work, after all, one has to appeal to the groupoidal Segal conditions:
I have stepped back and added a Definition-subsection
with the declaration that an $\infty$-action is free if its shear map “in degree 1” is (-1)-truncated, and a proof that this implies that also all “higher shear maps” are (-1)-truncated.
WIth this, the Prop. from #6 above (here) now says that as soon as the shear map $X \times G \to X \times X$ of an $\infty$-action is $(-1)$-truncated, the homotopy quotient of the $\infty$-action is the plain quotient of its 0-truncated version.
I should add a commentary to the entry on the following point, which can be confusing:
The $\infty$-action on a principal $\infty$-bundle is always fiber-wise free, but not globally so unless it’s base space is 0-truncated. Partially-conversely, every $\infty$-action is fiberwise free (in fact principal) over its homotopy quotient. (all internal to some $\infty$-topos).
1 to 9 of 9