Theorems · Definition · group theory

Rep.indToCoind

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

Let S ≤ G be a subgroup and A a k-linear S-representation. This is the k-linear map Ind_S^G(A) →ₗ[k] Coind_S^G(A) sending (⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a).

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRel