Theorems · Definition · group theory

Rep.resCoindHomEquiv

{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) → (Rep.res φ B ⟶ A) ≃ₗ[k] B ⟶ Rep.coind.{u, v, w, max t w} φ A

Given a monoid homomorphism φ : G →* H, an H-representation B, and a G-representation A, there is a k-linear equivalence between the G-representation morphisms res φ B ⟶ A and the H-representation morphisms B ⟶ coind φ A. Note Rep.resCoindHomEquiv.{t, u, v, w} has the property that even with all inputs explicitly given, the first universe cannot be synthesized.

Defined in

Mathlib.RepresentationTheory.Coinduced

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingMonoidMonoid