Theorems · Definition · group theory

Rep.resMap

{k : Type u} →
  [inst : Semiring k] →
    {G : Type v1} →
      {H : Type v2} →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            {X Y : Rep.{u_1, u, v1} k G} →
              (f : H →* G) → (X ⟶ Y) → (Rep.of (MonoidHom.comp X.ρ f) ⟶ Rep.of (MonoidHom.comp Y.ρ f))

The map induced by a monoid homomorphism f : H →* G on morphisms between G-representations.

Defined in

Mathlib.RepresentationTheory.Rep.Res

Cited by

23 results in Mathlib

Foundations

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

Assumes

SemiringMonoidMonoid