Documentation

Mathlib.RepresentationTheory.Invariants

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)] :

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

Equations
Instances For
    @[simp]

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

    @[simp]

    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) :

    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' := }
    Instances For
      @[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)] :

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

      Equations
      Instances For
        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 : GroupCat} {X : Rep k G} {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 : GroupCat} (X : Rep k G) (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.
        Instances For
          @[simp]
          theorem Representation.linHom.invariantsEquivRepHom_symm_apply_coe {k : Type u} [CommRing k] {G : GroupCat} (X : Rep k G) (Y : Rep k G) (f : X Y) :
          @[simp]
          theorem Representation.linHom.invariantsEquivRepHom_apply_hom {k : Type u} [CommRing k] {G : GroupCat} (X : Rep k G) (Y : Rep k G) (f : (X.linHom Y).invariants) :
          noncomputable def Representation.linHom.invariantsEquivFdRepHom {k : Type u} [Field k] {G : GroupCat} (X : FdRep k G) (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.
          Instances For