Theorems · Definition · group theory

Rep.indCoindIso

{k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] →
              (A : Rep.{max w u, u, v} k ↥S) → Rep.ind S.subtype A ≅ Rep.coind.{u, v, v, max u w} 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 an isomorphism Ind_S^G(A) ≅ Coind_S^G(A). The forward map sends (⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a), and the inverse sends f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n.

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRelSubgroup.FiniteIndex