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.ρ.
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
Instances For
@[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 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.
Instances For
@[implicit_reducible]
@[implicit_reducible]
instance
Rep.instConcreteCategoryIntertwiningMapVρ
{k : Type u}
{G : Type v}
[Semiring k]
[Monoid G]
:
CategoryTheory.ConcreteCategory (Rep k G) fun (A B : Rep k G) => A.ρ.IntertwiningMap B.ρ
@[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 σ)
:
Typecheck an IntertwiningMap as a morphism in Rep.
Instances For
@[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 σ)
:
@[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}
:
@[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 τ)
:
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)
:
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 σ)
:
An equiv between the underlying representations induce isomorphism between objects in
Rep k G.
Instances For
@[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)
:
@[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 σ)
:
@[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 σ)
:
@[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)
:
@[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 σ)
:
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 σ)
:
theorem
Rep.hom_comp_toLinearMap
{k : Type u}
{G : Type v}
[Semiring k]
[Monoid G]
{A B C : Rep k G}
(f : A ⟶ B)
(g : B ⟶ C)
:
(Hom.hom (CategoryTheory.CategoryStruct.comp f g)).toLinearMap = (Hom.hom g).toLinearMap ∘ₗ (Hom.hom f).toLinearMap
@[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}
:
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 : ℕ)
:
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 σ)
:
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 σ)
:
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 : ℤ)
:
@[implicit_reducible]
instance
Rep.instAddCommGroupHom
{k : Type u}
{G : Type v}
[Semiring k]
[Monoid G]
{A B : Rep k G}
:
AddCommGroup (A ⟶ B)
@[implicit_reducible]
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 ι)
:
@[reducible, inline]
abbrev
Rep.trivial
(k : Type u)
(G : Type v)
[Semiring k]
[Monoid G]
(V : Type w)
[AddCommGroup V]
[Module k V]
:
Rep k G
The trivial k-linear G-representation on a k-module V.
Instances For
theorem
Rep.trivial_ρ
{k : Type u}
{G : Type v}
[Semiring k]
[Monoid G]
{V : Type w}
[AddCommGroup V]
[Module k V]
(g : G)
:
Given a representation A of a commutative monoid G, the map ρ_A(g) is a representation
morphism A ⟶ A for any g : G.
Instances For
@[simp]
theorem
Rep.applyAsHom_apply
{k : Type u}
[Semiring k]
{G : Type v}
[CommMonoid G]
{A : Rep k G}
(g : G)
(x : ↑A)
:
theorem
Rep.applyAsHom_comm
{k : Type u}
[Semiring k]
{G : Type v}
[CommMonoid G]
{A B : Rep k G}
(f : A ⟶ B)
(g : G)
:
theorem
Rep.applyAsHom_comm_assoc
{k : Type u}
[Semiring k]
{G : Type v}
[CommMonoid G]
{A B : Rep k G}
(f : A ⟶ B)
(g : G)
{Z : Rep k G}
(h : B ⟶ Z)
:
theorem
Rep.applyAsHom_comm_apply
{k : Type u}
[Semiring k]
{G : Type v}
[CommMonoid G]
{A B : Rep 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]
The natural isomorphism between the representations on k[G¹] and k[G] induced by left
multiplication in G.
Instances For
@[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]
:
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.
Instances For
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 k G
Turns a k-module A with a compatible DistribMulAction of a monoid G into a
k-linear G-representation on A.
Instances For
@[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)
:
def
Rep.ofMulDistribMulAction
(M : Type u_1)
(G : Type u_2)
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
:
Turns a CommGroup G with a MulDistribMulAction of a monoid M into a
ℤ-linear M-representation on Additive G.
Instances For
def
Rep.toAdditive
{M : Type u_1}
{G : Type u_2}
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
:
Unfolds ofMulDistribMulAction; useful to keep track of additivity.
Instances For
@[simp]
theorem
Rep.toAdditive_apply
{M : Type u_1}
{G : Type u_2}
[Monoid M]
[CommGroup G]
[MulDistribMulAction M G]
(a : ↑(ofMulDistribMulAction M G))
:
@[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))
:
@[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)
:
@[reducible, inline]
abbrev
Rep.subrepresentation
{k : Type u}
[Ring k]
{G : Type v}
[CommMonoid G]
(A : Rep k G)
(W : Submodule k ↑A)
(le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W)
:
Rep k G
Given a k-linear G-representation (V, ρ), this is the representation defined by
restricting ρ to a G-invariant k-submodule of V.
Instances For
def
Rep.subtype
{k : Type u}
[Ring k]
{G : Type v}
[CommMonoid G]
(A : Rep k G)
(W : Submodule k ↑A)
(le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W)
:
The natural inclusion of a subrepresentation into the ambient representation.
Instances For
@[simp]
theorem
Rep.subtype_hom_toFun
{k : Type u}
[Ring k]
{G : Type v}
[CommMonoid G]
(A : Rep k G)
(W : Submodule k ↑A)
(le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W)
(self : ↥W)
:
@[reducible, inline]
abbrev
Rep.quotient
{k : Type u}
[Ring k]
{G : Type v}
[CommMonoid G]
(A : Rep k G)
(W : Submodule k ↑A)
(le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W)
:
Rep 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 ρ.
Instances For
@[simp]
theorem
Rep.mkQ_hom_toFun
{k : Type u}
[Ring k]
{G : Type v}
[CommMonoid G]
(A : Rep k G)
(W : Submodule k ↑A)
(le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W)
(a✝ : ↑A)
:
def
Rep.trivialFunctor
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
:
CategoryTheory.Functor (ModuleCat k) (Rep k G)
The functor equipping a module with the trivial representation.
Instances For
instance
Rep.instIsTrivialObjModuleCatTrivialFunctor
{k : Type u}
{G : Type v}
[Ring k]
[Monoid G]
(X : ModuleCat k)
:
((trivialFunctor k G).obj X).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]
:
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 k G) (ModuleCat k)
instance
Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier
{k : Type u}
{G : Type v}
[Ring k]
[Monoid G]
:
(CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).Faithful
theorem
Rep.RepToAction_obj
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
(X : Rep k G)
:
(RepToAction k G).obj X = { V := ModuleCat.of k ↑X, ρ := (ModuleCat.of k ↑X).endRingEquiv.symm.toMonoidHom.comp X.ρ }
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 k G) (ModuleCat k)).Additive
@[reducible, inline]
abbrev
Rep.forgetNatIsoActionForget
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
:
CategoryTheory.forget₂ (Rep 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.
Instances For
instance
Rep.instMonoModuleCatToModuleCatHom
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
{A B : Rep k G}
(f : A ⟶ B)
[CategoryTheory.Mono f]
:
instance
Rep.instEpiModuleCatToModuleCatHom
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
{A B : Rep k G}
(f : A ⟶ B)
[CategoryTheory.Epi f]
:
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)
:
@[implicit_reducible]
instance
Rep.instLinear
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
CategoryTheory.Linear k (Rep k G)
instance
Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
CategoryTheory.Functor.Linear k (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))
@[implicit_reducible]
@[simp]
@[simp]
@[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)
:
@[simp]
theorem
Rep.hom_hom_associator
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
{X Y Z : Rep k G}
:
Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ)
instance
Rep.instMonoidalLinear
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
CategoryTheory.MonoidalLinear k (Rep k G)
@[implicit_reducible]
@[implicit_reducible]
noncomputable instance
Rep.instSymmetricCategory
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
noncomputable def
Rep.ihom
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A : Rep k G)
:
CategoryTheory.Functor (Rep k G) (Rep 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⁻¹).
Instances For
noncomputable def
Rep.tensorHomEquiv
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep k G)
:
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.
Instances For
@[simp]
theorem
Rep.tensorHomEquiv_symm_apply
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep 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 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]
@[simp]
theorem
Rep.ihom_ev_app_hom
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B : Rep 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 k G)
:
(Hom.hom ((CategoryTheory.ihom.coev A).app B)).toLinearMap = (TensorProduct.mk k ↑A ↑((CategoryTheory.Functor.id (Rep k G)).obj B)).flip
@[simp]
theorem
Rep.MonoidalClosed.linearHomEquiv_hom
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep 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 k G)
(f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C)
:
theorem
Rep.MonoidalClosed.linearHomEquiv_symm_hom
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep k G)
(f : B ⟶ (CategoryTheory.ihom A).obj 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 k G)
(f : A ⟶ (CategoryTheory.ihom B).obj C)
:
(Hom.hom ((linearHomEquivComm A B C).symm f)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).toLinearMap
theorem
Rep.free_ext
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
{α : Type u'}
(A : Rep k G)
(f g : free k G α ⟶ A)
(h :
∀ (i : α), (Hom.hom f) (Finsupp.single i (Finsupp.single 1 1)) = (Hom.hom g) (Finsupp.single i (Finsupp.single 1 1)))
:
@[reducible, inline]
noncomputable abbrev
Rep.finsuppTensorLeft
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
(A B : Rep k G)
(α : Type u)
[DecidableEq α]
:
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).
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.finsuppTensorRight
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
(A B : Rep k G)
(α : Type u)
[DecidableEq α]
:
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).
Instances For
@[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₂).
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.linearization
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
:
CategoryTheory.Functor (Action (Type w) G) (Rep k G)
The monoidal functor sending a type H with a G-action to the induced k-linear
G-representation on k[H].
Instances For
@[implicit_reducible]
noncomputable instance
Rep.instMonoidalActionTypeLinearization
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
:
(linearization k G).Monoidal
@[reducible, inline]
noncomputable abbrev
Rep.linearizationOfMulActionIso
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
(H : Type u)
[MulAction 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.