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.
added hyperlinks to the text at induced representation. Made sure that it is cross-linked with Frobenius reciprocity.
Somebody wrote a lot of detailed material in the entry what is nice. It however leaves much work to make it coherent. The section “explanation” should maybe be called “The case of Lie groups”. The section after that is giving the geometric view point by looking at the sections of equivariant bundles. However, it is extremely important what kind of sections: in the context of Lie groups, the standard attached to word induced representation is to have not continuous or smooth but rather -sections. Also I would like to put somewhere the interpretation via the tensor product (say for algebraic groups, one looks at representations at the level of enveloping algebra of a Lie algebra so the inducing functor from to is simply the extension of scalars . In so massive entry it is difficult to organize where to put such a remark, unless one spends time thinking how toseriously reorganize.
at induced representation I have made a Definition-section with two subsections. The first one, “traditional definition” contains the material that was there already, and a new one General abstract formulation in homotopy type theory adds an abstract point of view.
(I added a similar comment also to infinity-representation.)
I long meant to expand on this, but no time so far. This addition was promted by discussion over at the HoTT site.
I like the addition of the version in HoTT !
On the other hand, I think it would be good just to omit the word “general” in title and leave “abstract formulation…”; I mean it is very general in one direction, and brings many new cases, but it is not likely of course including really all existing versions of induced representations (algebraic, functional, Hopf algebraic etc.), not all of which could fit into infinity topos setup. Namely, the things which can be delooped are rather rare; many things, say noncommutatve noncocommutative Hopf alebras, where also there is induced representation will likely not have classifying spaces even in generalized sense (unless of course, we can go to some sort of noncommutative higher category theory, but this one is expected to have somewhat weaker semantics than HoTT). Of course, it is quite general. “Abstract formulation” is suggestive enough and who knows what is HoTT will already also know which level of generality that is. The real problem is now that the section on “traditional point of view” has only the group case so far, and even only discrete groups. Unfortunately, I will be able to help there only much later.
So this ’general abstract’ formulation is making further sense of Lawvere’s original linkage of representation theory to logic:
As a final example of a hyperdoctrine, we mention the one in which types are finite categories and terms arbitrary functors between them, while , where is the category of finite sets and mappings, with substitution as the special Godement multiplication. Quantification must then consist of generalized limits and colimits…By focusing on those having one object and all morphisms invertible, one sees that this hyperdoctrine includes the theory of permutation groups; in fact, such are groups and a “property” of is nothing but a representation of by permutations. Quantification yields “induced representations” and implication gives a kind of “intertwining representation”. Deductions are of course equivariant maps. (Adjointness in Foundations, p. 14)
Is there an analogue of this:
Frobenius reciprocity is saying that coinduction is isomorphic to induction (ie induction is both left and right adjoint to restriction) provided that is an inclusion.
But that relied on a finiteness assumption.
I have vague memory that in modular representation theory (that is finite characteristic case) they have much use from distinguishing restriction and corestriction functors, I am not sure about induction vs, coinduction. The groups there are quite usual, like GL(n).
re #4
it would be good just to omit the word “general” in title
Okay, sure. I was emplyong the common phrase “general abstract” for category-theoretic formulations. Notice though that it captures everything that the entry originally and still is discussing at all: representations of gorups. But of course its not “fully general” in that one can consider representations of other things, too. I’ll not object if you remove the word “general”.
OK, let us remove general only once in the stage when we discuss things beyond groups. For now it is more general :)
re #5:
Thanks, David! I hadn’t seen that. Have added the reference now and a pointed to it at induced representation.
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…
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.
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.
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.
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, , between groups
If is of finite index the analogous constructions for linear representations 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 -representations.
Added a section Examples and applications - Hecke algebra.
Here is the Hecke algebra of an -representation with respect to some , expressed in homotopy type theory:
:-)
(David, I’ll get back to you re #14. I was about to, but then got distracted by Hecke…)
Could we set up a form of higher hyperdoctrine for these higher representations, some functor from group objects in an ambient -topos to the -category of -actions?
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?
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.
At induced+representation#general_abstract_formulation where it has
The general case of -groups in -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?
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.
I was there due to thinking about the (co)monads on induced from a map of -groups, , by
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 a subgroup of ?
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 a subgroup of ?
One thing to keep in mind is that in general the -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 , and acting on the point, the above left adjoint produces the groupoid , regarded as an -representation of the trivial group.
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?
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.
At the level of 1-groups, for the dependent product what do we have?
For subgroups
What of epis?
What of
[To return to when I’ve finished marking here.]
So p. 150 of Basic Bundle Theory and K-Cohomology Invariants is useful here.
For , and -action , the coinduced action (dependent product) is , regarded as an -space by left multiplication via . (Couple of misprints there, I think.)
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.
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”.
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.
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
1 to 32 of 32