The category of unitary representations of a group

For 𝕜 = ℝ, ℂ, this file defines the category of 𝕜-valued unitary representations

structure UnitaryRep (𝕜 : Type u_2) (G : Type u_3) [RCLike 𝕜] [Group G] : Type (max (max (u + 1) u_2) u_3)

The category of unitary representations of a group G and their morphisms.

• of :: (
• E : Type u

  The underlying finite-dimensional Hilbert space of an object in UnitaryRep 𝕜 G

• normedAddCommGroup : NormedAddCommGroup self.E
• innerProductSpace : InnerProductSpace 𝕜 self.E
• completeSpace : CompleteSpace self.E
• ρ : UnitaryRepresentation 𝕜 G self.E

  The underlying unitary representation of an object in UnitaryRep 𝕜 G

• )

@[implicit_reducible]

instance UnitaryRep.instCoeSortType {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : CoeSort (UnitaryRep 𝕜 G) (Type u)

Equations

• UnitaryRep.instCoeSortType = { coe := UnitaryRep.E }

structure UnitaryRep.Hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] (A B : UnitaryRep 𝕜 G) : Type u

The type of morphisms in UnitaryRep.{u} 𝕜 G.

• hom' : A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation

  The underlying G-equivariant linear map.

theorem UnitaryRep.Hom.ext_iff {𝕜 : Type u_2} {G : Type u_3} {inst✝ : RCLike 𝕜} {inst✝¹ : Group G} {A B : UnitaryRep 𝕜 G} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

theorem UnitaryRep.Hom.ext {𝕜 : Type u_2} {G : Type u_3} {inst✝ : RCLike 𝕜} {inst✝¹ : Group G} {A B : UnitaryRep 𝕜 G} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y

@[implicit_reducible]

noncomputable instance UnitaryRep.instCategory {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : CategoryTheory.Category.{u, max (max (u + 1) u_3) u_2} (UnitaryRep 𝕜 G)

Equations

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

@[implicit_reducible]

instance UnitaryRep.instConcreteCategoryIntertwiningMapEToRepresentationρ {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : CategoryTheory.ConcreteCategory (UnitaryRep 𝕜 G) fun (A B : UnitaryRep 𝕜 G) => A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation

Equations

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

@[reducible, inline]

abbrev UnitaryRep.Hom.hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A.Hom B) : A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation

Turn a morphism in UnitaryRep back into an IntertwiningMap.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev UnitaryRep.ofHom {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) : { E := E, normedAddCommGroup := inst✝, innerProductSpace := inst✝¹, completeSpace := inst✝², ρ := ρ } ⟶ { E := F, normedAddCommGroup := inst✝³, innerProductSpace := inst✝⁴, completeSpace := inst✝⁵, ρ := σ }

Typecheck an IntertwiningMap as a morphism in UnitaryRep.

Equations

• UnitaryRep.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def UnitaryRep.Hom.Simps.hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A.Hom B) : A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• UnitaryRep.Hom.Simps.hom f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem UnitaryRep.hom_id {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A : UnitaryRep 𝕜 G} : Hom.hom (CategoryTheory.CategoryStruct.id A) = 1

theorem UnitaryRep.id_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A : UnitaryRep 𝕜 G} (a : A.E) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem UnitaryRep.hom_comp {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B C : UnitaryRep 𝕜 G} (f : A ⟶ B) (g : B ⟶ C) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem UnitaryRep.comp_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B C : UnitaryRep 𝕜 G} (f : A ⟶ B) (g : B ⟶ C) (a : A.E) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

theorem UnitaryRep.hom_ext {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) : f = g

theorem UnitaryRep.hom_ext_iff {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

theorem UnitaryRep.hom_comm_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) (g : G) (a : A.E) : (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

@[simp]

theorem UnitaryRep.hom_ofHom {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) : Hom.hom (ofHom f) = f

@[simp]

theorem UnitaryRep.ofHom_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) : ofHom (Hom.hom f) = f

@[simp]

theorem UnitaryRep.ofHom_id {𝕜 : Type u_2} {G : Type u_3} {E : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {ρ : UnitaryRepresentation 𝕜 G E} : ofHom (Representation.IntertwiningMap.id ρ.toRepresentation) = CategoryTheory.CategoryStruct.id { E := E, normedAddCommGroup := inst✝, innerProductSpace := inst✝¹, completeSpace := inst✝², ρ := ρ }

@[simp]

theorem UnitaryRep.ofHom_comp {𝕜 : Type u_2} {G : Type u_3} {E F H : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} {τ : UnitaryRepresentation 𝕜 G H} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) (g : σ.toRepresentation.IntertwiningMap τ.toRepresentation) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem UnitaryRep.ofHom_apply {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) (x : E) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem UnitaryRep.inv_hom_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (e : A ≅ B) (x : A.E) : (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

theorem UnitaryRep.hom_inv_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (e : A ≅ B) (x : B.E) : (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

theorem UnitaryRep.forget_obj {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A : UnitaryRep 𝕜 G} : (CategoryTheory.forget (UnitaryRep 𝕜 G)).obj A = A.E

theorem UnitaryRep.forget_map {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) : ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (UnitaryRep 𝕜 G)).map f)) = ⇑(CategoryTheory.ConcreteCategory.hom f)

noncomputable def UnitaryRep.mkIso {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) : { E := E, normedAddCommGroup := inst✝, innerProductSpace := inst✝¹, completeSpace := inst✝², ρ := ρ } ≅ { E := F, normedAddCommGroup := inst✝³, innerProductSpace := inst✝⁴, completeSpace := inst✝⁵, ρ := σ }

An equiv between the underlying representations induce isomorphism between objects in UnitaryRep 𝕜 G.

Equations

• UnitaryRep.mkIso e = { hom := UnitaryRep.ofHom ↑e, inv := UnitaryRep.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem UnitaryRep.mkIso_hom_hom_apply {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) (x : E) : (Hom.hom (mkIso e).hom) x = (↑e).toLinearMap x

@[simp]

theorem UnitaryRep.mkIso_hom_hom_toLinearMap {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) : (Hom.hom (mkIso e).hom).toLinearMap = (↑e).toLinearMap

@[simp]

theorem UnitaryRep.mkIso_inv_hom_toLinearMap {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) : (Hom.hom (mkIso e).inv).toLinearMap = (↑e.symm).toLinearMap

@[simp]

theorem UnitaryRep.mkIso_inv_hom_apply {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) (y : F) : (Hom.hom (mkIso e).inv) y = e.symm y

@[simp]

theorem UnitaryRep.mkIso_hom_hom {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (e : ρ.toRepresentation.Equiv σ.toRepresentation) : Hom.hom (mkIso e).hom = ↑e

noncomputable def UnitaryRep.equivOfIso {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (i : A ≅ B) : A.ρ.toRepresentation.Equiv B.ρ.toRepresentation

The equivalence between representations induced from iso between objects in UnitaryRep 𝕜 G.

Equations

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

@[simp]

theorem UnitaryRep.equivOfIso_invFun {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (i : A ≅ B) (a : B.E) : (equivOfIso i).invFun a = (CategoryTheory.ConcreteCategory.hom i.inv) a

@[simp]

theorem UnitaryRep.equivOfIso_toFun {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (i : A ≅ B) (a : A.E) : (equivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

instance UnitaryRep.reflectsIsomorphisms_forget {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : (CategoryTheory.forget (UnitaryRep 𝕜 G)).ReflectsIsomorphisms

theorem UnitaryRep.hom_bijective {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Function.Bijective Hom.hom

theorem UnitaryRep.hom_injective {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Function.Injective Hom.hom

Convenience shortcut for UnitaryRep.hom_bijective.injective.

theorem UnitaryRep.hom_surjective {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Function.Surjective Hom.hom

Convenience shortcut for UnitaryRep.hom_bijective.surjective.

def UnitaryRep.homEquiv {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : (A ⟶ B) ≃ A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation

The morphisms between two objects in UnitaryRep 𝕜 G are equivalent to the intertwining maps between their underlying representations.

Equations

• UnitaryRep.homEquiv = { toFun := UnitaryRep.Hom.hom, invFun := UnitaryRep.ofHom, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem UnitaryRep.homEquiv_symm_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A.ρ.toRepresentation.IntertwiningMap B.ρ.toRepresentation) : homEquiv.symm f = ofHom f

@[simp]

theorem UnitaryRep.homEquiv_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A.Hom B) : homEquiv f = f.hom

@[implicit_reducible]

noncomputable instance UnitaryRep.instAddHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Add (A ⟶ B)

Equations

• UnitaryRep.instAddHom = { add := fun (f g : A ⟶ B) => UnitaryRep.ofHom (UnitaryRep.Hom.hom f + UnitaryRep.Hom.hom g) }

theorem UnitaryRep.ofHom_add {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f g : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) : ofHom (f + g) = ofHom f + ofHom g

theorem UnitaryRep.add_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f g : A ⟶ B) : Hom.hom (f + g) = Hom.hom f + Hom.hom g

theorem UnitaryRep.hom_comp_toLinearMap {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B C : UnitaryRep 𝕜 G} (f : A ⟶ B) (g : B ⟶ C) : (Hom.hom (CategoryTheory.CategoryStruct.comp f g)).toLinearMap = (Hom.hom g).toLinearMap ∘ₗ (Hom.hom f).toLinearMap

theorem UnitaryRep.add_comp {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B C : UnitaryRep 𝕜 G} (f₁ f₂ : A ⟶ B) (g : B ⟶ C) : CategoryTheory.CategoryStruct.comp (f₁ + f₂) g = CategoryTheory.CategoryStruct.comp f₁ g + CategoryTheory.CategoryStruct.comp f₂ g

theorem UnitaryRep.comp_add {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B C : UnitaryRep 𝕜 G} (f : A ⟶ B) (g₁ g₂ : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (g₁ + g₂) = CategoryTheory.CategoryStruct.comp f g₁ + CategoryTheory.CategoryStruct.comp f g₂

@[implicit_reducible]

noncomputable instance UnitaryRep.instZeroHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Zero (A ⟶ B)

Equations

• UnitaryRep.instZeroHom = { zero := UnitaryRep.ofHom 0 }

@[simp]

theorem UnitaryRep.ofHom_zero {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} : ofHom 0 = 0

@[simp]

theorem UnitaryRep.zero_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Hom.hom 0 = 0

@[implicit_reducible]

noncomputable instance UnitaryRep.instSMulNatHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : SMul ℕ (A ⟶ B)

Equations

• UnitaryRep.instSMulNatHom = { smul := fun (n : ℕ) (f : A ⟶ B) => UnitaryRep.ofHom (n • UnitaryRep.Hom.hom f) }

theorem UnitaryRep.ofHom_nsmul {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) (n : ℕ) : ofHom (n • f) = n • ofHom f

theorem UnitaryRep.nsmul_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) (n : ℕ) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

noncomputable instance UnitaryRep.instNegHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Neg (A ⟶ B)

Equations

• UnitaryRep.instNegHom = { neg := fun (f : A ⟶ B) => UnitaryRep.ofHom (-UnitaryRep.Hom.hom f) }

theorem UnitaryRep.ofHom_neg {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) : ofHom (-f) = -ofHom f

theorem UnitaryRep.neg_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) : Hom.hom (-f) = -Hom.hom f

@[implicit_reducible]

noncomputable instance UnitaryRep.instSubHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : Sub (A ⟶ B)

Equations

• UnitaryRep.instSubHom = { sub := fun (f g : A ⟶ B) => UnitaryRep.ofHom (UnitaryRep.Hom.hom f - UnitaryRep.Hom.hom g) }

theorem UnitaryRep.ofHom_sub {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f g : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) : ofHom (f - g) = ofHom f - ofHom g

theorem UnitaryRep.sub_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f g : A ⟶ B) : Hom.hom (f - g) = Hom.hom f - Hom.hom g

@[implicit_reducible]

noncomputable instance UnitaryRep.instSMulIntHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : SMul ℤ (A ⟶ B)

Equations

• UnitaryRep.instSMulIntHom = { smul := fun (n : ℤ) (f : A ⟶ B) => UnitaryRep.ofHom (n • UnitaryRep.Hom.hom f) }

theorem UnitaryRep.ofHom_zsmul {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ρ.toRepresentation.IntertwiningMap σ.toRepresentation) (n : ℤ) : ofHom (n • f) = n • ofHom f

theorem UnitaryRep.zsmul_hom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : A ⟶ B) (n : ℤ) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

noncomputable instance UnitaryRep.instAddCommGroupHom {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} : AddCommGroup (A ⟶ B)

Equations

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

@[implicit_reducible]

noncomputable instance UnitaryRep.instPreadditive {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : CategoryTheory.Preadditive (UnitaryRep 𝕜 G)

Equations

• UnitaryRep.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

theorem UnitaryRep.sum_hom {ι : Type u_1} {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} (f : ι → (A ⟶ B)) (s : Finset ι) : Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)

theorem UnitaryRep.ofHom_sum {ι : Type u_1} {𝕜 : Type u_2} {G : Type u_3} {E F : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {ρ : UnitaryRepresentation 𝕜 G E} {σ : UnitaryRepresentation 𝕜 G F} (f : ι → σ.toRepresentation.IntertwiningMap ρ.toRepresentation) (s : Finset ι) : ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)

@[reducible, inline]

abbrev UnitaryRep.trivial (𝕜 : Type u_2) (G : Type u_3) (E : Type u) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : UnitaryRep 𝕜 G

The trivial 𝕜-linear G-representation on a 𝕜-module V.

Equations

• UnitaryRep.trivial 𝕜 G E = { E := E, normedAddCommGroup := inst✝², innerProductSpace := inst✝¹, completeSpace := inst✝, ρ := UnitaryRepresentation.trivial 𝕜 G E }

theorem UnitaryRep.trivial_ρ (𝕜 : Type u_2) (G : Type u_3) (E : Type u) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : (trivial 𝕜 G E).ρ = UnitaryRepresentation.trivial 𝕜 G E

theorem UnitaryRep.trivial_E (𝕜 : Type u_2) (G : Type u_3) (E : Type u) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : (trivial 𝕜 G E).E = E

@[simp]

theorem UnitaryRep.trivial_ρ_apply {𝕜 : Type u_2} {G : Type u_3} {E : Type u} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (g : G) (x : E) : ((trivial 𝕜 G E).ρ g) x = x

@[implicit_reducible]

instance UnitaryRep.instInhabited {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] : Inhabited (UnitaryRep 𝕜 G)

Equations

• UnitaryRep.instInhabited = { default := UnitaryRep.trivial 𝕜 G PUnit.{?u.1 + 1} }

theorem UnitaryRep.ρ_mul {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A : UnitaryRep 𝕜 G} (g1 g2 : G) : A.ρ (g1 * g2) = (A.ρ g2).trans (A.ρ g1)