Theorems · Definition · group theory

Rep.coindToInd

{k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} →
          (A : Rep.{w, u, v} k ↥S) →
            [S.FiniteIndex] → ↑(Rep.coind.{u, v, v, w} S.subtype A) →ₗ[k] ↑(Rep.ind S.subtype A)

Let S ≤ G be a finite index subgroup, g₁, ..., gₙ a set of right coset representatives of S, and A a k-linear S-representation. This is the k-linear map Coind_S^G(A) →ₗ[k] Ind_S^G(A) sending f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n.

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingGroupSubgroup.FiniteIndex