Theorems · Theorem · group theory

Representation.ind_apply

∀ {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) (h : H),
  (Representation.ind φ ρ) h =
    Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ)
      (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x => x * h⁻¹),
        isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroupAddCommGroupModule