Theorems · Definition · group theory

Rep.leftRegularTensorTrivialIsoFree

(k G α : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.leftRegular k G) (Rep.trivial k G (MonoidAlgebra k α)) ≅
        Rep.free k G α

The natural isomorphism sending single g r₁ ⊗ single a r₂ ↦ single a (single g r₁r₂).

Defined in: Mathlib.RepresentationTheory.Rep.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
CategoryTheory.Isostatement · cited by 3,963
Monoidstatement and proof · cited by 3,887
CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
Repstatement · cited by 843
MonoidAlgebrastatement · cited by 590
Rep.trivialstatement · cited by 20
Rep.leftRegularstatement · cited by 19
Rep.freestatement · cited by 9
Rep.mkIsoproof · cited by 7
Representation.leftRegularTensorTrivialIsoFreeproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

Rep.diagonalSuccIsoFreeproof · cited by 1
Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eqproof · cited by 0