Subspace of invariants a group representation

This file introduces the subspace of invariants of a group representation and proves basic results about it. The main tool used is the average of all elements of the group, seen as an element of MonoidAlgebra k G. The action of this special element gives a projection onto the subspace of invariants. In order for the definition of the average element to make sense, we need to assume for most of the results that the order of G is invertible in k (e. g. k has characteristic 0).

noncomputable def GroupAlgebra.average (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] : MonoidAlgebra k G

The average of all elements of the group G, considered as an element of MonoidAlgebra k G.

Equations

• GroupAlgebra.average k G = ⅟↑(Fintype.card G) • ∑ g : G, (MonoidAlgebra.of k G) g

@[simp]

theorem GroupAlgebra.mul_average_left (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (g : G) : Finsupp.single g 1 * GroupAlgebra.average k G = GroupAlgebra.average k G

average k G is invariant under left multiplication by elements of G.

@[simp]

theorem GroupAlgebra.mul_average_right (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (g : G) : GroupAlgebra.average k G * Finsupp.single g 1 = GroupAlgebra.average k G

average k G is invariant under right multiplication by elements of G.

noncomputable def Representation.invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Submodule k V

The subspace of invariants, consisting of the vectors fixed by all elements of G.

Equations

• ρ.invariants = { carrier := {v : V | ∀ (g : G), (ρ g) v = v}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Representation.mem_invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (v : V) : v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v

theorem Representation.invariants_eq_inter {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.invariants.carrier = ⋂ (g : G), Function.fixedPoints ⇑(ρ g)

theorem Representation.invariants_eq_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] : ρ.invariants = ⊤

noncomputable def Representation.averageMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] : V →ₗ[k] V

The action of average k G gives a projection map onto the subspace of invariants.

Equations

• ρ.averageMap = ρ.asAlgebraHom (GroupAlgebra.average k G)

theorem Representation.averageMap_invariant {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] (v : V) : ρ.averageMap v ∈ ρ.invariants

The averageMap sends elements of V to the subspace of invariants.

theorem Representation.averageMap_id {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] (v : V) (hv : v ∈ ρ.invariants) : ρ.averageMap v = v

The averageMap acts as the identity on the subspace of invariants.

theorem Representation.isProj_averageMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] : LinearMap.IsProj ρ.invariants ρ.averageMap

theorem Representation.linHom.mem_invariants_iff_comm {k : Type u} [CommRing k] {G : Grp} {X Y : Rep k ↑G} (f : ↑X.V →ₗ[k] ↑Y.V) (g : ↑G) : ((X.ρ.linHom Y.ρ) g) f = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

noncomputable def Representation.linHom.invariantsEquivRepHom {k : Type u} [CommRing k] {G : Grp} (X Y : Rep k ↑G) : ↥(X.ρ.linHom Y.ρ).invariants ≃ₗ[k] X ⟶ Y

The invariants of the representation linHom X.ρ Y.ρ correspond to the representation homomorphisms from X to Y.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.linHom.invariantsEquivRepHom_symm_apply_coe {k : Type u} [CommRing k] {G : Grp} (X Y : Rep k ↑G) (f : X ⟶ Y) : ↑((Representation.linHom.invariantsEquivRepHom X Y).symm f) = f.hom.hom

@[simp]

theorem Representation.linHom.invariantsEquivRepHom_apply_hom_hom {k : Type u} [CommRing k] {G : Grp} (X Y : Rep k ↑G) (f : ↥(X.ρ.linHom Y.ρ).invariants) : ((Representation.linHom.invariantsEquivRepHom X Y) f).hom.hom = ↑f

noncomputable def Representation.linHom.invariantsEquivFDRepHom {k : Type u} [Field k] {G : Grp} (X Y : FDRep k ↑G) : ↥(Representation.linHom X.ρ Y.ρ).invariants ≃ₗ[k] X ⟶ Y

The invariants of the representation linHom X.ρ Y.ρ correspond to the representation homomorphisms from X to Y.

Equations

• One or more equations did not get rendered due to their size.