Theorems · Definition · group theory

Rep.diagonalSuccIsoTensorTrivial

(k G : Type u) →
  [inst : Group G] →
    [inst_1 : CommRing k] →
      (n : ℕ) →
        Rep.diagonal k G (n + 1) ≅
          CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.leftRegular k G)
            (Rep.trivial k G (MonoidAlgebra k (Fin n → G)))

An isomorphism of k-linear representations of G from k[Gⁿ⁺¹] to k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x) sending (g₀, ..., gₙ) to g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ). The inverse sends g₀ ⊗ (g₁, ..., gₙ) to (g₀, g₀g₁, ..., g₀g₁...gₙ).

Defined in

Mathlib.RepresentationTheory.Rep.Iso

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupCommRing