The unitary dual of a group

def UnitaryDual (𝕜 : Type u) (G : Type u_2) [RCLike 𝕜] [Group G] : Type (max (u + 1) u_2)

Equations

• UnitaryDual 𝕜 G = CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (ψ : UnitaryRep 𝕜 G) => ψ.ρ.toRepresentation.IsIrreducible)

def UnitaryDual.E {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] (ψ : UnitaryDual 𝕜 G) : Type u

Equations

• ψ.E = (Quotient.out ψ).obj.E

@[implicit_reducible]

noncomputable instance UnitaryDual.instNormedAddCommGroupE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : NormedAddCommGroup ψ.E

Equations

• UnitaryDual.instNormedAddCommGroupE = (Quotient.out ψ).obj.normedAddCommGroup

@[implicit_reducible]

noncomputable instance UnitaryDual.instInnerProductSpaceE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : InnerProductSpace 𝕜 ψ.E

Equations

• UnitaryDual.instInnerProductSpaceE = (Quotient.out ψ).obj.innerProductSpace

instance UnitaryDual.instCompleteSpaceE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : CompleteSpace ψ.E

instance UnitaryDual.instFiniteDimensionalE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : FiniteDimensional 𝕜 ψ.E

noncomputable def UnitaryDual.ρ {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] (ψ : UnitaryDual 𝕜 G) : UnitaryRepresentation 𝕜 G ψ.E

Equations

• ψ.ρ = (Quotient.out ψ).obj.ρ

@[simp]

theorem UnitaryDual.isIrreducible_ρ {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : ψ.ρ.toRepresentation.IsIrreducible

instance UnitaryDual.instNontrivialE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {ψ : UnitaryDual 𝕜 G} : Nontrivial ψ.E

@[implicit_reducible]

noncomputable instance UnitaryDual.instCoeFunForallLinearIsometryEquivIdE {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] : CoeFun (UnitaryDual 𝕜 G) fun (ψ : UnitaryDual 𝕜 G) => G → ψ.E ≃ₗᵢ[𝕜] ψ.E

Equations

• UnitaryDual.instCoeFunForallLinearIsometryEquivIdE = { coe := fun (ψ : UnitaryDual 𝕜 G) => ⇑ψ.ρ }

@[implicit_reducible]

noncomputable instance UnitaryDual.instDecidableEq {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] : DecidableEq (UnitaryDual 𝕜 G)

Equations

• UnitaryDual.instDecidableEq = Classical.decEq (UnitaryDual 𝕜 G)

noncomputable def UnitaryDual.ofUnitaryRepresentation {𝕜 : Type u} {G : Type u_2} [RCLike 𝕜] [Group G] {E : Type u} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (ρ : UnitaryRepresentation 𝕜 G E) (hρ : ρ.toRepresentation.IsIrreducible) : UnitaryDual 𝕜 G

Equations

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

@[implicit_reducible]

instance UnitaryDual.instFintypeComplexOfFinite {G : Type u_2} [Group G] [Finite G] : Fintype (UnitaryDual ℂ G)

Equations

• UnitaryDual.instFintypeComplexOfFinite = sorry

@[simp]

theorem UnitaryDual.finrank_E_eq_one {G : Type u_2} [CommGroup G] (ψ : UnitaryDual ℂ G) : Module.finrank ℂ ψ.E = 1