Theorems · Theorem · group theory

Rep.resCoindHomEquiv_symm_apply

∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : B ⟶ Rep.coind.{u, v, w, max t w} φ A),
  (Rep.resCoindHomEquiv.{t, u, v, w} φ B A).symm f =
    Rep.ofHom
      { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Rep.Hom.hom f).toLinearMap,
        isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Coinduced

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMonoidMonoid