Faithful quotient representations

Mathlib's Representation.ofQuotient descends a representation through a normal subgroup acting trivially. The kernel always acts trivially, and quotienting by it gives a faithful representation on the original module, with the caller's scalar and additive structures.

instance Representation.isTrivial_comp_ker {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : IsTrivial (MonoidHom.comp ρ (MonoidHom.ker ρ).subtype)

Restriction to the kernel is a trivial representation.

@[simp]

theorem Representation.ofQuotient_comp_mk' {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : MonoidHom.comp (ρ.ofQuotient S) (QuotientGroup.mk' S) = ρ

Restricting a quotient representation along the quotient map recovers the original representation, on the same module with the caller's scalar and additive structures.

theorem Representation.injective_ofQuotient_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : Function.Injective ⇑(ρ.ofQuotient S) ↔ S = MonoidHom.ker ρ

A quotient representation is faithful exactly when the subgroup removed is the entire kernel.