Theorems · Definition · group theory

Representation.linearizeMap

{k : Type u} →
  {G : Type v} →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        {X Y : Action (Type w) G} →
          (X ⟶ Y) → (Representation.linearize k G X).IntertwiningMap (Representation.linearize k G Y)

Every morphism between G-sets could be made into an intertwining map between Representations by the linear map induced on the indexing sets.

Defined in

Mathlib.RepresentationTheory.Action

Cited by

15 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidSemiring