added a section at the beginning (here) that just states the definition right away. Kept the previous material, but re-titled the subsection as “More exposition”.

]]>added a section at the beginning (here) that just states the definition right away. Kept the previous material, but re-titled the subsection as “More exposition”.

]]>added pointer to *Brauer induction theorem*

While doing so I noticed that this entry is in bad shape. It’s too verbose without getting to the simple point. If nobody objects, I’ll eventually go and remove much of the old chatty material and bring in the actual abstract characterization and the explicit formula for induced representations right away

]]>Pull-push transforms involve just the dependent sum and base change (linear polynomials functors), right? It sounds like Mackey functor people also think about coinduction/dependent product, and even more explicitly in work on (non-linear) polynomial functors/Tambara functors.

Anyway, perhaps there’s another opportunity for HoTT enthusiasts to do some calculations.

]]>Certainly. As the entry *Mackey functor* mentions a bit, these are of similar nature as motives in the guise of “sheaves with transfer”, which in turn is a of the general kind of “pull-push integral transforms through correspondences”. There are some comments on the general similarity of these structures with structures naturally appearing in dependent linear homotopy theory in the very last section of “Quantization via linear homotopy types”.

Hmm, I wonder if (linear) HoTT could lend a hand with the topic of Mackey functors. There’s plenty of talk of induction and coinduction, fixed-points and quotients, as in Mackey functors, induction from restriction functors and coinduction from transfer functors:

]]>Boltje’s plus constructions extend two well-known constructions on Mackey functors, the fixed-point functor and the fixed-quotient functor. In this paper, we show that the plus constructions are induction and coinduction functors of general module theory.

So p. 150 of Basic Bundle Theory and K-Cohomology Invariants is useful here.

For $\rho: H \to G$, and $H$-action $Y$, the coinduced action (dependent product) is $Map_H(G, Y)$, $G$ regarded as an $H$-space by left multiplication via $\rho$. (Couple of misprints there, I think.)

]]>At the level of 1-groups, for the dependent product what do we have?

For subgroups

- $\mathbf{B} H \to \mathbf{B} G$: essentially a fiber product of the thing $H$ acts on with coset space $G/H$.

What of epis?

- $\mathbf{B} G \to \ast$: fixed points of the $G$-action.

What of

- $\mathbf{B} G \to \mathbf{B} H$, so $H$ a quotient of $G$: something like what’s fixed in the $G$-action by the associated normal subgroup?

[To return to when I’ve finished marking here.]

]]>Yes, one of the big themes in higher stuctures is that everything becomes simpler, more basic, more elementary, instead of more complicated. In a century from now it will be common wisdom. The kids will be taught homotopy theory and will look upon what is remembered of the contemporary state of the art with the same respect with which we regard roman numerals and epicycles.

]]>In traditional discussions one will have to find conditions that serve to avoid this.

Life really is easier in an untruncated world. Who would want to go away from there?

]]>whether they could be seen as a form of necessity/possibilit

They certainly could, and I think it will be interesting to do so.

Is there a reason why the traditional treatment (here and elsewhere) just looks at $H$ a subgroup of $G$?

One thing to keep in mind is that in general the $\infty$-adjunction applied to a rep on an ordinary space may end up giving something whose underlying object is higher groupoidal. In traditional discussions one will have to find conditions that serve to avoid this.

For instance in the extreme case that $G = \ast$, and $H$ acting on the point, the above left adjoint produces the groupoid $\mathbf{B}H$, regarded as an $\infty$-representation of the trivial group.

]]>I was there due to thinking about the (co)monads on $Act(H)$ induced from a map of $\infty$-groups, $f: H \to G$, by

$(\sum_f \dashv f^* \dashv \prod_f) \colon Act(H) \stackrel{\overset{\sum_f}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\underset{\prod_f}{\to}}} Act(G) \,,$and whether they could be seen as a form of necessity/possibility.

Is there a reason why the traditional treatment (here and elsewhere) just looks at $H$ a subgroup of $G$?

]]>Thanks for catching this. Not sure if this will remain stable in the future. But so generally I shouldn’t be pointing to section numbers like this. I’ll remove the specific section numbers.

]]>At induced+representation#general_abstract_formulation where it has

The general case of $\infty$-groups in $\infty$-toposes is further discussed in sections 3.3.11-3.3.13 of [dcct]

I guess that’s now 5.1.14-5.1.16. Is the new section numbering likely to remain stable?

]]>we’ve already got something better, i.e., a dependent type theory, with pullbacks of slices, etc.?

Yes!

What can I say exactly about the relationship between a hyperdoctrine and a dependent type theory?

The notion of hyperdoctrine is essentially the attempt to axiomatize how slices behave in a locally cartesian closed category, to be used in cases where we may not actaually have one. If we have a locally cartesian closed category already, its codomain fibration is a hyperdoctrine, but we don’t really need to say that, we can just stick with our locally cartesian closed category. And that’s (the semantics of a) dependent type theory.

]]>Oh, am I missing the point that we’ve already got something better, i.e., a dependent type theory, with pullbacks of slices, etc.?

What can I say exactly about the relationship between a hyperdoctrine and a dependent type theory?

]]>Could we set up a form of higher hyperdoctrine for these higher representations, some functor from group objects in an ambient $(\infty,1)$-topos to the $(\infty,1)$-category of $\infty$-actions?

]]>Added a section *Examples and applications - Hecke algebra*.

Here is the Hecke algebra of an $H$-representation $E$ with respect to some $i : H \to G$, expressed in homotopy type theory:

$Hecke(E,i) = \underset{\mathbf{B}G}{\prod} \left[ \underset{\mathbf{B}i}{\sum}E, \underset{\mathbf{B}i}{\sum} E \right] \,.$:-)

(David, I’ll get back to you re #14. I was about to, but then got distracted by Hecke…)

]]>In Equality in Hyperdoctrines Lawvere’s interested in hyperdoctrines in which two kinds of identity hold, the possession of which allows for a satisfactory theory of equality. The first of these conditions is

…formally similar to, and reduces in particular to, the Frobenius reciprocity formula for permutation representations of groups,

these forming a hyperdoctrine. The second condition is Beck-Chevalley. So does that explain the origin? Frobenius reciprocity generally holds in the case of representations, but in the specific case of permutation representations it takes on a particular form, and it’s that form that Lawvere uses to designates a special property of some hyperdoctrines.

My other small wonder concerns later where he writes of a morphism, $f$, between groups

If $f$ is of finite index the analogous constructions for

linearrepresentations yield isomorphic results, which is perhaps why there seems to be no established name for “universal quantification” in representation theory.

So ’coinduction’ is the established name now, leading to the question of whether induction and coinduction can coincide ever in the realm of $\infty$-representations.

]]>Hi David,

sorry, I realize that I might be talking nonsense: I didn’t actually follow your links (still haven’t) , being in a haste (still am). Maybe if you have (or somebody else reading this here has…) a second you could add a remark on that relation to *Frobenius reciprocity*.

Are the representation-theoretic and the category-theoretic meanings of Frobenius reciprocity not interlinked?

Given the Lawvere-type interpretation of the induced representation as the dependent sum in a locally cartesian closed category of representations they are interlinked. But I never saw somebody admit that this is the *reason* why the term is used that way, historically. And even if, what I usually see is that “Frobenius reciprocity” in representation theoretic terms just means that “the induction functor is adjoint to the restriction functor”, whereas the category-theoretic meaning would be a second step: given that it is adjoint, it in addition satisfies a certain relation that exhibits the restriction functor as a cartesian closed functor.

That’s why I am asking. I was wondering if you had a deeper insight here. I remember we had this kind of discussion before and I think it ended inconclusively.

]]>I always get confused about these things. Are the representation-theoretic and the category-theoretic meanings of Frobenius reciprocity not interlinked?

I gathered from Simon and Todd here that finiteness was needed for Frobenius to imply that induction and coinduction are isomorphic, so not holding by definition.

]]>Frobenius reciprocity is saying that coinduction is isomorphic to induction (ie induction is both left and right adjoint to restriction) provided that f:G→H is an inclusion.

Let’s see, just to be sure: there are these two meanings of Frobenius reciprocity, the representation-theoretic and the category-theoretic one. For the former, the above sentence holds pretty much by definition, I gather. (?) Or are you saying that the sentence above starts with the latter meaning of Frobenius reciprocity? That I would need to further think about…

]]>re #5:

Thanks, David! I hadn’t seen that. Have added the reference now and a pointed to it at *induced representation*.