Theorems · Definition · group theory

Rep.coind

{k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (G →* H) → Rep.{u_1, u, v} k G → Rep.{max w u_1, u, w} k H

If φ : G →* H and A : Rep k G then coind φ A is the coinduction of A along φ, defined by letting H act on the G-equivariant functions H → A by (h • f) h₁ := f (h₁ * h).

Defined in

Mathlib.RepresentationTheory.Coinduced

Cited by

23 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Quot.sound

Assumes

CommRingMonoidMonoid