Theorems · Definition · group theory

Representation.asModuleEquiv

{k : Type u_4} →
  {G : Type u_5} →
    {V : Type u_6} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (ρ : Representation k G V) → ρ.asModule ≃ₗ[k] V

The additive equivalence from the Module k[G] to the original vector space of the representative. This is just the identity, but it is helpful for typechecking and keeping track of instances.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

9 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Quot.sound

Assumes

SemiringMonoidAddCommMonoidModule