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]
Equations
- One or more equations did not get rendered due to their size.
@[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.ρ
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
Instances For
def
Rep.Hom.Simps.hom
{k : Type u}
{G : Type v}
[Semiring k]
[Monoid G]
(A B : Rep k G)
(f : A.Hom B)
:
A.ρ.IntertwiningMap B.ρ
Use the ConcreteCategory.hom projection for @[simps] lemmas.
Equations
- Rep.Hom.Simps.hom A B f = f.hom
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)
:
@[implicit_reducible]
Equations
- Rep.instInhabited = { default := Rep.of (Representation.trivial k G PUnit.{?u.20 + 1}) }
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.
Equations
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 σ)
:
The morphisms between two objects in Rep k G has an equivalence to the intertwining maps
between their underlying representations.
Equations
- Rep.homEquiv = { toFun := Rep.Hom.hom, invFun := Rep.ofHom, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[implicit_reducible]
Equations
- Rep.instAddHom = { add := fun (f g : A ⟶ B) => Rep.ofHom (Rep.Hom.hom f + Rep.Hom.hom g) }
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 σ)
:
@[implicit_reducible]
Equations
- Rep.instSubHom = { sub := fun (f g : A ⟶ B) => Rep.ofHom (Rep.Hom.hom f - Rep.Hom.hom g) }
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)
Equations
- One or more equations did not get rendered due to their size.
@[implicit_reducible]
Equations
- Rep.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
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.
Equations
- Rep.trivial k G V = Rep.of (Representation.trivial k G 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]
noncomputable abbrev
Rep.ofMulAction
(k : Type u)
(G : Type v)
[Ring k]
[Monoid G]
(H : Type w')
[MulAction G H]
:
Rep 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.
Equations
- Rep.ofMulAction k G H = Rep.of (Representation.ofMulAction k G H)
Instances For
@[reducible, inline]
The k-linear G-representation on k[G], induced by left multiplication.
Equations
- Rep.leftRegular k G = Rep.ofMulAction k G G
Instances For
@[reducible, inline]
The k-linear G-representation on k[Gⁿ], induced by left multiplication.
Equations
- Rep.diagonal k G n = Rep.ofMulAction k G (Fin n → G)
Instances For
@[reducible, inline]
The natural isomorphism between the representations on k[G¹] and k[G] induced by left
multiplication in G.
Equations
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.
Equations
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.
Equations
- Rep.ofDistribMulAction k G A = Rep.of (Representation.ofDistribMulAction k G 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.
Equations
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.
Equations
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)
:
Given an R-algebra S, the ℤ-linear representation associated to the natural action of
S ≃ₐ[R] S on Sˣ.
Equations
- Rep.ofAlgebraAutOnUnits R S = Rep.ofMulDistribMulAction (S ≃ₐ[R] S) Sˣ
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.leftRegularHom
{k : Type u}
{G : Type v}
[Ring k]
[Monoid G]
(A : Rep k G)
(x : ↑A)
:
Given an element x : A, there is a natural morphism of representations k[G] ⟶ A sending
g ↦ A.ρ(g)(x).
Equations
- A.leftRegularHom x = Rep.ofHom { toLinearMap := (Finsupp.lift (↑A) k G) fun (g : G) => (A.ρ g) x, isIntertwining' := ⋯ }
Instances For
@[reducible, inline]
abbrev
Rep.subrepresentation
{k : Type u}
{G : Type v}
[Ring k]
[Monoid 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.
Equations
- A.subrepresentation W le_comap = Rep.of (A.ρ.subrepresentation W le_comap)
Instances For
def
Rep.subtype
{k : Type u}
{G : Type v}
[Ring k]
[Monoid 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
@[reducible, inline]
abbrev
Rep.quotient
{k : Type u}
{G : Type v}
[Ring k]
[Monoid 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}
{G : Type v}
[Ring k]
[Monoid 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.
Equations
- One or more equations did not get rendered due to their size.
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)
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
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]
Equations
- Rep.instModuleHom = { toSMul := Rep.instSMulHom, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
@[implicit_reducible]
instance
Rep.instLinear
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
CategoryTheory.Linear k (Rep k G)
Equations
- Rep.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }
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))
@[reducible, inline]
The equivalence between IntertwiningMaps and morphism between X Y : Rep k G is linear.
Equations
- X.homLinearEquiv Y = { toFun := Rep.homEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Rep.homEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[implicit_reducible]
Equations
- One or more equations did not get rendered due to their size.
@[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]
Equations
- One or more equations did not get rendered due to their size.
@[implicit_reducible]
noncomputable instance
Rep.instSymmetricCategory
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
:
Equations
- Rep.instSymmetricCategory = { toBraidedCategory := Rep.instBraidedCategory, symmetry := ⋯ }
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⁻¹).
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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]
Equations
- One or more equations did not get rendered due to their size.
@[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
noncomputable def
Rep.MonoidalClosed.linearHomEquiv
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep k G)
:
There is a k-linear isomorphism between the sets of representation morphisms Hom(A ⊗ B, C)
and Hom(B, Homₖ(A, C)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Rep.MonoidalClosed.linearHomEquivComm
{k : Type u}
[CommRing k]
{G : Type v}
[Group G]
(A B C : Rep k G)
:
There is a k-linear isomorphism between the sets of representation morphisms Hom(A ⊗ B, C)
and Hom(A, Homₖ(B, C)).
Equations
- Rep.MonoidalClosed.linearHomEquivComm A B C = (CategoryTheory.Linear.homCongr k (β_ A B) (CategoryTheory.Iso.refl C)).trans (Rep.MonoidalClosed.linearHomEquiv B A C)
Instances For
@[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
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.
Equations
- Rep.normNatTrans = { app := Rep.norm, naturality := ⋯ }
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.freeLift
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
{α : Type u'}
(A : Rep k G)
(f : α → ↑A)
:
Given f : α → A, the natural representation morphism (α →₀ k[G]) ⟶ A sending
single a (single g r) ↦ r • A.ρ g (f a).
Equations
- Rep.freeLift k G A f = Rep.ofHom (A.ρ.freeLift f)
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.freeLiftLEquiv
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
(α : Type u')
(A : Rep k G)
:
The natural linear equivalence between functions α → A and representation morphisms
(α →₀ k[G]) ⟶ A.
Equations
- Rep.freeLiftLEquiv k G α A = ((Rep.free k G α).homLinearEquiv A).trans (A.ρ.freeLiftLEquiv α)
Instances For
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).
Equations
- Rep.finsuppTensorLeft k G A B α = Rep.mkIso (A.ρ.finsuppTensorLeft 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).
Equations
- Rep.finsuppTensorRight k G A B α = Rep.mkIso (A.ρ.finsuppTensorRight 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₂).
Equations
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].
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable instance
Rep.instMonoidalActionTypeLinearization
(k : Type u)
(G : Type v)
[CommRing k]
[Monoid G]
:
(linearization k G).Monoidal
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
Rep.leftRegularHomEquiv
{k : Type u}
{G : Type v}
[CommRing k]
[Monoid G]
(A : Rep k G)
:
Given a k-linear G-representation A, there is a k-linear isomorphism between
representation morphisms Hom(k[G], A) and A.
Equations
- A.leftRegularHomEquiv = ((Rep.leftRegular k G).homLinearEquiv A).trans A.ρ.leftRegularMapEquiv