Isomorphism of representations and of the modules they carry

Mathlib's Representation.IntertwiningMap.equivLinearMapAsModule identifies the intertwining maps ρ → σ with the k[G]-linear maps ρ.asModule → σ.asModule, but not the isomorphisms with the isomorphisms: an equivalence of representations is a bijective intertwining map, while a linear equivalence of modules carries its inverse as data. This file supplies the missing dictionary, in both directions and in the form that is usually wanted, an equivalence of Nonemptys.

The point of the dictionary is that classification statements are naturally proved on one side and used on the other. The isomorphism classes of simple k[G]-modules are what the semisimple-algebra theory counts, while the objects being classified are representations.

Main results

• Representation.asModuleEquiv_apply, Representation.asModuleEquiv_symm_apply, Representation.IntertwiningMap.equivLinearMapAsModule_apply, and Representation.IntertwiningMap.equivLinearMapAsModule_symm_apply: evaluation of the two identifications Mathlib leaves definitional, the one of ρ.asModule with V and the one between intertwining maps and k[G]-linear maps, in both directions.
• Representation.finrank_moduleCat_asModule: bundling the attached module and restricting scalars preserves the dimension of the representation.
• TauCeti.Representation.equivOfAsModuleLinearEquiv: a k[G]-linear isomorphism ρ.asModule ≃ₗ σ.asModule is an equivalence of representations.
• TauCeti.Representation.asModuleLinearEquivOfEquiv: the converse.
• TauCeti.Representation.nonempty_equiv_iff: the two notions of isomorphism agree.
• Representation.prodAsModuleEquiv: the module of a product of representations is the product of their modules.
• Representation.linearEquivAsModuleComp: an isomorphism onto ρ.asModule restricts along f : H →* G to an isomorphism onto (ρ.comp f).asModule.
• TauCeti.fdRepIsoOfAsModuleLinearEquiv: over a commutative ring, and for module-finite carriers, such an isomorphism of modules is an isomorphism of the objects of FDRep k G that the representations name.
• TauCeti.nonempty_fdRepIso_iff: the two notions of isomorphism agree on FDRep k G, so a classification proved for representations reads off as a classification of objects.
• TauCeti.toSkeleton_fdRepOf_toRepresentation_eq_iff: two subrepresentations determine the same module-finite representation class exactly when their associated submodules are linearly equivalent.

@[simp]

theorem Representation.finrank_moduleCat_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Module.finrank k ↑↧ρ.asModule = Module.finrank k V

Bundling the group-algebra module of a representation and restricting scalars to the coefficient field preserves its dimension. The scalar structure supplied by ModuleCat is restriction along algebraMap, rather than the original structure on ρ.asModule.

@[simp]

theorem Representation.asModuleEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} (x : ρ.asModule) : ρ.asModuleEquiv x = x

Evaluation of the identification of ρ.asModule with V. Representation.asModuleEquiv is the identity map of the underlying type, so it may be erased from an application; naming that fact keeps proofs that cross the type synonym from unfolding it.

@[simp]

theorem Representation.asModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} (x : V) : ρ.asModuleEquiv.symm x = x

Evaluation of the inverse identification of ρ.asModule with V.

@[simp]

theorem Representation.IntertwiningMap.equivLinearMapAsModule_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (x : ρ.asModule) : ((equivLinearMapAsModule ρ σ) f) x = f x

Evaluation of the k[G]-linear map attached to an intertwining map. The map Representation.IntertwiningMap.equivLinearMapAsModule ρ σ f is f itself on the underlying types, so it too may be erased from an application.

@[simp]

theorem Representation.IntertwiningMap.equivLinearMapAsModule_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.asModule →ₗ[MonoidAlgebra k G] σ.asModule) (v : V) : ((equivLinearMapAsModule ρ σ).symm f) v = σ.asModuleEquiv (f (ρ.asModuleEquiv.symm v))

Evaluation of the intertwining map attached to a k[G]-linear map. This is the inverse direction of Representation.IntertwiningMap.equivLinearMapAsModule_apply, with the changes of underlying type made explicit by Representation.asModuleEquiv.

noncomputable def TauCeti.Representation.equivOfAsModuleLinearEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule) : ρ.Equiv σ

A k[G]-linear isomorphism of the attached modules is an equivalence of representations. This reads Representation.IntertwiningMap.equivLinearMapAsModule backwards: the k[G]-linear map underlying f is an intertwining map, and it is bijective.

Equations

• TauCeti.Representation.equivOfAsModuleLinearEquiv f = ((Representation.IntertwiningMap.equivLinearMapAsModule ρ σ).symm ↑f).ofBijective ⋯

@[simp]

theorem TauCeti.Representation.equivOfAsModuleLinearEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule) (v : V) : (equivOfAsModuleLinearEquiv f) v = σ.asModuleEquiv (f (ρ.asModuleEquiv.symm v))

noncomputable def TauCeti.Representation.asModuleLinearEquivOfEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) : ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule

**An equivalence of representations is a k[G]-linear isomorphism of the attached modules.** The inverse of TauCeti.Representation.equivOfAsModuleLinearEquiv; the underlying map is the one Representation.IntertwiningMap.equivLinearMapAsModule` attaches to the intertwining map.

Equations

• TauCeti.Representation.asModuleLinearEquivOfEquiv φ = LinearEquiv.ofBijective ((Representation.IntertwiningMap.equivLinearMapAsModule ρ σ) ↑φ) ⋯

@[simp]

theorem TauCeti.Representation.asModuleLinearEquivOfEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) (x : ρ.asModule) : (asModuleLinearEquivOfEquiv φ) x = σ.asModuleEquiv.symm (φ (ρ.asModuleEquiv x))

@[simp]

theorem TauCeti.Representation.equivOfAsModuleLinearEquiv_asModuleLinearEquivOfEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) : equivOfAsModuleLinearEquiv (asModuleLinearEquivOfEquiv φ) = φ

@[simp]

theorem TauCeti.Representation.asModuleLinearEquivOfEquiv_equivOfAsModuleLinearEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule) : asModuleLinearEquivOfEquiv (equivOfAsModuleLinearEquiv f) = f

theorem TauCeti.Representation.nonempty_equiv_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} : Nonempty (ρ.Equiv σ) ↔ Nonempty (ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule)

The two notions of isomorphism agree. Two representations are equivalent exactly when the k[G]-modules they carry are isomorphic.

noncomputable def Representation.prodAsModuleEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.prod σ).asModule ≃ₗ[MonoidAlgebra k G] ρ.asModule × σ.asModule

The module of a product representation is equivalent to the product of the modules.

Equations

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

@[simp]

theorem Representation.prodAsModuleEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (x : (ρ.prod σ).asModule) : (ρ.prodAsModuleEquiv σ) x = (ρ.asModuleEquiv.symm x.1, σ.asModuleEquiv.symm x.2)

@[simp]

theorem Representation.prodAsModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (x : ρ.asModule × σ.asModule) : (ρ.prodAsModuleEquiv σ).symm x = (ρ.prod σ).asModuleEquiv.symm (ρ.asModuleEquiv x.1, σ.asModuleEquiv x.2)

noncomputable def Representation.linearEquivAsModuleComp {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {H : Type u_5} {Q : Type u_6} [Monoid H] [AddCommMonoid Q] [Module (MonoidAlgebra k G) Q] [Module (MonoidAlgebra k H) Q] (f : H →* G) (hQ : ∀ (a : MonoidAlgebra k H) (q : Q), a • q = (MonoidAlgebra.mapDomainRingHom k f) a • q) (e : Q ≃ₗ[MonoidAlgebra k G] ρ.asModule) : Q ≃ₗ[MonoidAlgebra k H] asModule (MonoidHom.comp ρ f)

Restricting an isomorphism onto ρ.asModule along a monoid homomorphism. If f : H →* G and k[H] acts on Q through f, then a k[G]-linear isomorphism Q ≃ ρ.asModule is also a k[H]-linear isomorphism Q ≃ (ρ.comp f).asModule.

Equations

• ρ.linearEquivAsModuleComp f hQ e = { toFun := ⇑e, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Representation.linearEquivAsModuleComp_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {H : Type u_5} {Q : Type u_6} [Monoid H] [AddCommMonoid Q] [Module (MonoidAlgebra k G) Q] [Module (MonoidAlgebra k H) Q] (f : H →* G) (hQ : ∀ (a : MonoidAlgebra k H) (q : Q), a • q = (MonoidAlgebra.mapDomainRingHom k f) a • q) (e : Q ≃ₗ[MonoidAlgebra k G] ρ.asModule) (q : Q) : (ρ.linearEquivAsModuleComp f hQ e) q = e q

@[simp]

theorem Representation.linearEquivAsModuleComp_symm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {H : Type u_5} {Q : Type u_6} [Monoid H] [AddCommMonoid Q] [Module (MonoidAlgebra k G) Q] [Module (MonoidAlgebra k H) Q] (f : H →* G) (hQ : ∀ (a : MonoidAlgebra k H) (q : Q), a • q = (MonoidAlgebra.mapDomainRingHom k f) a • q) (e : Q ≃ₗ[MonoidAlgebra k G] ρ.asModule) (v : V) : (ρ.linearEquivAsModuleComp f hQ e).symm v = e.symm v

noncomputable def TauCeti.fdRepIsoOfAsModuleLinearEquiv {k V W : Type u} {G : Type v} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [Module.Finite k V] [AddCommGroup W] [Module k W] [Module.Finite k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.asModule ≃ₗ[MonoidAlgebra k G] σ.asModule) : FDRep.of ρ ≅ FDRep.of σ

A k[G]-linear isomorphism of the attached modules is an isomorphism in FDRep k G. The finitely generated representations are a full subcategory of Rep k G, where an equivalence of representations is already an isomorphism.

Equations

• TauCeti.fdRepIsoOfAsModuleLinearEquiv f = (CategoryTheory.forget₂ (FDRep k G) (Rep k G)).preimageIso (Rep.mkIso (TauCeti.Representation.equivOfAsModuleLinearEquiv f))

theorem TauCeti.nonempty_fdRepIso_iff {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : FDRep k G} : Nonempty (X ≅ Y) ↔ Nonempty (Representation.Equiv X.ρ Y.ρ)

The two notions of isomorphism agree on FDRep k G. Two objects are isomorphic exactly when the representations they carry are equivalent, so a classification of representations up to equivalence is a classification of the objects of FDRep k G up to isomorphism.

theorem TauCeti.toSkeleton_fdRepOf_toRepresentation_eq_iff {G : Type v} [Monoid G] {K X : Type u} [CommRing K] [AddCommGroup X] [Module K X] {π : Representation K G X} (S T : Subrepresentation π) [Module.Finite K ↥S.toSubmodule] [Module.Finite K ↥T.toSubmodule] : CategoryTheory.toSkeleton (FDRep.of S.toRepresentation) = CategoryTheory.toSkeleton (FDRep.of T.toRepresentation) ↔ Nonempty (↥S.asSubmodule ≃ₗ[MonoidAlgebra K G] ↥T.asSubmodule)

The module-finite representation classes carried by two subrepresentations agree exactly when their associated group-algebra submodules are linearly equivalent.