Intertwining maps along a homomorphism of monoids

Mathlib's Representation.IsIntertwiningMap compares two representations of one and the same monoid. For a homomorphism f : G →* H, a linear map intertwining ρ : Representation R G V with σ.comp f, for σ : Representation R H W, is the same datum as a morphism of G-representations M ⟶ Res(f)(N), and, when f is an isomorphism, also as a morphism Res(f⁻¹)(M) ⟶ N of H-representations. This file supplies those two adapters, the identity, composition and inversion lemmas for intertwining maps along a homomorphism of monoids, and the compatibility of such a map with the norm ∑ g, ρ g of a finite group.

These are the general representation-theoretic inputs of a change-of-group map in group homology and cohomology: groupHomology.chainsMap consumes the first adapter and groupCohomology.cochainsMap the second.

The file also records that restricting a trivial representation along a homomorphism of monoids gives a trivial representation, so that Rep.res f A carries an IsTrivial instance whenever A does.

Restriction along composites agrees with successive restriction as an equality of functors, and restriction along a monoid isomorphism is an equivalence of representation categories.

Main definitions

• Representation.IsIntertwiningMap.toRes: an intertwining map along f : G →* H read as a morphism M ⟶ Res(f)(N) of G-representations.
• Representation.IsIntertwiningMap.ofRes: an intertwining map along an isomorphism e : G ≃* H read as a morphism Res(e⁻¹)(M) ⟶ N of H-representations.
• MulEquiv.resFunctorEquiv: the equivalence induced by restriction along a monoid isomorphism.

Main results

• MonoidHom.resFunctor_comp: restriction along a composite is successive restriction.
• MonoidHom.resFunctor_id: restriction along the identity is the identity functor.
• Representation.isTrivial_comp: the restriction of a trivial representation along a homomorphism of monoids is trivial; in particular Rep.res f A is trivial when A is.
• Representation.IsIntertwiningMap.trans and Representation.IsIntertwiningMap.symm: intertwining maps along homomorphisms of monoids compose, and invert along an isomorphism when their linear part is an equivalence.
• Representation.IsIntertwiningMap.comp_norm: an intertwining map along an isomorphism of finite groups intertwines the two norms.
• Representation.IsIntertwiningMap.tensor: the tensor product of two intertwining maps along one homomorphism of monoids is intertwining along it.
• Rep.isIntertwiningMap_tensor_res: restriction and tensor products are compatible along a homomorphism of monoids.
• Rep.isIntertwiningMap_trivial: the identity intertwines trivial representations along any homomorphism of monoids.
• Rep.isIntertwiningMap_id and Rep.isIntertwiningMap_res: the identity map is intertwining along the identity isomorphism of the monoid, and along f between a restricted representation and the representation it restricts.
• Rep.isIntertwiningMap_res_res and Rep.isIntertwiningMap_res_res_toRes_naturality: the identity map is intertwining between the restrictions along two factorisations of one homomorphism, naturally in the representation.

theorem Representation.IsIntertwiningMap.trans {R : Type u} {G : Type uG} {H : Type uH} {K : Type uK} {V : Type uV} {W : Type uW} {U : Type uU} [Semiring R] [Monoid G] [Monoid H] [Monoid K] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] [AddCommMonoid U] [Module R U] {ρ : Representation R G V} {σ : Representation R H W} {τ : Representation R K U} {f : G →* H} {φ : V →ₗ[R] W} (hφ : ρ.IsIntertwiningMap (MonoidHom.comp σ f) φ) {g : H →* K} {ψ : W →ₗ[R] U} (hψ : σ.IsIntertwiningMap (MonoidHom.comp τ g) ψ) : ρ.IsIntertwiningMap (MonoidHom.comp τ (g.comp f)) (ψ ∘ₗ φ)

Intertwining maps along homomorphisms of monoids compose.

theorem Representation.IsIntertwiningMap.symm {R : Type u} {G : Type uG} {H : Type uH} {V : Type uV} {W : Type uW} [Semiring R] [Monoid G] [Monoid H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R H W} {e : G ≃* H} {e' : V ≃ₗ[R] W} (he : ρ.IsIntertwiningMap (MonoidHom.comp σ ↑e) ↑e') : σ.IsIntertwiningMap (MonoidHom.comp ρ ↑e.symm) ↑e'.symm

The inverse of an intertwining map along an isomorphism of monoids is intertwining, when its linear part is an equivalence.

instance Representation.isTrivial_comp {R : Type u} {G : Type uG} {H : Type uH} {W : Type uW} [Semiring R] [Monoid G] [Monoid H] [AddCommMonoid W] [Module R W] (σ : Representation R H W) [σ.IsTrivial] (f : G →* H) : IsTrivial (MonoidHom.comp σ f)

The restriction of a trivial representation along a homomorphism of monoids is trivial.

theorem Representation.invariants_le_invariants_comp_subtype {R : Type u_1} {G : Type u_2} {V : Type u_3} [Group G] [CommRing R] [AddCommGroup V] [Module R V] {ρ : Representation R G V} {H : Subgroup G} : ρ.invariants ≤ invariants (MonoidHom.comp ρ H.subtype)

A G-invariant element is H-invariant.

theorem Representation.IsIntertwiningMap.comp_norm {R : Type u} {G : Type uG} {H : Type uH} {V : Type uV} {W : Type uW} [Semiring R] [Group G] [Group H] [Fintype G] [Fintype H] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] {ρ : Representation R G V} {σ : Representation R H W} {e : G ≃* H} {φ : V →ₗ[R] W} (hφ : ρ.IsIntertwiningMap (MonoidHom.comp σ ↑e) φ) : φ ∘ₗ ρ.norm = σ.norm ∘ₗ φ

An intertwining map along an isomorphism of finite groups intertwines the two norms. The group isomorphism permutes the summands of ∑ g, ρ g.

theorem Rep.isIntertwiningMap_id {R : Type u} {G : Type uG} [Semiring R] [Monoid G] (M : Rep R G) : M.ρ.IsIntertwiningMap (MonoidHom.comp M.ρ ↑(MulEquiv.refl G)) LinearMap.id

The identity map of a representation is intertwining along the identity isomorphism of its monoid.

theorem Rep.isIntertwiningMap_res {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] (N : Rep R H) (f : G →* H) : (res f N).ρ.IsIntertwiningMap (MonoidHom.comp N.ρ f) ↑(LinearEquiv.refl R ↑N)

Restricting the coefficients along f and comparing back by the identity is an intertwining map along f.

theorem Rep.isIntertwiningMap_trivial {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] (V : Type uV) [AddCommGroup V] [Module R V] (f : G →* H) : (trivial R G V).ρ.IsIntertwiningMap (MonoidHom.comp (trivial R H V).ρ f) ↑(LinearEquiv.refl R V)

The identity of V intertwines the trivial representations on V along any homomorphism of monoids.

theorem Rep.isIntertwiningMap_res_res {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {K : Type uK} {L : Type uL} [Monoid K] [Monoid L] (N : Rep R H) {f₁ : K →* G} {f₂ : G →* H} {g₁ : K →* L} {g₂ : L →* H} (hfg : g₂.comp g₁ = f₂.comp f₁) : (res f₁ (res f₂ N)).ρ.IsIntertwiningMap (MonoidHom.comp (res g₂ N).ρ g₁) LinearMap.id

The identity of N is intertwining along g₁ from Res(f₁)(Res(f₂)(N)) to Res(g₂)(N) when g₂ ∘ g₁ = f₂ ∘ f₁; its toRes is the comparison morphism Res(f₁)(Res(f₂)(N)) ⟶ Res(g₁)(Res(g₂)(N)) of K-representations.

def Representation.IsIntertwiningMap.toRes {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {M : Rep R G} {N : Rep R H} {φ : ↑M →ₗ[R] ↑N} {f : G →* H} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ f) φ) : M ⟶ Rep.res f N

An intertwining map along f : G →* H read as a morphism M ⟶ Res(f)(N) of G-representations. This is the datum that groupHomology.chainsMap consumes.

Equations

• hφ.toRes = Rep.ofHom { toLinearMap := φ, isIntertwining' := ⋯ }

def Representation.IsIntertwiningMap.ofRes {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {M : Rep R G} {N : Rep R H} {φ : ↑M →ₗ[R] ↑N} {e : G ≃* H} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ ↑e) φ) : Rep.res (↑e.symm) M ⟶ N

An intertwining map along an isomorphism e : G ≃* H read as a morphism Res(e⁻¹)(M) ⟶ N of H-representations. This is the datum that groupCohomology.cochainsMap consumes.

Equations

• hφ.ofRes = Rep.ofHom { toLinearMap := φ, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IsIntertwiningMap.toRes_hom_toLinearMap {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {M : Rep R G} {N : Rep R H} {φ : ↑M →ₗ[R] ↑N} {f : G →* H} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ f) φ) : (Rep.Hom.hom hφ.toRes).toLinearMap = φ

@[simp]

theorem Representation.IsIntertwiningMap.toRes_hom_apply {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {M : Rep R G} {N : Rep R H} {φ : ↑M →ₗ[R] ↑N} {f : G →* H} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ f) φ) (v : ↑M) : (Rep.Hom.hom hφ.toRes) v = φ v

toRes hφ acts on vectors as φ. The coercion is stated at IntertwiningMap M.ρ (N.ρ.comp f), simp's normal form of IntertwiningMap M.ρ (Rep.res f N).ρ, so that simp can use this lemma.

@[simp]

theorem Representation.IsIntertwiningMap.ofRes_hom_toLinearMap {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {M : Rep R G} {N : Rep R H} {φ : ↑M →ₗ[R] ↑N} {e : G ≃* H} (hφ : M.ρ.IsIntertwiningMap (MonoidHom.comp N.ρ ↑e) φ) : (Rep.Hom.hom hφ.ofRes).toLinearMap = φ

theorem Rep.isIntertwiningMap_res_res_toRes_naturality {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {K : Type uK} {L : Type uL} [Monoid K] [Monoid L] {f₁ : K →* G} {f₂ : G →* H} {g₁ : K →* L} {g₂ : L →* H} (hfg : g₂.comp g₁ = f₂.comp f₁) {N N' : Rep R H} (ψ : N ⟶ N') : CategoryTheory.CategoryStruct.comp ⋯.toRes ((resFunctor g₁).map ((resFunctor g₂).map ψ)) = CategoryTheory.CategoryStruct.comp ((resFunctor f₁).map ((resFunctor f₂).map ψ)) ⋯.toRes

The comparison morphisms (isIntertwiningMap_res_res N hfg).toRes from Res(f₁)(Res(f₂)(N)) to Res(g₁)(Res(g₂)(N)) are natural in N. The square is oriented like the comm₁₂ field τ₁ ≫ S₂.f = S₁.f ≫ τ₂ of a morphism of short complexes.

theorem Rep.isIntertwiningMap_res_res_toRes_naturality_assoc {R : Type u} {G : Type uG} {H : Type uH} [Semiring R] [Monoid G] [Monoid H] {K : Type uK} {L : Type uL} [Monoid K] [Monoid L] {f₁ : K →* G} {f₂ : G →* H} {g₁ : K →* L} {g₂ : L →* H} (hfg : g₂.comp g₁ = f₂.comp f₁) {N N' : Rep R H} (ψ : N ⟶ N') {Z : Rep R K} (h : of ((MonoidHom.comp N'.ρ g₂).comp g₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp ⋯.toRes (CategoryTheory.CategoryStruct.comp (resMap g₁ (resMap g₂ ψ)) h) = CategoryTheory.CategoryStruct.comp (resMap f₁ (resMap f₂ ψ)) (CategoryTheory.CategoryStruct.comp ⋯.toRes h)

The comparison morphisms (isIntertwiningMap_res_res N hfg).toRes from Res(f₁)(Res(f₂)(N)) to Res(g₁)(Res(g₂)(N)) are natural in N. The square is oriented like the comm₁₂ field τ₁ ≫ S₂.f = S₁.f ≫ τ₂ of a morphism of short complexes.

theorem Representation.IsIntertwiningMap.tensor {R : Type u} {G : Type uG} {H : Type uH} [CommRing R] [Monoid G] [Monoid H] {f : G →* H} {M₁ M₂ : Rep R G} {N₁ N₂ : Rep R H} {φ₁ : ↑M₁ →ₗ[R] ↑N₁} {φ₂ : ↑M₂ →ₗ[R] ↑N₂} (h₁ : M₁.ρ.IsIntertwiningMap (MonoidHom.comp N₁.ρ f) φ₁) (h₂ : M₂.ρ.IsIntertwiningMap (MonoidHom.comp N₂.ρ f) φ₂) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂).ρ.IsIntertwiningMap (MonoidHom.comp (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁ N₂).ρ f) (TensorProduct.map φ₁ φ₂)

The tensor product of two intertwining maps along one homomorphism of monoids f is intertwining along f. This is Mathlib's Representation.IntertwiningMap.tensor, stated for intertwining maps along a homomorphism.

theorem Rep.isIntertwiningMap_tensor_res {R : Type u} {G : Type uG} {H : Type uH} [CommRing R] [Monoid G] [Monoid H] (N₁ N₂ : Rep R H) (f : G →* H) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (res f N₁) (res f N₂)).ρ.IsIntertwiningMap (MonoidHom.comp (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁ N₂).ρ f) (TensorProduct.map ↑(LinearEquiv.refl R ↑N₁) ↑(LinearEquiv.refl R ↑N₂))

Restriction and tensor products are compatible: the tensor product of the identity maps from the restricted representations to their originals intertwines the actions along f.

theorem MonoidHom.resFunctor_comp {k : Type u} [Semiring k] {H : Type u_1} {K : Type u_2} {L : Type u_3} [Monoid H] [Monoid K] [Monoid L] (φ : K →* L) (ψ : H →* K) : Rep.resFunctor (φ.comp ψ) = (Rep.resFunctor φ).comp (Rep.resFunctor ψ)

Restricting representations along a composite homomorphism is restricting twice over. Mathlib has no equality of this shape (Action.resComp is the natural isomorphism for Action), so we record the equality form, which keeps the reduction out of proofs that state equalities of restriction functors.

theorem MonoidHom.resFunctor_id {k : Type u} [Semiring k] {H : Type u_1} [Monoid H] : Rep.resFunctor (id H) = CategoryTheory.Functor.id (Rep k H)

Restricting along the identity is the identity functor.

def MulEquiv.resFunctorEquiv {k : Type u} [Semiring k] {H : Type u_1} {K : Type u_2} [Monoid H] [Monoid K] (e : H ≃* K) : Rep k K ≌ Rep k H

Restriction along a monoid isomorphism is an equivalence of categories, with inverse restriction along the inverse isomorphism. This is the Rep analogue of Mathlib's Action.resEquiv, which does not apply because Rep is a structure rather than an Action.

Its two functors are identified with restriction by MulEquiv.resFunctorEquiv_functor and MulEquiv.resFunctorEquiv_inverse.

Equations

• e.resFunctorEquiv = CategoryTheory.Equivalence.mk (Rep.resFunctor e.toMonoidHom) (Rep.resFunctor e.symm.toMonoidHom) (CategoryTheory.eqToIso ⋯) (CategoryTheory.eqToIso ⋯)

@[simp]

theorem MulEquiv.resFunctorEquiv_functor {k : Type u} [Semiring k] {H : Type u_1} {K : Type u_2} [Monoid H] [Monoid K] (e : H ≃* K) : e.resFunctorEquiv.functor = Rep.resFunctor e.toMonoidHom

The forward functor of the restriction equivalence is restriction along the isomorphism.

@[simp]

theorem MulEquiv.resFunctorEquiv_inverse {k : Type u} [Semiring k] {H : Type u_1} {K : Type u_2} [Monoid H] [Monoid K] (e : H ≃* K) : e.resFunctorEquiv.inverse = Rep.resFunctor e.symm.toMonoidHom

The inverse functor of the restriction equivalence is restriction along the inverse.