Theorems · Definition · group theory

Rep.diagonalSuccIsoFree

(k G : Type u) →
  [inst : Group G] → [inst_1 : CommRing k] → (n : ℕ) → Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G)

Representation isomorphism k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]), where the right-hand representation is defined pointwise by the left regular representation on k[G]. The map sends single (g₀, ..., gₙ) a ↦ single (g₀⁻¹g₁, ..., gₙ₋₁⁻¹gₙ) (single g₀ a).

Defined in

Mathlib.RepresentationTheory.Rep.Iso

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupCommRing