Rep k G is the category of k-linear representations of G.

Given a G-representation ρ on a module V, you can construct the bundled representation as Rep.of ρ. Conversely, given a bundled representation A : Rep k G, you can get the underlying module as A.V and the representation on it as A.ρ.

structure Rep (k : Type u) (G : Type v) [Semiring k] [Monoid G] : Type (max (max u v) (w + 1))

The category of representations of monoid G and their morphisms.

• V : Type w

  the underlying type of an object in Rep k G

• hV1 : AddCommGroup ↑self
• hV2 : Module k ↑self
• ρ : Representation k G ↑self

  the underlying representation of an object in Rep k G

@[implicit_reducible]

instance Rep.instCoeSortType {k : Type u} {G : Type v} [Semiring k] [Monoid G] : CoeSort (Rep.{w, u, v} k G) (Type w)

@[reducible, inline]

abbrev Rep.of {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X : Type w} [AddCommGroup X] [Module k X] (ρ : Representation k G X) : Rep.{w, u, v} k G

The object in the category of representations associated to a type equipped a representation. This is the preferred way to construct a term of Rep k G.

theorem Rep.of_V {k : Type u} {G : Type v} [Semiring k] [Monoid G] (X : Type w) [AddCommGroup X] [Module k X] (ρ : Representation k G X) : ↑(of ρ) = X

theorem Rep.of_ρ {k : Type u} {G : Type v} [Semiring k] [Monoid G] (X : Type w) [AddCommGroup X] [Module k X] (ρ : Representation k G X) : (of ρ).ρ = ρ

structure Rep.Hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) : Type w

The type of morphisms in Rep.{w} k G.

• hom' : A.ρ.IntertwiningMap B.ρ

  The underlying G-equivariant linear map.

theorem Rep.Hom.ext_iff {k : Type u} {G : Type v} {inst✝ : Semiring k} {inst✝¹ : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem Rep.Hom.ext {k : Type u} {G : Type v} {inst✝ : Semiring k} {inst✝¹ : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

@[implicit_reducible]

instance Rep.instCategory {k : Type u} {G : Type v} [Semiring k] [Monoid G] : CategoryTheory.Category.{w, max (max (w + 1) v) u} (Rep.{w, u, v} k G)

@[implicit_reducible]

instance Rep.instConcreteCategoryIntertwiningMapVρ {k : Type u} {G : Type v} [Semiring k] [Monoid G] : CategoryTheory.ConcreteCategory (Rep.{w, u, v} k G) fun (A B : Rep.{w, u, v} k G) => A.ρ.IntertwiningMap B.ρ

@[reducible, inline]

abbrev Rep.Hom.hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A.Hom B) : A.ρ.IntertwiningMap B.ρ

Turn a morphism in Rep back into an IntertwiningMap.

@[reducible, inline]

abbrev Rep.ofHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : of ρ ⟶ of σ

Typecheck an IntertwiningMap as a morphism in Rep.

def Rep.Hom.Simps.hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (f : A.Hom B) : A.ρ.IntertwiningMap B.ρ

Use the ConcreteCategory.hom projection for @[simps] lemmas.

@[simp]

theorem Rep.hom_id {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A : Rep.{w, u, v} k G) : Hom.hom (CategoryTheory.CategoryStruct.id A) = Representation.IntertwiningMap.id A.ρ

theorem Rep.id_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A : Rep.{w, u, v} k G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem Rep.hom_comp {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B C : Rep.{w, u, v} k G) (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem Rep.comp_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

theorem Rep.hom_ext {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem Rep.hom_ext_iff {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

theorem Rep.hom_comm_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (g : G) (a : ↑A) : (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

@[simp]

theorem Rep.hom_ofHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : Hom.hom (ofHom f) = f

@[simp]

theorem Rep.ofHom_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem Rep.ofHom_id {k : Type u} {G : Type v} [Semiring k] [Monoid G] {Y : Type w} [AddCommGroup Y] [Module k Y] {σ : Representation k G Y} : ofHom (Representation.IntertwiningMap.id σ) = CategoryTheory.CategoryStruct.id (of σ)

@[simp]

theorem Rep.ofHom_comp {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} {Z : Type w} [AddCommGroup Z] [Module k Z] {τ : Representation k G Z} (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem Rep.ofHom_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem Rep.inv_hom_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (e : A ≅ B) (x : ↑A) : (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

theorem Rep.hom_inv_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (e : A ≅ B) (x : ↑B) : (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

@[implicit_reducible]

instance Rep.instInhabited {k : Type u} {G : Type v} [Semiring k] [Monoid G] : Inhabited (Rep.{u, u, v} k G)

theorem Rep.forget_obj {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A : Rep.{w, u, v} k G) : (CategoryTheory.forget (Rep.{w, u, v} k G)).obj A = ↑A

theorem Rep.forget_map {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (f : A ⟶ B) : (CategoryTheory.forget (Rep.{w, u, v} k G)).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

def Rep.mkIso {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : of ρ ≅ of σ

An equiv between the underlying representations induce isomorphism between objects in Rep k G.

@[simp]

theorem Rep.mkIso_hom_hom_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) (x : X) : (Hom.hom (mkIso e).hom) x = (↑e).toLinearMap x

@[simp]

theorem Rep.mkIso_hom_hom_toLinearMap {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : (Hom.hom (mkIso e).hom).toLinearMap = (↑e).toLinearMap

@[simp]

theorem Rep.mkIso_inv_hom_toLinearMap {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : (Hom.hom (mkIso e).inv).toLinearMap = (↑e.symm).toLinearMap

@[simp]

theorem Rep.mkIso_inv_hom_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) (y : Y) : (Hom.hom (mkIso e).inv) y = e.symm y

@[simp]

theorem Rep.mkIso_hom_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : Hom.hom (mkIso e).hom = ↑e

def Representation.equivOfIso {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (i : A ≅ B) : A.ρ.Equiv B.ρ

The equivalence between representations induced from iso between objects in Rep k G.

@[simp]

theorem Representation.equivOfIso_invFun {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (i : A ≅ B) (a : ↑B) : (equivOfIso i).invFun a = (CategoryTheory.ConcreteCategory.hom i.inv) a

@[simp]

theorem Representation.equivOfIso_toFun {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (i : A ≅ B) (a : ↑A) : (equivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

instance Rep.reflectsIsomorphisms_forget {k : Type u} {G : Type v} [Semiring k] [Monoid G] : (CategoryTheory.forget (Rep.{w, u, v} k G)).ReflectsIsomorphisms

theorem Rep.hom_bijective {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Bijective Hom.hom

theorem Rep.hom_injective {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Injective Hom.hom

Convenience shortcut for Rep.hom_bijective.injective.

theorem Rep.hom_surjective {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Surjective Hom.hom

Convenience shortcut for Rep.hom_bijective.surjective.

def Rep.homEquiv {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : (A ⟶ B) ≃ A.ρ.IntertwiningMap B.ρ

The morphisms between two objects in Rep k G has an equivalence to the intertwining maps between their underlying representations.

@[simp]

theorem Rep.homEquiv_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A.Hom B) : homEquiv f = f.hom

@[simp]

theorem Rep.homEquiv_symm_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A.ρ.IntertwiningMap B.ρ) : homEquiv.symm f = ofHom f

@[implicit_reducible]

instance Rep.instAddHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Add (A ⟶ B)

theorem Rep.ofHom_add {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f g : ρ.IntertwiningMap σ) : ofHom (f + g) = ofHom f + ofHom g

theorem Rep.add_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f g : A ⟶ B) : Hom.hom (f + g) = Hom.hom f + Hom.hom g

theorem Rep.hom_comp_toLinearMap {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g : B ⟶ C) : (Hom.hom (CategoryTheory.CategoryStruct.comp f g)).toLinearMap = (Hom.hom g).toLinearMap ∘ₗ (Hom.hom f).toLinearMap

theorem Rep.add_comp {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B C : Rep.{w, u, v} k G} (f₁ f₂ : A ⟶ B) (g : B ⟶ C) : CategoryTheory.CategoryStruct.comp (f₁ + f₂) g = CategoryTheory.CategoryStruct.comp f₁ g + CategoryTheory.CategoryStruct.comp f₂ g

theorem Rep.comp_add {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g₁ g₂ : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (g₁ + g₂) = CategoryTheory.CategoryStruct.comp f g₁ + CategoryTheory.CategoryStruct.comp f g₂

@[implicit_reducible]

instance Rep.instZeroHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Zero (A ⟶ B)

@[simp]

theorem Rep.ofHom_zero {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} : ofHom 0 = 0

@[simp]

theorem Rep.zero_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Hom.hom 0 = 0

@[implicit_reducible]

instance Rep.instSMulNatHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : SMul ℕ (A ⟶ B)

theorem Rep.ofHom_nsmul {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (n : ℕ) : ofHom (n • f) = n • ofHom f

theorem Rep.nsmul_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (n : ℕ) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

instance Rep.instNegHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Neg (A ⟶ B)

theorem Rep.ofHom_neg {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : ofHom (-f) = -ofHom f

theorem Rep.neg_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : Hom.hom (-f) = -Hom.hom f

@[implicit_reducible]

instance Rep.instSubHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Sub (A ⟶ B)

theorem Rep.ofHom_sub {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f g : ρ.IntertwiningMap σ) : ofHom (f - g) = ofHom f - ofHom g

theorem Rep.sub_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f g : A ⟶ B) : Hom.hom (f - g) = Hom.hom f - Hom.hom g

@[implicit_reducible]

instance Rep.instSMulIntHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : SMul ℤ (A ⟶ B)

theorem Rep.ofHom_zsmul {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (n : ℤ) : ofHom (n • f) = n • ofHom f

theorem Rep.zsmul_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (n : ℤ) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

instance Rep.instAddCommGroupHom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : AddCommGroup (A ⟶ B)

@[implicit_reducible]

instance Rep.instPreadditive {k : Type u} {G : Type v} [Semiring k] [Monoid G] : CategoryTheory.Preadditive (Rep.{w, u, v} k G)

theorem Rep.sum_hom {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {ι : Type u'} (f : ι → (A ⟶ B)) (s : Finset ι) : Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)

theorem Rep.ofHom_sum {k : Type u} {G : Type v} [Semiring k] [Monoid G] {ι : Type u'} {M N : Type v'} [AddCommGroup M] [AddCommGroup N] [Module k M] [Module k N] {σ : Representation k G M} {ρ : Representation k G N} (f : ι → σ.IntertwiningMap ρ) (s : Finset ι) : ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)

@[reducible, inline]

abbrev Rep.trivial (k : Type u) (G : Type v) [Semiring k] [Monoid G] (V : Type w) [AddCommGroup V] [Module k V] : Rep.{w, u, v} k G

The trivial k-linear G-representation on a k-module V.

theorem Rep.trivial_V {k : Type u} {G : Type v} [Semiring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] : ↑(trivial k G V) = V

theorem Rep.trivial_ρ {k : Type u} {G : Type v} [Semiring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] (g : G) : (trivial k G V).ρ g = LinearMap.id

@[simp]

theorem Rep.trivial_ρ_apply {k : Type u} {G : Type v} [Semiring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] (g : G) (v : V) : ((trivial k G V).ρ g) v = v

theorem Rep.ρ_mul {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A : Rep.{w, u, v} k G} (g1 g2 : G) : A.ρ (g1 * g2) = A.ρ g1 ∘ₗ A.ρ g2

def Rep.applyAsHom {k : Type u} [Semiring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (g : G) : A ⟶ A

Given a representation A of a commutative monoid G, the map ρ_A(g) is a representation morphism A ⟶ A for any g : G.

@[simp]

theorem Rep.applyAsHom_apply {k : Type u} [Semiring k] {G : Type v} [CommMonoid G] {A : Rep.{u_1, u, v} k G} (g : G) (x : ↑A) : (Hom.hom (A.applyAsHom g)) x = (A.ρ g) x

theorem Rep.applyAsHom_comm {k : Type u} [Semiring k] {G : Type v} [CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G) : CategoryTheory.CategoryStruct.comp (A.applyAsHom g) f = CategoryTheory.CategoryStruct.comp f (B.applyAsHom g)

theorem Rep.applyAsHom_comm_assoc {k : Type u} [Semiring k] {G : Type v} [CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G) {Z : Rep.{u_1, u, v} k G} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.applyAsHom g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (B.applyAsHom g) h)

theorem Rep.applyAsHom_comm_apply {k : Type u} [Semiring k] {G : Type v} [CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom f) ((A.ρ g) x) = (B.ρ g) ((CategoryTheory.ConcreteCategory.hom f) x)

@[reducible, inline]

noncomputable abbrev Rep.ofMulAction (k : Type u) (G : Type v) [Ring k] [Monoid G] (H : Type w') [MulAction G H] : Rep.{max u w', u, v} k G

Given a G-action on H, this is k[H] bundled with the natural representation G →* End(k[H]) as a term of type Rep k G.

@[reducible, inline]

noncomputable abbrev Rep.leftRegular (k : Type u) (G : Type v) [Ring k] [Monoid G] : Rep.{max u v, u, v} k G

The k-linear G-representation on k[G], induced by left multiplication.

@[reducible, inline]

noncomputable abbrev Rep.diagonal (k : Type u) (G : Type v) [Ring k] [Monoid G] (n : ℕ) : Rep.{max u v, u, v} k G

The k-linear G-representation on k[Gⁿ], induced by left multiplication.

@[reducible, inline]

noncomputable abbrev Rep.diagonalOneIsoLeftRegular (k : Type u) (G : Type v) [Ring k] [Monoid G] : diagonal k G 1 ≅ leftRegular k G

The natural isomorphism between the representations on k[G¹] and k[G] induced by left multiplication in G.

@[reducible, inline]

noncomputable abbrev Rep.ofMulActionSubsingletonIsoTrivial (k : Type u) (G : Type v) [Ring k] [Monoid G] (H : Type u) [Subsingleton H] [MulOneClass H] [MulAction G H] : ofMulAction k G H ≅ trivial k G k

When H = {1}, the G-representation on k[H] induced by an action of G on H is isomorphic to the trivial representation on k.

def Rep.ofDistribMulAction (k : Type u) (G : Type v) [Ring k] [Monoid G] (A : Type w') [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] : Rep.{w', u, v} k G

Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

@[simp]

theorem Rep.ofDistribMulAction_ρ_apply_apply (k : Type u) (G : Type v) [Ring k] [Monoid G] (A : Type w') [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (g : G) (a : A) : ((ofDistribMulAction k G A).ρ g) a = g • a

def Rep.ofAlgebraAut (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Rep.{u_2, 0, u_2} ℤ (S ≃ₐ[R] S)

Given an R-algebra S, the ℤ-linear representation associated to the natural action of S ≃ₐ[R] S on S.

def Rep.ofMulDistribMulAction (M : Type u_1) (G : Type u_2) [Monoid M] [CommGroup G] [MulDistribMulAction M G] : Rep.{u_2, 0, u_1} ℤ M

Turns a CommGroup G with a MulDistribMulAction of a monoid M into a ℤ-linear M-representation on Additive G.

def Rep.toAdditive {M : Type u_1} {G : Type u_2} [Monoid M] [CommGroup G] [MulDistribMulAction M G] : ↑(ofMulDistribMulAction M G) ≃+ Additive G

Unfolds ofMulDistribMulAction; useful to keep track of additivity.

@[simp]

theorem Rep.toAdditive_apply {M : Type u_1} {G : Type u_2} [Monoid M] [CommGroup G] [MulDistribMulAction M G] (a : ↑(ofMulDistribMulAction M G)) : toAdditive a = a

@[simp]

theorem Rep.toAdditive_symm_apply {M : Type u_1} {G : Type u_2} [Monoid M] [CommGroup G] [MulDistribMulAction M G] (a : ↑(ofMulDistribMulAction M G)) : toAdditive.symm a = a

@[simp]

theorem Rep.ofMulDistribMulAction_ρ_apply_apply {M : Type u_1} {G : Type u_2} [Monoid M] [CommGroup G] [MulDistribMulAction M G] (g : M) (a : Additive G) : ((ofMulDistribMulAction M G).ρ g) a = Additive.ofMul (g • Additive.toMul a)

def Rep.ofAlgebraAutOnUnits (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] : Rep.{u_4, 0, u_4} ℤ (S ≃ₐ[R] S)

Given an R-algebra S, the ℤ-linear representation associated to the natural action of S ≃ₐ[R] S on Sˣ.

@[reducible, inline]

noncomputable abbrev Rep.leftRegularHom {k : Type u} {G : Type v} [Ring k] [Monoid G] (A : Rep.{max u v, u, v} k G) (x : ↑A) : leftRegular k G ⟶ A

Given an element x : A, there is a natural morphism of representations k[G] ⟶ A sending g ↦ A.ρ(g)(x).

theorem Rep.leftRegularHom_hom_single {k : Type u} {G : Type v} [Ring k] [Monoid G] {A : Rep.{max u v, u, v} k G} (g : G) (x : ↑A) (r : k) : ((Hom.hom (A.leftRegularHom x)) fun₀ | g => r) = r • (A.ρ g) x

@[reducible, inline]

abbrev Rep.subrepresentation {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : Rep.{u_1, u, v} k G

Given a k-linear G-representation (V, ρ), this is the representation defined by restricting ρ to a G-invariant k-submodule of V.

def Rep.subtype {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : A.subrepresentation W le_comap ⟶ A

The natural inclusion of a subrepresentation into the ambient representation.

@[simp]

theorem Rep.subtype_hom_toFun {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) (self : ↥W) : (Hom.hom (A.subtype W le_comap)) self = ↑self

@[reducible, inline]

abbrev Rep.quotient {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : Rep.{u_1, u, v} k G

Given a k-linear G-representation (V, ρ) and a G-invariant k-submodule W ≤ V, this is the representation induced on V ⧸ W by ρ.

def Rep.mkQ {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : A ⟶ A.quotient W le_comap

The natural projection from a representation to its quotient by a subrepresentation.

@[simp]

theorem Rep.mkQ_hom_toFun {k : Type u} [Ring k] {G : Type v} [CommMonoid G] (A : Rep.{u_1, u, v} k G) (W : Submodule k ↑A) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) (a✝ : ↑A) : (Hom.hom (A.mkQ W le_comap)) a✝ = Submodule.Quotient.mk a✝

def Rep.trivialFunctor (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.Functor (ModuleCat k) (Rep.{w, u, v} k G)

The functor equipping a module with the trivial representation.

@[simp]

theorem Rep.trivialFunctor_obj_V (k : Type u) (G : Type v) [Ring k] [Monoid G] (V : ModuleCat k) : ↑((trivialFunctor k G).obj V) = ↑V

@[simp]

theorem Rep.trivialFunctor_map_hom (k : Type u) (G : Type v) [Ring k] [Monoid G] {X✝ Y✝ : ModuleCat k} (f : X✝ ⟶ Y✝) : Hom.hom ((trivialFunctor k G).map f) = { toLinearMap := ModuleCat.Hom.hom f, isIntertwining' := ⋯ }

@[reducible, inline]

abbrev Rep.IsTrivial {k : Type u} {G : Type v} [Ring k] [Monoid G] (A : Rep.{u_1, u, v} k G) : Prop

A predicate for representations that fix every element.

instance Rep.instIsTrivialObjModuleCatTrivialFunctor {k : Type u} {G : Type v} [Ring k] [Monoid G] (X : ModuleCat k) : ((trivialFunctor k G).obj X).IsTrivial

instance Rep.instIsTrivialTrivial {k : Type u} {G : Type v} [Ring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] : (trivial k G V).IsTrivial

instance Rep.instIsTrivialOfOfIsTrivial {k : Type u} {G : Type v} [Ring k] [Monoid G] {V : Type w} [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] : (of ρ).IsTrivial

instance Rep.instIsTrivialVOfCompLinearMapIdρ {k : Type u} {G : Type v} [Ring k] [Monoid G] {H : Type u'} {V : Type w} [Group H] [AddCommGroup V] [Module k V] (ρ : Representation k H V) (f : G →* H) [Representation.IsTrivial (MonoidHom.comp ρ f)] : Representation.IsTrivial (MonoidHom.comp (of ρ).ρ f)

@[implicit_reducible]

instance Rep.hasForgetToModuleCat {k : Type u} {G : Type v} [Ring k] [Monoid G] : CategoryTheory.HasForget₂ (Rep.{w, u, v} k G) (ModuleCat k)

@[reducible, inline]

abbrev Rep.Hom.toModuleCatHom {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : ModuleCat.of k ↑A ⟶ ModuleCat.of k ↑B

A morphism in Rep k G has an underlying linear map attached to it hence induce a morphism in ModuleCat k.

@[simp]

theorem Rep.forget₂_moduleCat_obj {k : Type u} {G : Type v} [Ring k] [Monoid G] (A : Rep.{w, u, v} k G) : (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).obj A = ModuleCat.of k ↑A

@[simp]

theorem Rep.forget₂_moduleCat_map {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).map f = ModuleCat.ofHom (Hom.hom f).toLinearMap

instance Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier {k : Type u} {G : Type v} [Ring k] [Monoid G] : (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).Faithful

def Rep.RepToAction (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.Functor (Rep.{w, u, v} k G) (Action (ModuleCat k) G)

Every object in Rep k G naturally correspond to an object in Action.

@[simp]

theorem Rep.RepToAction_obj_ρ (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : ((RepToAction k G).obj X).ρ = (ModuleCat.of k ↑X).endRingEquiv.symm.toMonoidHom.comp X.ρ

@[simp]

theorem Rep.RepToAction_obj_V_carrier (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : ↑((RepToAction k G).obj X).V = ↑X

@[simp]

theorem Rep.RepToAction_obj_V_isModule (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : ((RepToAction k G).obj X).V.isModule = X.hV2

@[simp]

theorem Rep.RepToAction_obj_V_isAddCommGroup (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : ((RepToAction k G).obj X).V.isAddCommGroup = X.hV1

@[simp]

theorem Rep.RepToAction_map_hom (k : Type u) (G : Type v) [Ring k] [Monoid G] {X✝ Y✝ : Rep.{w, u, v} k G} (f : X✝ ⟶ Y✝) : ((RepToAction k G).map f).hom = Hom.toModuleCatHom f

theorem Rep.RepToAction_obj (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : (RepToAction k G).obj X = { V := ModuleCat.of k ↑X, ρ := (ModuleCat.of k ↑X).endRingEquiv.symm.toMonoidHom.comp X.ρ }

def Rep.ActionToRep (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.Functor (Action (ModuleCat k) G) (Rep.{w, u, v} k G)

Every object in ModuleCat k that G acts on is an object in Rep k G.

@[simp]

theorem Rep.ActionToRep_obj_V (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Action (ModuleCat k) G) : ↑((ActionToRep k G).obj X) = ↑X.V

@[simp]

theorem Rep.ActionToRep_obj_ρ (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Action (ModuleCat k) G) : ((ActionToRep k G).obj X).ρ = X.V.endRingEquiv.toMonoidHom.comp X.ρ

@[simp]

theorem Rep.ActionToRep_map (k : Type u) (G : Type v) [Ring k] [Monoid G] {X✝ Y✝ : Action (ModuleCat k) G} (f : X✝ ⟶ Y✝) : (ActionToRep k G).map f = ofHom { toLinearMap := ModuleCat.Hom.hom f.hom, isIntertwining' := ⋯ }

def Rep.RepToAction_ActionToRep (k : Type u) (G : Type v) [Ring k] [Monoid G] (A : Action (ModuleCat k) G) : (RepToAction k G).obj ((ActionToRep k G).obj A) ≅ A

unitIso of the equivalence between Action and Rep.

def Rep.ActionToRep_RepToAction (k : Type u) (G : Type v) [Ring k] [Monoid G] (X : Rep.{w, u, v} k G) : (ActionToRep k G).obj ((RepToAction k G).obj X) ≅ X

counitIso of the equivalence between Action and Rep.

def Rep.repIsoAction (k : Type u) (G : Type v) [Ring k] [Monoid G] : Rep.{w, u, v} k G ≌ Action (ModuleCat k) G

The category equivalence between Rep and Action.

instance Rep.instIsEquivalenceActionModuleCatRepToAction (k : Type u) (G : Type v) [Ring k] [Monoid G] : (RepToAction k G).IsEquivalence

instance Rep.instIsEquivalenceActionModuleCatActionToRep (k : Type u) (G : Type v) [Ring k] [Monoid G] : (ActionToRep k G).IsEquivalence

instance Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier (k : Type u) (G : Type v) [Ring k] [Monoid G] : (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).Additive

@[reducible, inline]

abbrev Rep.forgetNatIsoActionForget (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k) ≅ (RepToAction k G).comp (Action.forget (ModuleCat k) G)

Forgetting Rep to ModuleCat is the same as first map to Action then forget to ModuleCat.

instance Rep.preservesLimits_forget (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)} (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))

instance Rep.preservesColimits_forget (k : Type u) (G : Type v) [Ring k] [Monoid G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)} (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))

theorem Rep.epi_iff_surjective {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(Hom.hom f)

theorem Rep.mono_iff_injective {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑(Hom.hom f)

instance Rep.instMonoModuleCatToModuleCatHom (k : Type u) (G : Type v) [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) [CategoryTheory.Mono f] : CategoryTheory.Mono (Hom.toModuleCatHom f)

instance Rep.instEpiModuleCatToModuleCatHom (k : Type u) (G : Type v) [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) [CategoryTheory.Epi f] : CategoryTheory.Epi (Hom.toModuleCatHom f)

@[implicit_reducible]

instance Rep.instSMulHom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N : Rep.{u_1, u, v} k G} : SMul k (M ⟶ N)

theorem Rep.ofHom_smul {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N : Type w} [AddCommGroup M] [AddCommGroup N] [Module k M] [Module k N] {σ : Representation k G M} {ρ : Representation k G N} (f : σ.IntertwiningMap ρ) (r : k) : ofHom (r • f) = r • ofHom f

theorem Rep.smul_hom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N : Rep.{u_1, u, v} k G} (f : M ⟶ N) (r : k) : Hom.hom (r • f) = r • Hom.hom f

theorem Rep.smul_comp {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N O : Rep.{u_1, u, v} k G} (r : k) (f : M ⟶ N) (g : N ⟶ O) : CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g

theorem Rep.comp_smul {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N O : Rep.{u_1, u, v} k G} (f : M ⟶ N) (r : k) (g : N ⟶ O) : CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g

@[implicit_reducible]

instance Rep.instModuleHom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M N : Rep.{u_1, u, v} k G} : Module k (M ⟶ N)

@[implicit_reducible]

instance Rep.instLinear {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Linear k (Rep.{u_1, u, v} k G)

instance Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor.Linear k (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))

@[reducible, inline]

abbrev Rep.homLinearEquiv {k : Type u} {G : Type v} [CommRing k] [Monoid G] (X Y : Rep.{u_1, u, v} k G) : (X ⟶ Y) ≃ₗ[k] X.ρ.IntertwiningMap Y.ρ

The equivalence between IntertwiningMaps and morphism between X Y : Rep k G is linear.

@[implicit_reducible]

noncomputable instance Rep.instMonoidalCategory {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.MonoidalCategory (Rep.{u, u, v} k G)

@[simp]

theorem Rep.tensorUnit_V {k : Type u} {G : Type v} [CommRing k] [Monoid G] : ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep.{u, u, v} k G)) = k

@[simp]

theorem Rep.tensorUnit_ρ {k : Type u} {G : Type v} [CommRing k] [Monoid G] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep.{u, u, v} k G)).ρ = Representation.trivial k G k

@[simp]

theorem Rep.tensor_V {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Rep.{u, u, v} k G} : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = TensorProduct k ↑X ↑Y

@[simp]

theorem Rep.tensor_ρ {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Rep.{u, u, v} k G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ = X.ρ.tprod Y.ρ

@[simp]

theorem Rep.hom_whiskerRight {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X₁ X₂ Y : Rep.{u, u, v} k G} (f : X₁ ⟶ X₂) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = Representation.IntertwiningMap.rTensor Y.ρ (Hom.hom f)

@[simp]

theorem Rep.hom_whiskerLeft {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y₁ Y₂ : Rep.{u, u, v} k G} (f : Y₁ ⟶ Y₂) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) = Representation.IntertwiningMap.lTensor X.ρ (Hom.hom f)

@[simp]

theorem Rep.hom_tensorHom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X₁ X₂ Y₁ Y₂ : Rep.{u, u, v} k G} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (Hom.hom f).tensor (Hom.hom g)

@[simp]

theorem Rep.of_tensor {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] (σ : Representation k G X) (ρ : Representation k G Y) : of (σ.tprod ρ) = CategoryTheory.MonoidalCategoryStruct.tensorObj (of σ) (of ρ)

@[simp]

theorem Rep.hom_hom_associator {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y Z : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ)

@[simp]

theorem Rep.hom_inv_associator {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y Z : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ).symm

@[simp]

theorem Rep.hom_hom_leftUnitor {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = ↑(Representation.TensorProduct.lid k X.ρ)

@[simp]

theorem Rep.hom_inv_leftUnitor {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = ↑(Representation.TensorProduct.lid k X.ρ).symm

@[simp]

theorem Rep.hom_hom_rightUnitor {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = ↑(Representation.TensorProduct.rid k X.ρ)

@[simp]

theorem Rep.hom_inv_rightUnitor {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = ↑(Representation.TensorProduct.rid k X.ρ).symm

instance Rep.instMonoidalPreadditive {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.MonoidalPreadditive (Rep.{u, u, v} k G)

instance Rep.instMonoidalLinear {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.MonoidalLinear k (Rep.{u, u, v} k G)

@[implicit_reducible]

noncomputable instance Rep.instBraidedCategory {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.BraidedCategory (Rep.{u, u, v} k G)

@[simp]

theorem Rep.hom_braiding {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Rep.{u, u, v} k G} : Hom.hom (β_ X Y).hom = ↑(Representation.TensorProduct.comm X.ρ Y.ρ)

@[implicit_reducible]

noncomputable instance Rep.instSymmetricCategory {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.SymmetricCategory (Rep.{u, u, v} k G)

noncomputable def Rep.ihom {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep.{w, u, v} k G) : CategoryTheory.Functor (Rep.{u_1, u, v} k G) (Rep.{max w u_1, u, v} k G)

Given a k-linear G-representation (A, ρ₁), this is the 'internal Hom' functor sending (B, ρ₂) to the representation Homₖ(A, B) that maps g : G and f : A →ₗ[k] B to (ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹).

@[simp]

theorem Rep.ihom_map {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep.{w, u, v} k G) {X Y : Rep.{u_1, u, v} k G} (f : X ⟶ Y) : A.ihom.map f = ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Rep.ihom_obj_V {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep.{w, u, v} k G) (B : Rep.{u_1, u, v} k G) : ↑(A.ihom.obj B) = (↑A →ₗ[k] ↑B)

@[simp]

theorem Rep.ihom_obj_ρ {k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep.{w, u, v} k G) (B : Rep.{u_1, u, v} k G) : (A.ihom.obj B).ρ = A.ρ.linHom B.ρ

@[simp]

theorem Rep.ihom_obj_ρ_apply {k : Type u} [CommRing k] {G : Type v} [Group G] {A : Rep.{u_1, u, v} k G} {B : Rep.{u_2, u, v} k G} (g : G) (x : ↑A →ₗ[k] ↑B) : ((A.ihom.obj B).ρ g) x = B.ρ g ∘ₗ x ∘ₗ A.ρ g⁻¹

noncomputable def Rep.tensorHomEquiv {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ (B ⟶ A.ihom.obj C)

Given a k-linear G-representation A, this is the Hom-set bijection in the adjunction A ⊗ - ⊣ ihom(A, -). It sends f : A ⊗ B ⟶ C to a Rep k G morphism defined by currying the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then flipping the arguments.

@[simp]

theorem Rep.tensorHomEquiv_symm_apply {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A.ihom.obj C) : (A.tensorHomEquiv B C).symm f = ofHom { toLinearMap := (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip, isIntertwining' := ⋯ }

@[simp]

theorem Rep.tensorHomEquiv_apply {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (A.tensorHomEquiv B C) f = ofHom { toLinearMap := (TensorProduct.curry (Hom.hom f).toLinearMap).flip, isIntertwining' := ⋯ }

@[implicit_reducible]

noncomputable instance Rep.instMonoidalClosed {k : Type u} [CommRing k] {G : Type v} [Group G] : CategoryTheory.MonoidalClosed (Rep.{u, u, v} k G)

@[simp]

theorem Rep.ihom_obj_ρ_def {k : Type u} [CommRing k] {G : Type v} [Group G] (A B : Rep.{u, u, v} k G) : (A ⟹ B).ρ = (A.ihom.obj B).ρ

@[simp]

theorem Rep.homEquiv_def {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) : (CategoryTheory.ihom.adjunction A).homEquiv B C = A.tensorHomEquiv B C

@[simp]

theorem Rep.ihom_ev_app_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B : Rep.{u, u, v} k G) : (Hom.hom ((CategoryTheory.ihom.ev A).app B)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip

@[simp]

theorem Rep.ihom_coev_app_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B : Rep.{u, u, v} k G) : (Hom.hom ((CategoryTheory.ihom.coev A).app B)).toLinearMap = (TensorProduct.mk k ↑A ↑((CategoryTheory.Functor.id (Rep.{u, u, v} k G)).obj B)).flip

noncomputable def Rep.MonoidalClosed.linearHomEquiv {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] B ⟶ A ⟹ C

There is a k-linear isomorphism between the sets of representation morphisms Hom(A ⊗ B, C) and Hom(B, Homₖ(A, C)).

noncomputable def Rep.MonoidalClosed.linearHomEquivComm {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] A ⟶ B ⟹ C

There is a k-linear isomorphism between the sets of representation morphisms Hom(A ⊗ B, C) and Hom(A, Homₖ(B, C)).

@[simp]

theorem Rep.MonoidalClosed.linearHomEquiv_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (Hom.hom ((linearHomEquiv A B C) f)).toLinearMap = (TensorProduct.curry (Hom.hom f).toLinearMap).flip

@[simp]

theorem Rep.MonoidalClosed.linearHomEquivComm_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (Hom.hom ((linearHomEquivComm A B C) f)).toLinearMap = TensorProduct.curry (Hom.hom f).toLinearMap

theorem Rep.MonoidalClosed.linearHomEquiv_symm_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A ⟹ C) : (Hom.hom ((linearHomEquiv A B C).symm f)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip

theorem Rep.MonoidalClosed.linearHomEquivComm_symm_hom {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : A ⟶ B ⟹ C) : (Hom.hom ((linearHomEquivComm A B C).symm f)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).toLinearMap

def Rep.norm {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] (A : Rep.{w, u, v} k G) : CategoryTheory.End A

Given a representation A of a finite group G, norm A is the representation morphism A ⟶ A defined by x ↦ ∑ A.ρ g x for g in G.

@[simp]

theorem Rep.norm_apply {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] (A : Rep.{w, u, v} k G) {x : ↑A} : (Hom.hom A.norm) x = A.ρ.norm x

theorem Rep.norm_comm {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f B.norm = CategoryTheory.CategoryStruct.comp A.norm f

theorem Rep.norm_comm_assoc {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) {Z : Rep.{u_1, u, v} k G} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp B.norm h) = CategoryTheory.CategoryStruct.comp A.norm (CategoryTheory.CategoryStruct.comp f h)

theorem Rep.norm_comm_apply {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (x : ↑A) : B.ρ.norm ((CategoryTheory.ConcreteCategory.hom f) x) = (CategoryTheory.ConcreteCategory.hom f) (A.ρ.norm x)

def Rep.normNatTrans {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] : CategoryTheory.End (CategoryTheory.Functor.id (Rep.{u_1, u, v} k G))

Given a representation A of a finite group G, the norm map A ⟶ A defined by x ↦ ∑ A.ρ g x for g in G defines a natural endomorphism of the identity functor.

@[simp]

theorem Rep.normNatTrans_app {k : Type u} [CommRing k] {G : Type v} [Group G] [Fintype G] (A : Rep.{u_1, u, v} k G) : normNatTrans.app A = A.norm

@[reducible, inline]

noncomputable abbrev Rep.finsupp {k : Type u} {G : Type v} [CommRing k] [Monoid G] (α : Type u') (A : Rep.{u_1, u, v} k G) : Rep.{max u' u_1, u, v} k G

The representation on α →₀ A defined pointwise by a representation on A.

@[simp]

theorem Rep.finsupp_V (k : Type u) (G : Type v) [CommRing k] [Monoid G] (α : Type u') (A : Rep.{u_1, u, v} k G) : ↑(finsupp α A) = (α →₀ ↑A)

@[reducible, inline]

noncomputable abbrev Rep.free (k : Type u) (G : Type v) [CommRing k] [Monoid G] (α : Type u') : Rep.{max (max u u') v, u, v} k G

The representation on α →₀ k[G] defined pointwise by the left regular representation on k[G].

@[reducible, inline]

noncomputable abbrev Rep.freeLift (k : Type u) (G : Type v) [CommRing k] [Monoid G] {α : Type u'} (A : Rep.{max (max u u') v, u, v} k G) (f : α → ↑A) : free k G α ⟶ A

Given f : α → A, the natural representation morphism (α →₀ k[G]) ⟶ A sending single a (single g r) ↦ r • A.ρ g (f a).

@[reducible, inline]

noncomputable abbrev Rep.freeLiftLEquiv (k : Type u) (G : Type v) [CommRing k] [Monoid G] (α : Type u') (A : Rep.{max (max u u') v, u, v} k G) : (free k G α ⟶ A) ≃ₗ[k] α → ↑A

The natural linear equivalence between functions α → A and representation morphisms (α →₀ k[G]) ⟶ A.

theorem Rep.free_ext (k : Type u) (G : Type v) [CommRing k] [Monoid G] {α : Type u'} (A : Rep.{max (max u u') v, u, v} k G) (f g : free k G α ⟶ A) (h : ∀ (i : α), ((Hom.hom f) fun₀ | i => fun₀ | 1 => 1) = (Hom.hom g) fun₀ | i => fun₀ | 1 => 1) : f = g

@[reducible, inline]

noncomputable abbrev Rep.finsuppTensorLeft (k : Type u) (G : Type v) [CommRing k] [Monoid G] (A B : Rep.{u, u, v} k G) (α : Type u) [DecidableEq α] : CategoryTheory.MonoidalCategoryStruct.tensorObj (finsupp α A) B ≅ finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Given representations A, B and a type α, this is the natural representation isomorphism (α →₀ A) ⊗ B ≅ (A ⊗ B) →₀ α sending single x a ⊗ₜ b ↦ single x (a ⊗ₜ b).

@[reducible, inline]

noncomputable abbrev Rep.finsuppTensorRight (k : Type u) (G : Type v) [CommRing k] [Monoid G] (A B : Rep.{u, u, v} k G) (α : Type u) [DecidableEq α] : CategoryTheory.MonoidalCategoryStruct.tensorObj A (finsupp α B) ≅ finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Given representations A, B and a type α, this is the natural representation isomorphism A ⊗ (α →₀ B) ≅ (A ⊗ B) →₀ α sending a ⊗ₜ single x b ↦ single x (a ⊗ₜ b).

@[reducible, inline]

noncomputable abbrev Rep.leftRegularTensorTrivialIsoFree (k G α : Type u) [CommRing k] [Monoid G] : CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular k G) (trivial k G (α →₀ k)) ≅ free k G α

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

@[reducible, inline]

noncomputable abbrev Rep.linearization (k : Type u) (G : Type v) [CommRing k] [Monoid G] : CategoryTheory.Functor (Action (Type w) G) (Rep.{max w u, u, v} k G)

The monoidal functor sending a type H with a G-action to the induced k-linear G-representation on k[H].

@[simp]

theorem Rep.linearization_obj_V (k : Type u) (G : Type v) [CommRing k] [Monoid G] (X : Action (Type w) G) : ↑((linearization k G).obj X) = (X.V →₀ k)

@[simp]

theorem Rep.linearization_map (k : Type u) (G : Type v) [CommRing k] [Monoid G] {X✝ Y✝ : Action (Type w) G} (f : X✝ ⟶ Y✝) : (linearization k G).map f = ofHom (Representation.linearizeMap f)

@[simp]

theorem Rep.linearization_obj_ρ (k : Type u) (G : Type v) [CommRing k] [Monoid G] (X : Action (Type w) G) : ((linearization k G).obj X).ρ = Representation.linearize k G X

@[implicit_reducible]

noncomputable instance Rep.instMonoidalActionTypeLinearization (k : Type u) (G : Type v) [CommRing k] [Monoid G] : (linearization k G).Monoidal

theorem Rep.μ_def {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.LaxMonoidal.μ (linearization k G) X Y = ofHom (Representation.LinearizeMonoidal.μ X Y)

theorem Rep.μ_hom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : Hom.hom (CategoryTheory.Functor.LaxMonoidal.μ (linearization k G) X Y) = Representation.LinearizeMonoidal.μ X Y

theorem Rep.ε_def {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor.LaxMonoidal.ε (linearization k G) = ofHom (Representation.LinearizeMonoidal.ε k G)

theorem Rep.ε_hom {k : Type u} {G : Type v} [CommRing k] [Monoid G] : Hom.hom (CategoryTheory.Functor.LaxMonoidal.ε (linearization k G)) = Representation.LinearizeMonoidal.ε k G

theorem Rep.δ_def {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.OplaxMonoidal.δ (linearization k G) X Y = ofHom (Representation.LinearizeMonoidal.δ X Y)

theorem Rep.δ_hom {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : Hom.hom (CategoryTheory.Functor.OplaxMonoidal.δ (linearization k G) X Y) = Representation.LinearizeMonoidal.δ X Y

theorem Rep.η_def {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor.OplaxMonoidal.η (linearization k G) = ofHom (Representation.LinearizeMonoidal.η k G)

theorem Rep.η_hom {k : Type u} {G : Type v} [CommRing k] [Monoid G] : Hom.hom (CategoryTheory.Functor.OplaxMonoidal.η (linearization k G)) = Representation.LinearizeMonoidal.η k G

@[reducible, inline]

noncomputable abbrev Rep.linearizationTrivialIso (k : Type u) (G : Type v) [CommRing k] [Monoid G] (X : Type u) : (linearization k G).obj (Action.trivial G X) ≅ trivial k G (X →₀ k)

The linearization of a type X on which G acts trivially is the trivial G-representation on k[X].

@[reducible, inline]

noncomputable abbrev Rep.linearizationOfMulActionIso (k : Type u) (G : Type v) [CommRing k] [Monoid G] (H : Type u) [MulAction G H] : (linearization k G).obj (Action.ofMulAction G H) ≅ ofMulAction k G H

The linearization of a type H with a G-action is definitionally isomorphic to the k-linear G-representation on k[H] induced by the G-action on H.

@[reducible, inline]

noncomputable abbrev Rep.leftRegularHomEquiv {k : Type u} {G : Type v} [CommRing k] [Monoid G] (A : Rep.{max u v, u, v} k G) : (leftRegular k G ⟶ A) ≃ₗ[k] ↑A

Given a k-linear G-representation A, there is a k-linear isomorphism between representation morphisms Hom(k[G], A) and A.

theorem Rep.leftRegularHomEquiv_symm_single {k : Type u} {G : Type v} [CommRing k] [Monoid G] {A : Rep.{max u v, u, v} k G} (x : ↑A) (g : G) : ((Hom.hom (A.leftRegularHomEquiv.symm x)) fun₀ | g => 1) = (A.ρ g) x