Theorems · Definition · group theory

Representation.IndV

{k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommGroup A] → [inst_4 : Module k A] → Representation k G A → Type (max u_4 u_3 u_1)

Given a group homomorphism φ : G →* H and a G-representation (A, ρ), this is the k-module (k[H] ⊗[k] A)_G with the G-representation on k[H] defined by φ. See Representation.ind for the induced H-representation on IndV φ ρ.

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupAddCommGroupModule