def Representation.IsLocallyFinite {K : Type u_1} {V : Type u_2} [Group K] [AddCommGroup V] [Module ℂ V] (σ : Representation ℂ K V) : Prop

structure GKModule (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (K : Type u_2) [Group K] (𝔨 : LieSubalgebra ℂ 𝔤) (Ad : K →* 𝔤 →ₗ[ℂ] 𝔤) (V : Type u_3) [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] : Type (max (max u_1 u_2) u_3)

• σ : Representation ℂ K V
• locallyFinite : self.σ.IsLocallyFinite
• diffσ : ↥𝔨 →ₗ[ℂ] V →ₗ[ℂ] V
• diff_eq_lie (X : ↥𝔨) (v : V) : (self.diffσ X) v = ⁅↑X, v⁆
• equivariance (k : K) (X : 𝔤) (v : V) : (self.σ k) ⁅X, v⁆ = ⁅(Ad k) X, (self.σ k) v⁆

structure GKModuleHom {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] {W : Type u_4} [AddCommGroup W] [Module ℂ W] [LieRingModule 𝔤 W] [LieModule ℂ 𝔤 W] (M : GKModule 𝔤 K 𝔨 Ad V) (N : GKModule 𝔤 K 𝔨 Ad W) : Type (max u_3 u_4)

• toLinearMap : V →ₗ[ℂ] W
• lie_comm (X : 𝔤) (v : V) : self.toLinearMap ⁅X, v⁆ = ⁅X, self.toLinearMap v⁆
• group_comm (k : K) (v : V) : self.toLinearMap ((M.σ k) v) = (N.σ k) (self.toLinearMap v)

structure GKModule.IsSubmodule {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (W : Submodule ℂ V) : Prop

• lie_invariant (X : 𝔤) (w : V) : w ∈ W → ⁅X, w⁆ ∈ W
• group_invariant (k : K) (w : V) : w ∈ W → (M.σ k) w ∈ W

def GKModule.IsIrreducibleGKModule {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) : Prop

def GKModule.IsKInvariant {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (W : Submodule ℂ V) : Prop

def GKModule.IsKIrreducible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (W : Submodule ℂ V) : Prop

def GKModule.AreKIsomorphic {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (W₁ W₂ : Submodule ℂ V) (h₁ : M.IsKInvariant W₁) (h₂ : M.IsKInvariant W₂) : Prop

def GKModule.KIsotypicComponent {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) (W₀ : Submodule ℂ V) (hW₀ : M.IsKIrreducible W₀) : Submodule ℂ V

def GKModule.IsAdmissible {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : GKModule 𝔤 K 𝔨 Ad V) : Prop