mathlib3 documentation

representation_theory.fdRep

fdRep k G is the category of finite dimensional k-linear representations of G. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If V : fdRep k G, there is a coercion that allows you to treat V as a type, and this type comes equipped with module k V and finite_dimensional k V instances. Also V.ρ gives the homomorphism G →* (V →ₗ[k] V).

Conversely, given a homomorphism ρ : G →* (V →ₗ[k] V), you can construct the bundled representation as Rep.of ρ.

We verify that fdRep k G is a k-linear monoidal category, and rigid when G is a group.

fdRep k G has all finite limits.

TODO #

source
@[protected, instance]
def fdRep.preadditive (k G : Type u) [field k] [monoid G] :
category_theory.preadditive (fdRep k G)
source
@[protected, instance]
def fdRep.concrete_category (k G : Type u) [field k] [monoid G] :
category_theory.concrete_category (fdRep k G)
source
@[reducible]
def fdRep (k G : Type u) [field k] [monoid G] :
Type (u+1)

The category of finite dimensional k-linear representations of a monoid G.

source
@[protected, instance]
def fdRep.has_finite_limits (k G : Type u) [field k] [monoid G] :
category_theory.limits.has_finite_limits (fdRep k G)
source
@[protected, instance]
def fdRep.large_category (k G : Type u) [field k] [monoid G] :
category_theory.large_category (fdRep k G)
source
@[protected, instance]
def fdRep.category_theory.linear {k G : Type u} [field k] [monoid G] :
category_theory.linear k (fdRep k G)
Equations
source
@[protected, instance]
def fdRep.has_coe_to_sort {k G : Type u} [field k] [monoid G] :
has_coe_to_sort (fdRep k G) (Type u)
Equations
source
@[protected, instance]
def fdRep.add_comm_group {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
add_comm_group ↥V
Equations
source
@[protected, instance]
def fdRep.module {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
module k ↥V
Equations
source
@[protected, instance]
def fdRep.finite_dimensional {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
finite_dimensional k ↥V
source
@[protected, instance]
def fdRep.quiver.hom.finite_dimensional {k G : Type u} [field k] [monoid G] (V W : fdRep k G) :
finite_dimensional k (V ⟶ W)

All hom spaces are finite dimensional.

source
def fdRep.ρ {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
G →* ↥V →ₗ[k] ↥V

The monoid homomorphism corresponding to the action of G onto V : fdRep k G.

Equations
source
def fdRep.iso_to_linear_equiv {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V ≅ W) :
↥V ≃ₗ[k] ↥W

The underlying linear_equiv of an isomorphism of representations.

Equations
source
theorem fdRep.iso.conj_ρ {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V ≅ W) (g : G) :
⇑(W.ρ) g = ⇑((fdRep.iso_to_linear_equiv i).conj) (⇑(V.ρ) g)
source
@[simp]
theorem fdRep.of_ρ {k G : Type u} [field k] [monoid G] {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V] (ρ : representation k G V) :
(fdRep.of ρ).ρ = ρ
source
def fdRep.of {k G : Type u} [field k] [monoid G] {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V] (ρ : representation k G V) :
fdRep k G

Lift an unbundled representation to fdRep.

Equations
source
@[protected, instance]
def fdRep.Rep.category_theory.has_forget₂ {k G : Type u} [field k] [monoid G] :
category_theory.has_forget₂ (fdRep k G) (Rep k G)
Equations
source
theorem fdRep.forget₂_ρ {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
((category_theory.forget₂ (fdRep k G) (Rep k G)).obj V).ρ = V.ρ
source
@[protected, instance]
def fdRep.category_theory.limits.has_kernels {k G : Type u} [field k] [monoid G] :
category_theory.limits.has_kernels (fdRep k G)
source
theorem fdRep.finrank_hom_simple_simple {k G : Type u} [field k] [monoid G] [is_alg_closed k] (V W : fdRep k G) [category_theory.simple V] [category_theory.simple W] :
finite_dimensional.finrank k (V ⟶ W) = ite (nonempty (V ≅ W)) 1 0
source
def fdRep.forget₂_hom_linear_equiv {k G : Type u} [field k] [monoid G] (X Y : fdRep k G) :
((category_theory.forget₂ (fdRep k G) (Rep k G)).obj X ⟶ (category_theory.forget₂ (fdRep k G) (Rep k G)).obj Y) ≃ₗ[k] X ⟶ Y

The forgetful functor to Rep k G preserves hom-sets and their vector space structure

Equations
source
@[protected, instance]
noncomputable def fdRep.category_theory.right_rigid_category {k G : Type u} [field k] [group G] :
category_theory.right_rigid_category (fdRep k G)
Equations
source
noncomputable def fdRep.dual_tensor_iso_lin_hom_aux {k G V : Type u} [field k] [group G] [add_comm_group V] [module k V] [finite_dimensional k V] (ρV : representation k G V) (W : fdRep k G) :
(fdRep.of ρV.dual ⊗ W).V ≅ (fdRep.of (ρV.lin_hom W.ρ)).V

Auxiliary definition for fdRep.dual_tensor_iso_lin_hom.

Equations
source
noncomputable def fdRep.dual_tensor_iso_lin_hom {k G V : Type u} [field k] [group G] [add_comm_group V] [module k V] [finite_dimensional k V] (ρV : representation k G V) (W : fdRep k G) :
fdRep.of ρV.dual ⊗ W ≅ fdRep.of (ρV.lin_hom W.ρ)

When V and W are finite dimensional representations of a group G, the isomorphism dual_tensor_hom_equiv k V W of vector spaces induces an isomorphism of representations.

Equations
source
@[simp]
theorem fdRep.dual_tensor_iso_lin_hom_hom_hom {k G V : Type u} [field k] [group G] [add_comm_group V] [module k V] [finite_dimensional k V] (ρV : representation k G V) (W : fdRep k G) :
(fdRep.dual_tensor_iso_lin_hom ρV W).hom.hom = dual_tensor_hom k V ↥W