Equivalences of permutation representations

For a monoid G, equivariantly equivalent G-sets carry equivalent permutation representations, and the permutation representation on a disjoint union is the product of the representations on its two pieces.

For a group G and a subgroup H, the permutation representation k[G ⧸ H] interpolates between the two extremes H = ⊤ and H = ⊥. This file identifies those extremes: the cosets of the whole group carry the trivial representation, and the cosets of the trivial subgroup carry the left regular representation.

Both identifications go through ofMulActionIsoCongr, which turns a G-equivariant equivalence of G-sets into an isomorphism of the permutation representations they carry.

Main definitions

• TauCeti.ofMulActionIsoCongr: an equivariant equivalence of G-sets induces an isomorphism of permutation representations.
• TauCeti.ofMulActionSumEquiv: the permutation representation on a disjoint union is the product of the permutation representations on the pieces.
• TauCeti.quotientIsoCongr: equal subgroups give isomorphic permutation representations.
• TauCeti.quotientTopIsoTrivial: k[G ⧸ ⊤] ≅ k with the trivial action.
• TauCeti.quotientBotIsoLeftRegular: k[G ⧸ ⊥] ≅ k[G] with the left regular action.

The equivalences and isomorphisms come with lemmas reading them and their inverses on basis elements. For the coset representations, these bases are indexed by G ⧸ H.

noncomputable def TauCeti.ofMulActionEquivCongr {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) : (Representation.ofMulAction k G X).Equiv (Representation.ofMulAction k G Y)

A G-equivariant equivalence of G-sets induces an equivalence of the permutation representations on their free modules.

Equations

• TauCeti.ofMulActionEquivCongr k e he = Representation.Equiv.mk (MonoidAlgebra.mapDomainLinearEquiv k k e) ⋯

@[simp]

theorem TauCeti.ofMulActionEquivCongr_apply_single {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) (x : X) (r : k) : (ofMulActionEquivCongr k e he) (MonoidAlgebra.single x r) = MonoidAlgebra.single (e x) r

@[simp]

theorem TauCeti.ofMulActionEquivCongr_symm_apply_single {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) (y : Y) (r : k) : (ofMulActionEquivCongr k e he).symm (MonoidAlgebra.single y r) = MonoidAlgebra.single (e.symm y) r

noncomputable def TauCeti.ofMulActionSumEquiv {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] : (Representation.ofMulAction k G (X ⊕ Y)).Equiv ((Representation.ofMulAction k G X).prod (Representation.ofMulAction k G Y))

The permutation representation on a disjoint union of G-sets is the product of the permutation representations on the two pieces.

Equations

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

@[simp]

theorem TauCeti.ofMulActionSumEquiv_apply_single_inl {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (x : X) (r : k) : (ofMulActionSumEquiv k) (MonoidAlgebra.single (Sum.inl x) r) = (MonoidAlgebra.single x r, 0)

@[simp]

theorem TauCeti.ofMulActionSumEquiv_apply_single_inr {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (y : Y) (r : k) : (ofMulActionSumEquiv k) (MonoidAlgebra.single (Sum.inr y) r) = (0, MonoidAlgebra.single y r)

@[simp]

theorem TauCeti.ofMulActionSumEquiv_symm_apply_single_inl {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (x : X) (r : k) : (ofMulActionSumEquiv k).symm (MonoidAlgebra.single x r, 0) = MonoidAlgebra.single (Sum.inl x) r

@[simp]

theorem TauCeti.ofMulActionSumEquiv_symm_apply_single_inr {G : Type v} [Monoid G] (k : Type u) [Semiring k] {X : Type w} {Y : Type w'} [MulAction G X] [MulAction G Y] (y : Y) (r : k) : (ofMulActionSumEquiv k).symm (0, MonoidAlgebra.single y r) = MonoidAlgebra.single (Sum.inr y) r

noncomputable def TauCeti.ofMulActionIsoCongr {G : Type v} [Monoid G] (k : Type u) [Ring k] {X Y : Type w} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) : Rep.ofMulAction k G X ≅ Rep.ofMulAction k G Y

A G-equivariant equivalence of G-sets induces an isomorphism of the permutation representations they carry.

Equations

• TauCeti.ofMulActionIsoCongr k e he = Rep.mkIso (TauCeti.ofMulActionEquivCongr k e he)

@[simp]

theorem TauCeti.ofMulActionIsoCongr_hom_hom_single {G : Type v} [Monoid G] (k : Type u) [Ring k] {X Y : Type w} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) (x : X) (r : k) : (Rep.Hom.hom (ofMulActionIsoCongr k e he).hom) (MonoidAlgebra.single x r) = MonoidAlgebra.single (e x) r

@[simp]

theorem TauCeti.ofMulActionIsoCongr_inv_hom_single {G : Type v} [Monoid G] (k : Type u) [Ring k] {X Y : Type w} [MulAction G X] [MulAction G Y] (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = g • e x) (y : Y) (r : k) : (Rep.Hom.hom (ofMulActionIsoCongr k e he).inv) (MonoidAlgebra.single y r) = MonoidAlgebra.single (e.symm y) r

noncomputable def TauCeti.quotientIsoCongr (k : Type u) [Ring k] {G : Type v} [Group G] {H K : Subgroup G} (h : H = K) : Rep.ofMulAction k G (G ⧸ H) ≅ Rep.ofMulAction k G (G ⧸ K)

Equal subgroups have the same cosets, so they carry isomorphic permutation representations.

Equations

• TauCeti.quotientIsoCongr k h = TauCeti.ofMulActionIsoCongr k (Subgroup.quotientEquivOfEq h) ⋯

@[simp]

theorem TauCeti.quotientIsoCongr_hom_hom_single (k : Type u) [Ring k] {G : Type v} [Group G] {H K : Subgroup G} (h : H = K) (q : G ⧸ H) (r : k) : (Rep.Hom.hom (quotientIsoCongr k h).hom) (MonoidAlgebra.single q r) = MonoidAlgebra.single ((Subgroup.quotientEquivOfEq h) q) r

@[simp]

theorem TauCeti.quotientIsoCongr_inv_hom_single (k : Type u) [Ring k] {G : Type v} [Group G] {H K : Subgroup G} (h : H = K) (q : G ⧸ K) (r : k) : (Rep.Hom.hom (quotientIsoCongr k h).inv) (MonoidAlgebra.single q r) = MonoidAlgebra.single ((Subgroup.quotientEquivOfEq ⋯) q) r

theorem TauCeti.quotientIsoCongr_hom_hom_single_mk (k : Type u) [Ring k] {G : Type v} [Group G] {H K : Subgroup G} (h : H = K) (x : G) (r : k) : (Rep.Hom.hom (quotientIsoCongr k h).hom) (MonoidAlgebra.single (↑x) r) = MonoidAlgebra.single (↑x) r

The basis element indexed by the coset of a representative, in the forward direction.

theorem TauCeti.quotientIsoCongr_inv_hom_single_mk (k : Type u) [Ring k] {G : Type v} [Group G] {H K : Subgroup G} (h : H = K) (x : G) (r : k) : (Rep.Hom.hom (quotientIsoCongr k h).inv) (MonoidAlgebra.single (↑x) r) = MonoidAlgebra.single (↑x) r

The basis element indexed by the coset of a representative, in the inverse direction.

noncomputable def TauCeti.quotientBotIsoLeftRegular (k : Type u) [Ring k] {G : Type v} [Group G] : Rep.ofMulAction k G (G ⧸ ⊥) ≅ Rep.leftRegular k G

The permutation representation of G on the cosets of the trivial subgroup is the left regular representation.

Equations

• TauCeti.quotientBotIsoLeftRegular k = TauCeti.ofMulActionIsoCongr k QuotientGroup.quotientBot.toEquiv ⋯

@[simp]

theorem TauCeti.quotientBotIsoLeftRegular_hom_hom_single (k : Type u) [Ring k] {G : Type v} [Group G] (q : G ⧸ ⊥) (r : k) : (Rep.Hom.hom (quotientBotIsoLeftRegular k).hom) (MonoidAlgebra.single q r) = MonoidAlgebra.single (QuotientGroup.quotientBot q) r

theorem TauCeti.quotientBotIsoLeftRegular_hom_hom_single_mk (k : Type u) [Ring k] {G : Type v} [Group G] (x : G) (r : k) : (Rep.Hom.hom (quotientBotIsoLeftRegular k).hom) (MonoidAlgebra.single (↑x) r) = MonoidAlgebra.single x r

The basis element indexed by the coset of a representative is sent to that representative.

@[simp]

theorem TauCeti.quotientBotIsoLeftRegular_inv_hom_single (k : Type u) [Ring k] {G : Type v} [Group G] (x : G) (r : k) : (Rep.Hom.hom (quotientBotIsoLeftRegular k).inv) (MonoidAlgebra.single x r) = MonoidAlgebra.single (↑x) r

noncomputable def TauCeti.quotientTopIsoTrivial (k : Type u) [Ring k] {G : Type u} [Group G] : Rep.ofMulAction k G (G ⧸ ⊤) ≅ Rep.trivial k G k

The permutation representation of G on the cosets of the whole group is the trivial representation: there is only one coset.

Equations

• TauCeti.quotientTopIsoTrivial k = Rep.ofMulActionSubsingletonIsoTrivial k G (G ⧸ ⊤)

@[simp]

theorem TauCeti.quotientTopIsoTrivial_hom_hom_single (k : Type u) [Ring k] {G : Type u} [Group G] (q : G ⧸ ⊤) (r : k) : (Rep.Hom.hom (quotientTopIsoTrivial k).hom) (MonoidAlgebra.single q r) = r

@[simp]

theorem TauCeti.quotientTopIsoTrivial_inv_hom_apply (k : Type u) [Ring k] {G : Type u} [Group G] (r : k) : (Rep.Hom.hom (quotientTopIsoTrivial k).inv) r = MonoidAlgebra.single (↑1) r