Theorems · Definition · group theory

Rep.indMap

{k : Type u} →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] → (φ : G →* H) → {A B : Rep.{u_1, u, v} k G} → (A ⟶ B) → (Rep.ind φ A ⟶ Rep.ind φ B)

Given a group homomorphism φ : G →* H, a morphism of G-representations f : A ⟶ B induces a morphism of H-representations (k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G.

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup