Transitivity of induction and coinduction #
This file records restriction and coinduction in stages for representations along composable monoid
homomorphisms, and induction in stages along composable group homomorphisms. It obtains the natural
isomorphisms from the equality of restriction functors MonoidHom.resFunctor_comp and
Mathlib's induction--restriction and restriction--coinduction adjunctions. This is the categorical
core used by the subgroup form of induction.
Uniqueness of adjoints produces those isomorphisms without ever saying what they do, and a comparison map known only up to an abstract adjoint characterisation is of no use to a computation with induced characters or with the Mackey decomposition, both of which have to follow a chosen coset representative through the isomorphism. The second half of this file therefore evaluates them on representatives:
⟦κ ⊗ₜ ⟦h ⊗ₜ a⟧⟧ ↦ ⟦ψ(h) κ ⊗ₜ a⟧, ⟦κ ⊗ₜ a⟧ ↦ ⟦κ ⊗ₜ ⟦1 ⊗ₜ a⟧⟧
for induction, and dually F ↦ (κ ↦ F κ 1), f ↦ (κ ↦ (h ↦ f (ψ(h) κ))) for coinduction.
The route to these formulas is the mates calculus rather than an unfolding of
Adjunction.leftAdjointCompIso. The identity CategoryTheory.unit_conjugateEquiv says that
conjugate natural transformations agree after composing with the two units; since the unit of the
induction--restriction adjunction is the generator map a ↦ ⟦1 ⊗ₜ a⟧ and resFunctorCompIso is
the identity on vectors, that identity computes the inverse isomorphism
(indFunctorCompIso φ ψ).inv on the generator ⟦1 ⊗ₜ a⟧ of the singly induced representation,
which is where both units land. Equivariance then spreads that single value over all group
coordinates, giving the inverse on every generator, and the forward formula follows by inverting
it. Both steps use the relation ⟦κ ⊗ₜ ⟦h ⊗ₜ a⟧⟧ = ⟦ψ(h) κ ⊗ₜ ⟦1 ⊗ₜ a⟧⟧ inside the coinvariants
(TauCeti.indV_mk_ind_mk), which also says that the elements with inner coordinate 1
generate, so that the formula determines the map. The coinduction side is the same argument run
through CategoryTheory.conjugateEquiv_counit_symm and the counit, which is evaluation at 1;
there it is the forward isomorphism that the counits compute, and the inverse that is derived.
Main definitions #
TauCeti.Rep.resFunctorCompIso,TauCeti.Rep.indFunctorCompIso,TauCeti.Rep.coindFunctorCompIso: restriction, induction and coinduction in stages, as natural isomorphisms of functors.TauCeti.Rep.indFunctorMulEquivIso: induction along a group isomorphism is restriction along its inverse.TauCeti.Rep.indFunctorSubgroupOfIso: induction in stages through an intermediate subgroupS ≤ T ≤ G, withSidentified with the subgroupS.subgroupOf TofT.
Main statements #
TauCeti.Rep.indFunctorCompIso_hom_app_hom_apply_mk_mkandTauCeti.Rep.indFunctorCompIso_inv_app_hom_apply_mk: induction in stages on representatives, the two directions of the isomorphism computed on the generators of the induced representation.TauCeti.Rep.eq_indFunctorCompIso_hom_app: those formulas pin the isomorphism down. A morphism of representations sending⟦1 ⊗ₜ ⟦1 ⊗ₜ a⟧⟧to⟦1 ⊗ₜ a⟧for everya : Ais the induction-in-stages isomorphism, which is how a comparison map built by hand is identified with the adjoint one.TauCeti.Rep.coindFunctorCompIso_hom_app_hom_apply_coe_applyandTauCeti.Rep.coindFunctorCompIso_inv_app_hom_apply_coe_apply_coe_apply: coinduction in stages on functions, the dual formulas.TauCeti.indV_mk_apply_inv,TauCeti.indV_mk_ind_mkandTauCeti.indV_ind_hom_ext: the coinvariants relation moving the group action of an induced representation into its group coordinate, its form for a twice-induced representation, and the resulting extensionality principle.TauCeti.Rep.ind_hom_apply_mkandTauCeti.Rep.ind_ind_hom_ext: a morphism out of an induced representation is the translate of its value at the group coordinate1, so two morphisms out of a twice-induced representation already agree once they agree on⟦1 ⊗ₜ ⟦1 ⊗ₜ a⟧⟧.
Implementation notes #
The four representative formulas are tagged with the pre-order @[simp↓] rather than @[simp],
like TauCeti.Rep.resFunctorCompIso_hom_app_apply above them. Their left-hand sides are readable
but not in post-order simp-normal form: on the induction side Representation.IndV.mk φ ρ h is a
reducible abbreviation that simp unfolds to Representation.Coinvariants.mk _ (single h 1 ⊗ₜ a),
and on the coinduction side simp rewrites the source and target of
(coindFunctorCompIso φ ψ).hom.app A, which appear as implicit arguments, with
CategoryTheory.Functor.comp_obj and Rep.coindFunctor_obj. A plain @[simp] tag is therefore
rejected by the simpNF linter and would never fire, and restating the formulas in the linter's
normal form is not a way out: that form pairs rewritten implicit type arguments with an unrewritten
Representation.IntertwiningMap.instFunLike instance argument, which no surface syntax elaborates
to. @[simp↓] fires the lemma before those subterms are normalised, so simp closes goals stated
in the readable form, and rw and exact still apply the lemmas as usual.
References #
C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, §10, and J.-P. Serre, Linear Representations of Finite Groups, §7.
Generators of induced and coinduced representations #
The lemmas of this section speak only about Representation.IndV and Representation.coindV and
mention no object of Rep, so they are not declared in the Rep namespace. They also stay out of a
Representation namespace: scripts/lint-dot-notation.py rejects a Mathlib type namespace nested
inside TauCeti, because the resulting name would not give dot notation on Representation.
Moving the group action out of an induced representation into its group coordinate:
⟦κ ⊗ₜ τ h⁻¹ y⟧ = ⟦ψ(h) κ ⊗ₜ y⟧. This is Representation.Coinvariants.mk_tmul_inv for the
tensor product defining Representation.IndV.
Moving the inner group coordinate of a twice-induced representation out to the outer one:
⟦κ ⊗ₜ ⟦h ⊗ₜ a⟧⟧ = ⟦ψ(h) κ ⊗ₜ ⟦1 ⊗ₜ a⟧⟧. Every element of Ind_ψ (Ind_φ A) is therefore a sum of
elements whose inner coordinate is 1, which is what makes the two representative formulas below
determine the induction-in-stages isomorphism.
Two linear maps out of a twice-induced representation agree as soon as they agree on the
elements ⟦κ ⊗ₜ ⟦1 ⊗ₜ a⟧⟧ whose inner group coordinate is 1.
Restriction along two composable group homomorphisms is naturally isomorphic to restriction
along their composite. The two functors are in fact equal (MonoidHom.resFunctor_comp), so this is
that equality read as an isomorphism.
Equations
Instances For
The forward component of resFunctorCompIso acts as the identity on vectors.
The inverse component of resFunctorCompIso acts as the identity on vectors.
Induction in stages: induction along a composite is naturally isomorphic to successive inductions along the two group homomorphisms.
Equations
- TauCeti.Rep.indFunctorCompIso φ ψ = (Rep.indResAdjunction k φ).leftAdjointCompIso (Rep.indResAdjunction k ψ) (Rep.indResAdjunction k (ψ.comp φ)) (TauCeti.Rep.resFunctorCompIso φ ψ)
Instances For
The induction-in-stages isomorphism is characterized by the restriction-composition isomorphism under the adjunction equivalence.
A morphism out of an induced representation is the κ⁻¹-translate of its value at the group
coordinate 1: it sends ⟦κ ⊗ₜ b⟧ to Y.ρ κ⁻¹ of its value on ⟦1 ⊗ₜ b⟧. Together with
TauCeti.indV_ind_hom_ext this is what lets a formula at the coordinate 1 determine a
morphism out of an induced representation.
Two morphisms of K-representations out of a twice-induced representation agree as soon as
they agree on the elements ⟦1 ⊗ₜ ⟦1 ⊗ₜ a⟧⟧. This is the Rep-morphism companion of
TauCeti.indV_ind_hom_ext: equivariance removes the outer group coordinate from its
hypothesis.
Induction in stages on representatives, backwards: the inverse of the induction-in-stages
isomorphism sends ⟦κ ⊗ₜ a⟧ to ⟦κ ⊗ₜ ⟦1 ⊗ₜ a⟧⟧. Tagged @[simp↓] rather than @[simp] because
simp unfolds the reducible Representation.IndV.mk in the left-hand side.
Induction in stages on representatives: the induction-in-stages isomorphism sends
⟦κ ⊗ₜ ⟦h ⊗ₜ a⟧⟧ to ⟦ψ(h) κ ⊗ₜ a⟧. This is the explicit formula the character and Mackey
computations consume, in place of the abstract adjoint comparison. Tagged @[simp↓] for the same
reason as TauCeti.Rep.indFunctorCompIso_inv_app_hom_apply_mk.
The induction-in-stages isomorphism is determined by its values on the generators. A
morphism of K-representations Ind_ψ (Ind_φ A) ⟶ Ind_{ψφ} A sending ⟦1 ⊗ₜ ⟦1 ⊗ₜ a⟧⟧ to
⟦1 ⊗ₜ a⟧ for every a : A is the induction-in-stages isomorphism. This is how a comparison map
built by hand is identified with the adjoint one produced by TauCeti.Rep.indFunctorCompIso.
Induction along an isomorphism is restriction along its inverse. For e : G ≃* H,
Ind_e ≅ Res_{e⁻¹} as functors Rep k G ⥤ Rep k H: both are left adjoint to Res_e, which is an
equivalence (MulEquiv.resFunctorEquiv).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Induction in stages through an intermediate subgroup. For subgroups S ≤ T of G,
inducing a representation of S, viewed as the subgroup S.subgroupOf T of T, first to T
and then to G is inducing it from S to G directly. The identification of S.subgroupOf T
with S is Subgroup.subgroupOfEquivOfLe.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Coinduction in stages: successive coinductions are naturally isomorphic to coinduction along the composite homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coinduction-in-stages isomorphism is characterized by the inverse restriction-composition isomorphism under the inverse adjunction equivalence.
Coinduction in stages on functions: the coinduction-in-stages isomorphism sends an
H-equivariant function F : K → coind φ A, whose values are themselves the G-equivariant
functions H → A, to κ ↦ F κ 1. This is the dual of
TauCeti.Rep.indFunctorCompIso_hom_app_hom_apply_mk_mk, and is obtained from its value at 1 by
K-equivariance. Tagged @[simp↓] rather than @[simp] because simp rewrites the source and
target of the isomorphism component in the left-hand side.
Coinduction in stages on functions, backwards: the inverse of the coinduction-in-stages
isomorphism turns a G-equivariant function f : K → A into κ ↦ (h ↦ f (ψ(h) κ)), the dual of
TauCeti.Rep.indFunctorCompIso_inv_app_hom_apply_mk. Tagged @[simp↓] for the same reason as
TauCeti.Rep.coindFunctorCompIso_hom_app_hom_apply_coe_apply.