Theorems · Definition · group theory

Rep.ind

{k : Type u} →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] → [inst_2 : Group H] → (G →* H) → Rep.{w, u, v} k G → Rep.{max (max u v') w, u, v'} k H

Given a group homomorphism φ : G →* H and a G-representation A, this is (k[H] ⊗[k] A)_G equipped with the H-representation defined by sending h : H and ⟦h₁ ⊗ₜ a⟧ to ⟦h₁h⁻¹ ⊗ₜ a⟧.

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

28 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup