The projection formula for induced representations

For a group homomorphism φ : G →* H, a G-representation A and an H-representation B, the projection formula (or tensor identity) is the isomorphism of H-representations

Ind_φ (A ⊗ Res_φ B) ≅ (Ind_φ A) ⊗ B.

It says that induction is a morphism of modules over the representation ring of H: an induced representation may be tensored with an H-representation either before or after inducing.

Mathlib has only the shadow of this statement obtained by taking H-coinvariants of both sides, Rep.coinvariantsTensorIndNatIso, which it uses for Shapiro's lemma. The isomorphism of representations itself is not a formal consequence of the induction--restriction adjunction: Representation.ind is built as the coinvariants of k[H] ⊗[k] A, so the map has to be produced by hand on representatives and then shown to descend and to be equivariant. That is what this file does, over an arbitrary commutative ring, at the generality of a group homomorphism rather than a subgroup inclusion.

The two directions are

⟦h ⊗ₜ (a ⊗ₜ b)⟧ ↦ ⟦h ⊗ₜ a⟧ ⊗ₜ ρ_B(h⁻¹) b, ⟦h ⊗ₜ a⟧ ⊗ₜ b ↦ ⟦h ⊗ₜ (a ⊗ₜ ρ_B(h) b)⟧.

The inverse h⁻¹ is not decorative. In Mathlib's model, g : G identifies h ⊗ₜ (a ⊗ₜ b) with φ(g)h ⊗ₜ (ρ_A(g) a ⊗ₜ ρ_B(φ g) b), so a twist ρ_B(f h) by a function f : H → H descends to the coinvariants as soon as f (φ(g) h) · φ(g) = f h for all g and h — a condition on f alone, which does not mention B. The canonical solution is f h = h⁻¹, and it is also the one that makes the map H-equivariant, because H acts on Ind_φ A by h₁ • ⟦h ⊗ₜ a⟧ = ⟦h h₁⁻¹ ⊗ₜ a⟧.

Main definitions

• TauCeti.indProjection: the projection formula, Rep.ind φ (X ⊗ Rep.res φ Y) ≅ Rep.ind φ X ⊗ Y in Rep k H.
• TauCeti.indProjectionEquiv, TauCeti.indProjectionLEquiv: the same isomorphism as an equivalence of Representations and as a k-linear equivalence of the underlying modules, built from the two explicit maps TauCeti.indProjectionHom and TauCeti.indProjectionInv.
• TauCeti.indProjectionNatIsoLeft, TauCeti.indProjectionNatIsoRight: the projection formula as a natural isomorphism of functors, in the left tensor factor (the Rep k G argument) and in the right one (the Rep k H argument) respectively.

The classical corollary for a subgroup S ≤ G, Ind_S^G (Res_S^G Y) ≅ k[G ⧸ S] ⊗ Y, needs the identification of Ind_S^G (trivial) with the permutation representation and therefore lives downstream, as TauCeti.indResProjection in TauCeti/RepresentationTheory/Induction/Permutation.lean.

Main statements

• TauCeti.indProjectionHom_apply_mk, TauCeti.indProjectionInv_apply_mk: the two k-linear maps on generators. Every proof below about the projection formula goes through these two rules rather than through the definitions.
• TauCeti.indProjection_hom_hom_apply, TauCeti.indProjection_inv_hom_apply: the two directions of the Rep k H isomorphism on generators.
• TauCeti.indProjection_hom_naturality_left, TauCeti.indProjection_hom_naturality_right: naturality in each variable.
• TauCeti.coinvariantsTensorIndHom_map_indProjection_mk: the comparison with Mathlib's coinvariants shadow. Taking H-coinvariants of indProjection and following with Mathlib's Rep.coinvariantsTensorIndHom sends ⟦⟦h ⊗ₜ z⟧⟧ to ⟦z⟧, with no trace of h left.

Implementation notes

Representation.IndV.mk φ ρ h is a reducible abbreviation for Coinvariants.mk _ ∘ₗ TensorProduct.mk k _ _ (MonoidAlgebra.single h 1), which simp unfolds. The generator lemmas below are therefore stated with IndV.mk, the readable form, but are not simp lemmas: their left-hand sides are not in simp-normal form and they never fire. This matches Mathlib's own Rep.coinvariantsTensorIndHom_mk_tmul_indVMk. They are applied by explicit rw/Eq.trans instead, so that only the two definitions TauCeti.indProjectionHom and TauCeti.indProjectionInv are ever unfolded, and only in their own generator lemmas. For the same reason the proofs below reach the generators by an explicit Representation.IndV.hom_ext/TensorProduct.ext' chain and peel the resulting compositions one at a time with LinearMap.comp_apply under conv_lhs/conv_rhs: an unrestricted ext/simp step also unfolds IndV.mk, after which the generator lemmas no longer match.

The Representation-level constructions are universe-polymorphic in k, G, H and the two carrier modules. The Rep k H layer is not, and cannot be: Rep.{w} k G is monoidal only for w the universe of k (ModuleCat.monoidalCategory is stated for ModuleCat.{u} R with R : Type u), while Rep.ind φ lands in Rep.{max u v' w} k H for H : Type v'. Tensoring Rep.ind φ X with Y therefore forces H into the universe of k, exactly as in Mathlib's own Rep.coinvariantsTensorIndHom section; only the source group G stays free.

References

This is the projection formula of Layer 0 in TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, whose Suggested.lean records it as indProjection. See J.-P. Serre, Linear Representations of Finite Groups, §3.3, and C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, §10.

noncomputable def TauCeti.indProjectionHom {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) : Representation.IndV φ (ρ.tprod (MonoidHom.comp τ φ)) →ₗ[k] TensorProduct k (Representation.IndV φ ρ) B

The forward map of the projection formula, ⟦h ⊗ₜ (a ⊗ₜ b)⟧ ↦ ⟦h ⊗ₜ a⟧ ⊗ₜ τ(h⁻¹) b. The twist by τ h⁻¹ is what makes the expression independent of the representative: it undoes the translation of the group coordinate recorded by Representation.Coinvariants.mk_self_apply.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.indProjectionHom_apply_mk {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) (h : H) (a : A) (b : B) : (indProjectionHom φ ρ τ) ((Representation.IndV.mk φ (ρ.tprod (MonoidHom.comp τ φ)) h) (a ⊗ₜ[k] b)) = (Representation.IndV.mk φ ρ h) a ⊗ₜ[k] (τ h⁻¹) b

TauCeti.indProjectionHom on generators. This is the only place the definition is unfolded; every later proof rewrites with this rule instead.

noncomputable def TauCeti.indProjectionInv {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) : TensorProduct k (Representation.IndV φ ρ) B →ₗ[k] Representation.IndV φ (ρ.tprod (MonoidHom.comp τ φ))

The backward map of the projection formula, ⟦h ⊗ₜ a⟧ ⊗ₜ b ↦ ⟦h ⊗ₜ (a ⊗ₜ τ(h) b)⟧.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.indProjectionInv_apply_mk {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) (h : H) (a : A) (b : B) : (indProjectionInv φ ρ τ) ((Representation.IndV.mk φ ρ h) a ⊗ₜ[k] b) = (Representation.IndV.mk φ (ρ.tprod (MonoidHom.comp τ φ)) h) (a ⊗ₜ[k] (τ h) b)

TauCeti.indProjectionInv on generators. This is the only place the definition is unfolded; every later proof rewrites with this rule instead.

noncomputable def TauCeti.indProjectionLEquiv {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) : Representation.IndV φ (ρ.tprod (MonoidHom.comp τ φ)) ≃ₗ[k] TensorProduct k (Representation.IndV φ ρ) B

The projection formula as a k-linear equivalence of the underlying modules: the two maps above are mutually inverse because τ h and τ h⁻¹ cancel.

Equations

• TauCeti.indProjectionLEquiv φ ρ τ = LinearEquiv.ofLinearMap (TauCeti.indProjectionHom φ ρ τ) (TauCeti.indProjectionInv φ ρ τ) ⋯ ⋯

@[simp]

theorem TauCeti.indProjectionLEquiv_apply {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) (x : Representation.IndV φ (ρ.tprod (MonoidHom.comp τ φ))) : (indProjectionLEquiv φ ρ τ) x = (indProjectionHom φ ρ τ) x

TauCeti.indProjectionLEquiv is TauCeti.indProjectionHom in the forward direction.

noncomputable def TauCeti.indProjectionEquiv {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type w} {B : Type w'} [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A) (τ : Representation k H B) : (Representation.ind φ (ρ.tprod (MonoidHom.comp τ φ))).Equiv ((Representation.ind φ ρ).tprod τ)

The projection formula as an equivalence of representations. Equivariance is the computation (h h₁⁻¹)⁻¹ = h₁ h⁻¹: translating the group coordinate on the induced side by h₁⁻¹ on the right is matched by acting with h₁ on the second tensor factor.

Equations

• TauCeti.indProjectionEquiv φ ρ τ = Representation.Equiv.mk (TauCeti.indProjectionLEquiv φ ρ τ) ⋯

noncomputable def TauCeti.indProjection {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) (Y : Rep k H) : Rep.ind φ (CategoryTheory.MonoidalCategoryStruct.tensorObj X (Rep.res φ Y)) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.ind φ X) Y

The projection formula in Rep k H: inducing a representation tensored with a restricted one is the induced representation tensored with the original, Ind_φ (X ⊗ Res_φ Y) ≅ (Ind_φ X) ⊗ Y.

Equations

• TauCeti.indProjection φ X Y = Rep.mkIso (TauCeti.indProjectionEquiv φ X.ρ Y.ρ)

theorem TauCeti.indProjection_hom_hom_apply {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) (Y : Rep k H) (h : H) (x : ↑X) (y : ↑Y) : (Rep.Hom.hom (indProjection φ X Y).hom) ((Representation.IndV.mk φ (CategoryTheory.MonoidalCategoryStruct.tensorObj X (Rep.res φ Y)).ρ h) (x ⊗ₜ[k] y)) = (Representation.IndV.mk φ X.ρ h) x ⊗ₜ[k] (Y.ρ h⁻¹) y

The forward direction of TauCeti.indProjection on generators. Not a simp lemma: simp unfolds the reducible Representation.IndV.mk, so the left-hand side is not in simp-normal form.

theorem TauCeti.indProjection_inv_hom_apply {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) (Y : Rep k H) (h : H) (x : ↑X) (y : ↑Y) : (Rep.Hom.hom (indProjection φ X Y).inv) ((Representation.IndV.mk φ X.ρ h) x ⊗ₜ[k] y) = (Representation.IndV.mk φ (CategoryTheory.MonoidalCategoryStruct.tensorObj X (Rep.res φ Y)).ρ h) (x ⊗ₜ[k] (Y.ρ h) y)

The backward direction of TauCeti.indProjection on generators.

theorem TauCeti.indProjection_hom_naturality_left {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {X X' : Rep k G} (f : X ⟶ X') (Y : Rep k H) : CategoryTheory.CategoryStruct.comp (Rep.indMap φ (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id (Rep.res φ Y)))) (indProjection φ X' Y).hom = CategoryTheory.CategoryStruct.comp (indProjection φ X Y).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (Rep.indMap φ f) (CategoryTheory.CategoryStruct.id Y))

The projection formula is natural in the left tensor factor, the Rep k G argument.

theorem TauCeti.indProjection_hom_naturality_right {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) {Y Y' : Rep k H} (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (Rep.indMap φ (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) ((Rep.resFunctor φ).map g))) (indProjection φ X Y').hom = CategoryTheory.CategoryStruct.comp (indProjection φ X Y).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id (Rep.ind φ X)) g)

The projection formula is natural in the right tensor factor, the Rep k H argument.

noncomputable def TauCeti.indProjectionNatIsoLeft {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (Y : Rep k H) : ((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).flip.obj (Rep.res φ Y)).comp (Rep.indFunctor k φ) ≅ (Rep.indFunctor k φ).comp ((CategoryTheory.MonoidalCategory.curriedTensor (Rep k H)).flip.obj Y)

The projection formula as a natural isomorphism in the left tensor factor: the functors X ↦ Ind_φ (X ⊗ Res_φ Y) and X ↦ (Ind_φ X) ⊗ Y from Rep k G to Rep k H agree.

Equations

• TauCeti.indProjectionNatIsoLeft φ Y = CategoryTheory.NatIso.ofComponents (fun (X : Rep k G) => TauCeti.indProjection φ X Y) ⋯

noncomputable def TauCeti.indProjectionNatIsoRight {k : Type u} {G : Type v} {H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) : (Rep.resFunctor φ).comp (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).obj X).comp (Rep.indFunctor k φ)) ≅ (CategoryTheory.MonoidalCategory.curriedTensor (Rep k H)).obj (Rep.ind φ X)

The projection formula as a natural isomorphism in the right tensor factor: the endofunctors Y ↦ Ind_φ (X ⊗ Res_φ Y) and Y ↦ (Ind_φ X) ⊗ Y of Rep k H agree. This is the shape of Mathlib's coinvariants version Rep.coinvariantsTensorIndNatIso.

Equations

• TauCeti.indProjectionNatIsoRight φ X = CategoryTheory.NatIso.ofComponents (TauCeti.indProjection φ X) ⋯

theorem TauCeti.coinvariantsTensorIndHom_map_indProjection_mk {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) (Y : Rep k H) (h : H) (x : ↑X) (y : ↑Y) : (ModuleCat.Hom.hom (Rep.coinvariantsTensorIndHom φ X Y)) ((ModuleCat.Hom.hom ((Rep.coinvariantsFunctor k H).map (indProjection φ X Y).hom)) ((Representation.Coinvariants.mk (Rep.ind φ (CategoryTheory.MonoidalCategoryStruct.tensorObj X (Rep.res φ Y))).ρ) ((Representation.IndV.mk φ (CategoryTheory.MonoidalCategoryStruct.tensorObj X (Rep.res φ Y)).ρ h) (x ⊗ₜ[k] y)))) = (Representation.Coinvariants.mk (X.ρ.tprod (Rep.res φ Y).ρ)) (x ⊗ₜ[k] y)

The comparison with Mathlib's coinvariants shadow. Applying H-coinvariants to TauCeti.indProjection and composing with Rep.coinvariantsTensorIndHom sends the class of a generator ⟦h ⊗ₜ z⟧ to ⟦z⟧, with no trace of h left: the twist Y.ρ h⁻¹ introduced by the projection formula is absorbed by the coinvariants relation.

This computes that one composite on generators; it is not an equality of the two isomorphisms, which do not have the same source and target: Rep.coinvariantsTensorIndHom runs from the coinvariants of (Ind_φ X) ⊗ Y to the coinvariants of X ⊗ Res_φ Y downstairs, while TauCeti.indProjection is an isomorphism in Rep k H upstairs.