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_2 u_3) (w + 1))

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

• of :: (
• E : Type w

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

• normedAddCommGroup : NormedAddCommGroup ↑self
• normedSpace : InnerProductSpace 𝕜 ↑self
• finiteDimensional : FiniteDimensional 𝕜 ↑self
• ρ : Representation 𝕜 G ↑self

  The underlying unitary representation of an object in UnitaryRep 𝕜 G

• isUnitary_ρ : self.ρ.IsUnitary
• )

@[implicit_reducible]

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

Equations

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

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

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

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

  The underlying G-equivariant linear map.

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

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'

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

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.ρ.IntertwiningMap B.ρ

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) : { E := E, normedAddCommGroup := inst✝, normedSpace := inst✝¹, finiteDimensional := inst✝², ρ := ρ, isUnitary_ρ := hρ } ⟶ { E := F, normedAddCommGroup := inst✝³, normedSpace := inst✝⁴, finiteDimensional := inst✝⁵, ρ := σ, isUnitary_ρ := hσ }

Typecheck an IntertwiningMap as a morphism in UnitaryRep.

Equations

• UnitaryRep.ofHom hρ hσ 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.ρ.IntertwiningMap B.ρ

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) = Representation.IntertwiningMap.id A.ρ

theorem UnitaryRep.id_apply {𝕜 : Type u_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A : UnitaryRep 𝕜 G} (a : ↑A) : (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) : (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) : (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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) : Hom.hom (ofHom hρ hσ 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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} (hρ : ρ.IsUnitary) : ofHom hρ hρ (Representation.IntertwiningMap.id ρ) = CategoryTheory.CategoryStruct.id { E := E, normedAddCommGroup := inst✝, normedSpace := inst✝¹, finiteDimensional := inst✝², ρ := ρ, isUnitary_ρ := hρ }

@[simp]

theorem UnitaryRep.ofHom_comp {𝕜 : Type u_2} {G : Type u_3} {E F H : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] {τ : Representation 𝕜 G H} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (hτ : τ.IsUnitary) (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ) : ofHom hρ hτ (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom hρ hσ f) (ofHom hσ hτ g)

theorem UnitaryRep.ofHom_apply {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) (x : E) : (CategoryTheory.ConcreteCategory.hom (ofHom hρ hσ 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) : (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) : (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

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

def UnitaryRep.mkIso {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) : { E := E, normedAddCommGroup := inst✝, normedSpace := inst✝¹, finiteDimensional := inst✝², ρ := ρ, isUnitary_ρ := hρ } ≅ { E := F, normedAddCommGroup := inst✝³, normedSpace := inst✝⁴, finiteDimensional := inst✝⁵, ρ := σ, isUnitary_ρ := hσ }

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

Equations

• UnitaryRep.mkIso hρ hσ e = { hom := UnitaryRep.ofHom hρ hσ ↑e, inv := UnitaryRep.ofHom hσ hρ ↑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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) (x : E) : (Hom.hom (mkIso hρ hσ e).hom) x = (↑e).toLinearMap x

@[simp]

theorem UnitaryRep.mkIso_hom_hom_toLinearMap {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) : (Hom.hom (mkIso hρ hσ e).hom).toLinearMap = (↑e).toLinearMap

@[simp]

theorem UnitaryRep.mkIso_inv_hom_toLinearMap {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) : (Hom.hom (mkIso hρ hσ e).inv).toLinearMap = (↑e.symm).toLinearMap

@[simp]

theorem UnitaryRep.mkIso_inv_hom_apply {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) (y : F) : (Hom.hom (mkIso hρ hσ e).inv) y = e.symm y

@[simp]

theorem UnitaryRep.mkIso_hom_hom {𝕜 : Type u_2} {G : Type u_3} {E F : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (e : ρ.Equiv σ) : Hom.hom (mkIso hρ hσ e).hom = ↑e

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

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) : (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) : (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.ρ.IntertwiningMap B.ρ

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.ρ.IntertwiningMap B.ρ) : 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f g : ρ.IntertwiningMap σ) : ofHom hρ hσ (f + g) = ofHom hρ hσ f + ofHom hρ hσ 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) : ofHom hρ hσ 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) (n : ℕ) : ofHom hρ hσ (n • f) = n • ofHom hρ hσ 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) : ofHom hρ hσ (-f) = -ofHom hρ hσ 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f g : ρ.IntertwiningMap σ) : ofHom hρ hσ (f - g) = ofHom hρ hσ f - ofHom hρ hσ 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]

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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : ρ.IsUnitary) (hσ : σ.IsUnitary) (f : ρ.IntertwiningMap σ) (n : ℤ) : ofHom hρ hσ (n • f) = n • ofHom hρ hσ 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]

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]

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_2} {G : Type u_3} [RCLike 𝕜] [Group G] {A B : UnitaryRep 𝕜 G} {ι : Type u'} (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 w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ρ : Representation 𝕜 G E} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {σ : Representation 𝕜 G F} (hρ : σ.IsUnitary) (hσ : ρ.IsUnitary) (f : ι → σ.IntertwiningMap ρ) (s : Finset ι) : ofHom hρ hσ (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom hρ hσ (f i)

@[reducible, inline]

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

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

Equations

• UnitaryRep.trivial 𝕜 G E = { E := E, normedAddCommGroup := inst✝², normedSpace := inst✝¹, finiteDimensional := inst✝, ρ := Representation.trivial 𝕜 G E, isUnitary_ρ := ⋯ }

theorem UnitaryRep.trivial_ρ (𝕜 : Type u_2) (G : Type u_3) (E : Type w) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : (trivial 𝕜 G E).ρ = Representation.trivial 𝕜 G E

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

@[simp]

theorem UnitaryRep.trivial_ρ_apply {𝕜 : Type u_2} {G : Type u_3} {E : Type w} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 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.21 + 1} }

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