Theorems · Definition · group theory

Representation.ind

{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) → Representation k H (Representation.IndV φ ρ)

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

7 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupAddCommGroupModule