Coset bases of group algebras

An injective group homomorphism p : M →* N makes R[N] free as a left R[M]-module, with scalars acting through mapDomainRingHom R p. The basis consists of the inverses of chosen left-coset representatives of p.range, which represent its right cosets.

Main definitions

• TauCeti.MonoidAlgebra.basisCosets: the coset basis of R[N] over R[M].

noncomputable def TauCeti.MonoidAlgebra.basisCosets (R : Type u_1) {M : Type u_2} {N : Type u_3} [Semiring R] [Group M] [Group N] (p : M →* N) (hp : Function.Injective ⇑p) : Module.Basis (N ⧸ p.range) (MonoidAlgebra R M) (MonoidAlgebra R N)

Inverses of left-coset representatives form a basis of the target group algebra over the source of an injective group-algebra map. These inverses represent the right cosets, as required for the left scalar action through mapDomainRingHom R p.

Equations

• TauCeti.MonoidAlgebra.basisCosets R p hp = { repr := (TauCeti.MonoidAlgebra.cosetLinearEquiv✝ p hp).symm }

@[simp]

theorem TauCeti.MonoidAlgebra.basisCosets_apply (R : Type u_1) {M : Type u_2} {N : Type u_3} [Semiring R] [Group M] [Group N] (p : M →* N) (hp : Function.Injective ⇑p) (q : N ⧸ p.range) : (basisCosets R p hp) q = MonoidAlgebra.single (Quotient.out q)⁻¹ 1

The coset basis vector is the monomial at the inverse of the chosen representative.