theorem
norm_of_inner_preserving
{V₁ : Type u_1}
[NormedAddCommGroup V₁]
[InnerProductSpace ℂ V₁]
{V₂ : Type u_2}
[NormedAddCommGroup V₂]
[InnerProductSpace ℂ V₂]
(S₁ : Submodule ℂ V₁)
(S₂ : Submodule ℂ V₂)
(A : ↥S₁ ≃ₗ[ℂ] ↥S₂)
(h_inner : ∀ (x y : ↥S₁), inner ℂ (S₂.subtype (A x)) (S₂.subtype (A y)) = inner ℂ (S₁.subtype x) (S₁.subtype y))
(x : ↥S₁)
:
theorem
dixmier_schur_sesquilinear
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F₁ : Type u_2}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_3}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
:
∃ (c : ℂ),
∀ (x y : ↥(π₁.kFiniteSubspace K_sub)),
inner ℂ ((π₂.kFiniteSubspace K_sub).subtype (A x)) ((π₂.kFiniteSubspace K_sub).subtype (A y)) = c * inner ℂ ((π₁.kFiniteSubspace K_sub).subtype x) ((π₁.kFiniteSubspace K_sub).subtype y)
theorem
pullback_inner_product_proportional
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F₁ : Type u_2}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_3}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
:
∃ (c : ℝ),
0 < c ∧ ∀ (x y : ↥(π₁.kFiniteSubspace K_sub)),
inner ℂ ((π₂.kFiniteSubspace K_sub).subtype (A x)) ((π₂.kFiniteSubspace K_sub).subtype (A y)) = ↑c * inner ℂ ((π₁.kFiniteSubspace K_sub).subtype x) ((π₁.kFiniteSubspace K_sub).subtype y)
theorem
schur_inner_product_preservation
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F₁ : Type u_2}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_3}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
:
∃ (B : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub)),
(∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), B ⁅X, v⁆ = ⁅X, B v⁆) ∧ (∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
B (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (B v)) ∧ ∀ (x y : ↥(π₁.kFiniteSubspace K_sub)),
inner ℂ ((π₂.kFiniteSubspace K_sub).subtype (B x)) ((π₂.kFiniteSubspace K_sub).subtype (B y)) = inner ℂ ((π₁.kFiniteSubspace K_sub).subtype x) ((π₁.kFiniteSubspace K_sub).subtype y)
theorem
schur_norm_preservation
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F₁ : Type u_2}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_3}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
:
∃ (B : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub)),
(∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), B ⁅X, v⁆ = ⁅X, B v⁆) ∧ (∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
B (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (B v)) ∧ ∀ (x : ↥(π₁.kFiniteSubspace K_sub)),
‖(π₂.kFiniteSubspace K_sub).subtype (B x)‖ = ‖(π₁.kFiniteSubspace K_sub).subtype x‖
theorem
analytic_cross_space_intertwining
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
[LieGroup I ⊤ G]
[IsTopologicalGroup G]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_5}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[CompactSpace ↥K_sub]
(_hadm₁ : π₁.IsAdmissible K_sub)
(_hadm₂ : π₂.IsAdmissible K_sub)
(𝔤 : Type u_6)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(ι₁ : 𝔤 →ₗ⁅ℂ⁆ F₁ →ₗ[ℂ] F₁)
(ι₂ : 𝔤 →ₗ⁅ℂ⁆ F₂ →ₗ[ℂ] F₂)
(T : F₁ ≃ₗᵢ[ℂ] F₂)
(v : F₁)
(_hv : v ∈ π₁.kFiniteSubspace K_sub)
(_hTv : T v ∈ π₂.kFiniteSubspace K_sub)
(h : F₂ →L[ℂ] ℂ)
(hiter_eq : ∀ (Xs : List 𝔤), h (T (iterLieAction ι₁ Xs v)) = h (iterLieAction ι₂ Xs (T v)))
(g : G)
:
theorem
hc_equivariance_kfinite
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H' : Type u_2}
[TopologicalSpace H']
(I : ModelWithCorners ℝ E H')
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I ⊤ G]
[IsTopologicalGroup G]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_5}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(hadm₁ : π₁.IsAdmissible K_sub)
(hadm₂ : π₂.IsAdmissible K_sub)
(𝔤 : Type u_6)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(ι₁ : 𝔤 →ₗ⁅ℂ⁆ F₁ →ₗ[ℂ] F₁)
(ι₂ : 𝔤 →ₗ⁅ℂ⁆ F₂ →ₗ[ℂ] F₂)
(hι₁_compat :
∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)),
(ι₁ X) ((π₁.kFiniteSubspace K_sub).subtype v) = (π₁.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(hι₂_compat :
∀ (X : 𝔤) (v : ↥(π₂.kFiniteSubspace K_sub)),
(ι₂ X) ((π₂.kFiniteSubspace K_sub).subtype v) = (π₂.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
(h_dense₁ : DenseRange ⇑(π₁.kFiniteSubspace K_sub).subtype)
(h_dense₂ : DenseRange ⇑(π₂.kFiniteSubspace K_sub).subtype)
(h_norm :
∀ (x : ↥(π₁.kFiniteSubspace K_sub)),
‖(π₂.kFiniteSubspace K_sub).subtype (A x)‖ = ‖(π₁.kFiniteSubspace K_sub).subtype x‖)
(hι₁_stable : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v ∈ π₁.kFiniteSubspace K_sub)
(hι₂_stable : ∀ (X : 𝔤), ∀ v ∈ π₂.kFiniteSubspace K_sub, (ι₂ X) v ∈ π₂.kFiniteSubspace K_sub)
(g : G)
(x : ↥(π₁.kFiniteSubspace K_sub))
:
(A.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂ h_norm)
((π₁.toMonoidHom g) ((π₁.kFiniteSubspace K_sub).subtype x)) = (π₂.toMonoidHom g)
((A.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂ h_norm)
((π₁.kFiniteSubspace K_sub).subtype x))
theorem
proposition_7_1_schur_and_analytic
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H' : Type u_2}
[TopologicalSpace H']
(I : ModelWithCorners ℝ E H')
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I ⊤ G]
[IsTopologicalGroup G]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_5}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(hadm₁ : π₁.IsAdmissible K_sub)
(hadm₂ : π₂.IsAdmissible K_sub)
(𝔤 : Type u_6)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(ι₁ : 𝔤 →ₗ⁅ℂ⁆ F₁ →ₗ[ℂ] F₁)
(ι₂ : 𝔤 →ₗ⁅ℂ⁆ F₂ →ₗ[ℂ] F₂)
(hι₁_compat :
∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)),
(ι₁ X) ((π₁.kFiniteSubspace K_sub).subtype v) = (π₁.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(hι₂_compat :
∀ (X : 𝔤) (v : ↥(π₂.kFiniteSubspace K_sub)),
(ι₂ X) ((π₂.kFiniteSubspace K_sub).subtype v) = (π₂.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
(h_dense₁ : DenseRange ⇑(π₁.kFiniteSubspace K_sub).subtype)
(h_dense₂ : DenseRange ⇑(π₂.kFiniteSubspace K_sub).subtype)
(hι₁_stable : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v ∈ π₁.kFiniteSubspace K_sub)
(hι₂_stable : ∀ (X : 𝔤), ∀ v ∈ π₂.kFiniteSubspace K_sub, (ι₂ X) v ∈ π₂.kFiniteSubspace K_sub)
:
∃ (B : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub)) (_ :
∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), B ⁅X, v⁆ = ⁅X, B v⁆) (_ :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
B (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (B v))
(h_norm :
∀ (x : ↥(π₁.kFiniteSubspace K_sub)),
‖(π₂.kFiniteSubspace K_sub).subtype (B x)‖ = ‖(π₁.kFiniteSubspace K_sub).subtype x‖),
∀ (g : G) (x : ↥(π₁.kFiniteSubspace K_sub)),
(B.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂ h_norm)
((π₁.toMonoidHom g) ((π₁.kFiniteSubspace K_sub).subtype x)) = (π₂.toMonoidHom g)
((B.extendOfIsometry (π₁.kFiniteSubspace K_sub).subtype (π₂.kFiniteSubspace K_sub).subtype h_dense₁ h_dense₂
h_norm)
((π₁.kFiniteSubspace K_sub).subtype x))
theorem
equivariance_extends_from_dense
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{F₁ : Type u_2}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_3}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(T : F₁ ≃ₗᵢ[ℂ] F₂)
{S : Type u_4}
[TopologicalSpace S]
(ι : S → F₁)
(h_dense : DenseRange ι)
(h_agree : ∀ (g : G) (s : S), T ((π₁.toMonoidHom g) (ι s)) = (π₂.toMonoidHom g) (T (ι s)))
(g : G)
(v : F₁)
:
theorem
proposition_7_1
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H' : Type u_2}
[TopologicalSpace H']
(I : ModelWithCorners ℝ E H')
{G : Type u_3}
[Group G]
[TopologicalSpace G]
[ChartedSpace H' G]
[LieGroup I ⊤ G]
[IsTopologicalGroup G]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[InnerProductSpace ℂ F₁]
[CompleteSpace F₁]
{F₂ : Type u_5}
[NormedAddCommGroup F₂]
[InnerProductSpace ℂ F₂]
[CompleteSpace F₂]
(π₁ : ContinuousRep G F₁)
(π₂ : ContinuousRep G F₂)
(K_sub : Subgroup G)
[hK_compact : CompactSpace ↥K_sub]
(hunit₁ : π₁.IsUnitary)
(hunit₂ : π₂.IsUnitary)
(hadm₁ : π₁.IsAdmissible K_sub)
(hadm₂ : π₂.IsAdmissible K_sub)
(𝔤 : Type u_6)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₁.kFiniteSubspace K_sub)]
[LieRingModule 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π₂.kFiniteSubspace K_sub)]
(ι₁ : 𝔤 →ₗ⁅ℂ⁆ F₁ →ₗ[ℂ] F₁)
(ι₂ : 𝔤 →ₗ⁅ℂ⁆ F₂ →ₗ[ℂ] F₂)
(hι₁_compat :
∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)),
(ι₁ X) ((π₁.kFiniteSubspace K_sub).subtype v) = (π₁.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(hι₂_compat :
∀ (X : 𝔤) (v : ↥(π₂.kFiniteSubspace K_sub)),
(ι₂ X) ((π₂.kFiniteSubspace K_sub).subtype v) = (π₂.kFiniteSubspace K_sub).subtype ⁅X, v⁆)
(A : ↥(π₁.kFiniteSubspace K_sub) ≃ₗ[ℂ] ↥(π₂.kFiniteSubspace K_sub))
(hA_lie : ∀ (X : 𝔤) (v : ↥(π₁.kFiniteSubspace K_sub)), A ⁅X, v⁆ = ⁅X, A v⁆)
(hA_K :
∀ (k : ↥K_sub) (v : ↥(π₁.kFiniteSubspace K_sub)),
A (((kFiniteSubspace_kAction π₁ K_sub) k) v) = ((kFiniteSubspace_kAction π₂ K_sub) k) (A v))
(hι₁_stable : ∀ (X : 𝔤), ∀ v ∈ π₁.kFiniteSubspace K_sub, (ι₁ X) v ∈ π₁.kFiniteSubspace K_sub)
(hι₂_stable : ∀ (X : 𝔤), ∀ v ∈ π₂.kFiniteSubspace K_sub, (ι₂ X) v ∈ π₂.kFiniteSubspace K_sub)
:
Nonempty (UnitaryRepEquiv π₁ π₂)