theorem
gkmodule_has_countable_spanning_set
{𝔤 : 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)
(hirr : M.IsIrreducibleGKModule)
[FiniteDimensional ℂ 𝔤]
:
∃ (s : Set V), Submodule.span ℂ s = ⊤ ∧ Cardinal.mk ↑s ≤ Cardinal.aleph0
theorem
dixmier_countable_dim_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]
(M : GKModule 𝔤 K 𝔨 Ad V)
(hirr : M.IsIrreducibleGKModule)
[FiniteDimensional ℂ 𝔤]
:
theorem
schur_gkmodule_zero_or_bijective
{𝔤 : 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)
(hirr : M.IsIrreducibleGKModule)
(φ : GKModuleHom M M)
:
def
gkmoduleSubScalar
{𝔤 : 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)
(φ : GKModuleHom M M)
(c : ℂ)
:
GKModuleHom M M
Instances For
theorem
no_inv_fd_subspace_of_all_bij
{V : Type u_1}
[AddCommGroup V]
[Module ℂ V]
(φ : V →ₗ[ℂ] V)
(hbij : ∀ (c : ℂ), Function.Bijective ⇑(φ - c • LinearMap.id))
(W : Submodule ℂ V)
(hW : W ≠ ⊥)
(hfin : FiniteDimensional ℂ ↥W)
(hinv : ∀ w ∈ W, φ w ∈ W)
:
theorem
resolvent_vectors_linearIndependent
{V : Type u_1}
[AddCommGroup V]
[Module ℂ V]
[Nontrivial V]
(φ : V →ₗ[ℂ] V)
(hbij : ∀ (c : ℂ), Function.Bijective ⇑(φ - c • LinearMap.id))
(v : V)
(hv : v ≠ 0)
:
LinearIndependent ℂ fun (c : ℂ) => (LinearEquiv.ofBijective (φ - c • LinearMap.id) ⋯).symm v
theorem
gkmodule_endo_has_eigenvalue
{𝔤 : 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]
[Nontrivial V]
[FiniteDimensional ℂ 𝔤]
(M : GKModule 𝔤 K 𝔨 Ad V)
(hirr : M.IsIrreducibleGKModule)
(φ : GKModuleHom M M)
:
∃ (c : ℂ), ¬Function.Injective ⇑(gkmoduleSubScalar M φ c).toLinearMap
theorem
schur_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]
[Nontrivial V]
[FiniteDimensional ℂ 𝔤]
(M : GKModule 𝔤 K 𝔨 Ad V)
(hirr : M.IsIrreducibleGKModule)
(φ : GKModuleHom M M)
:
∃ (c : ℂ), ∀ (v : V), φ.toLinearMap v = c • v
noncomputable def
ueaAction
(𝔤 : Type u_1)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(V : Type u_2)
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
:
Instances For
theorem
ueaAction_ι
{𝔤 : Type u_1}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{V : Type u_2}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
(X : 𝔤)
:
theorem
center_ueaAction_lie_comm
{𝔤 : Type u_1}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{V : Type u_2}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
(z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)))
(X : 𝔤)
(v : V)
:
theorem
infinitesimal_character_exists
{𝔤 : 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]
[Nontrivial V]
[FiniteDimensional ℂ 𝔤]
(M : GKModule 𝔤 K 𝔨 Ad V)
(hirr : M.IsIrreducibleGKModule)
(hK_center :
∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (k : K) (v : V),
((ueaAction 𝔤 V) ↑z) ((M.σ k) v) = (M.σ k) (((ueaAction 𝔤 V) ↑z) v))
:
∃ (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ),
∀ (z : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤))) (v : V), ((ueaAction 𝔤 V) ↑z) v = χ z • v
theorem
intertwiner_additive_on_kfinite
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(_hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_add : ∀ (x y : G₁.Ŵ), T (x + y) = T x + T y)
(v w : V₁)
:
theorem
intertwiner_smul_on_kfinite
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(_hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_smul : ∀ (c : ℂ) (x : G₁.Ŵ), T (c • x) = c • T x)
(c : ℂ)
(v : V₁)
:
theorem
intertwiner_preserves_kfinite
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_add : ∀ (x y : G₁.Ŵ), T (x + y) = T x + T y)
(hT_smul : ∀ (c : ℂ) (x : G₁.Ŵ), T (c • x) = c • T x)
(v : V₁)
:
theorem
intertwiner_restriction_linear
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_add : ∀ (x y : G₁.Ŵ), T (x + y) = T x + T y)
(hT_smul : ∀ (c : ℂ) (x : G₁.Ŵ), T (c • x) = c • T x)
(φ_fun : V₁ → V₂)
(hφ_fun : ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ_fun v))
:
theorem
intertwiner_restriction_lie_comm
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(_hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_lie : ∀ (X : 𝔤) (w : G₁.Ŵ), T (G₁.lie_action_Ŵ X w) = G₂.lie_action_Ŵ X (T w))
(φ_lin : V₁ →ₗ[ℂ] V₂)
(hφ : ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ_lin v))
(X : 𝔤)
(v : V₁)
:
theorem
Globalization.lie_action_Ŵ_continuous
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(G_glob : Globalization G K_sub M)
(X : 𝔤)
:
Continuous (G_glob.lie_action_Ŵ X)
theorem
Globalization.ι_range_dense
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(G_glob : Globalization G K_sub M)
:
theorem
G_intertwiner_continuous
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
:
theorem
lie_intertwining_on_kfinite
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(X : 𝔤)
(v : V₁)
:
theorem
lie_action_naturality_axiom
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(X : 𝔤)
(w : G₁.Ŵ)
:
theorem
intertwiner_lie_intertwining
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(X : 𝔤)
(w : G₁.Ŵ)
:
theorem
globalization_hom_restriction
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
(hT : ∀ (g : G) (w : G₁.Ŵ), T ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T w))
(hT_add : ∀ (x y : G₁.Ŵ), T (x + y) = T x + T y)
(hT_smul : ∀ (c : ℂ) (x : G₁.Ŵ), T (c • x) = c • T x)
:
∃ (φ : GKModuleHom M₁ M₂), ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ.toLinearMap v)
theorem
globalization_hom_extension_unique
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
[CompactSpace ↥K_sub.range]
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T₁ T₂ : G₁.Ŵ → G₂.Ŵ)
(_hT₁ : ∀ (g : G) (w : G₁.Ŵ), T₁ ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T₁ w))
(_hT₂ : ∀ (g : G) (w : G₁.Ŵ), T₂ ((G₁.π.toMonoidHom g) w) = (G₂.π.toMonoidHom g) (T₂ w))
(hcT₁ : Continuous T₁)
(hcT₂ : Continuous T₂)
(heq_on_kfin : ∀ (v : V₁), T₁ (G₁.ι v) = T₂ (G₁.ι v))
:
@[reducible]
def
Globalization.topologicalSpaceŴ
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(Gl : Globalization G K_sub M)
:
Instances For
@[reducible]
def
Globalization.addCommGroupŴ
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(Gl : Globalization G K_sub M)
:
AddCommGroup Gl.Ŵ
Instances For
@[reducible]
def
Globalization.moduleŴ
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(Gl : Globalization G K_sub M)
:
Instances For
@[reducible]
def
Globalization.πApp
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V : Type u_4}
[AddCommGroup V]
[Module ℂ V]
[LieRingModule 𝔤 V]
[LieModule ℂ 𝔤 V]
{M : GKModule 𝔤 K 𝔨 Ad V}
(Gl : Globalization G K_sub M)
(g : G)
(w : Gl.Ŵ)
:
Gl.Ŵ
Instances For
def
IsGIntertwiner
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
{M₁ : GKModule 𝔤 K 𝔨 Ad V₁}
{M₂ : GKModule 𝔤 K 𝔨 Ad V₂}
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
:
Instances For
def
IsGlobAdditive
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
{M₁ : GKModule 𝔤 K 𝔨 Ad V₁}
{M₂ : GKModule 𝔤 K 𝔨 Ad V₂}
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
:
Instances For
def
IsGlobLinear
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{K : Type u_2}
[Group K]
{K_sub : K →* G}
{𝔤 : Type u_3}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_4}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_5}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
{M₁ : GKModule 𝔤 K 𝔨 Ad V₁}
{M₂ : GKModule 𝔤 K 𝔨 Ad V₂}
(G₁ : Globalization G K_sub M₁)
(G₂ : Globalization G K_sub M₂)
(T : G₁.Ŵ → G₂.Ŵ)
:
Instances For
theorem
globalization_equivalence_fully_faithful
(SG : SemisimpleLieGroup)
{K : Type u_1}
[Group K]
{K_sub : K →* SG.G}
[CompactSpace ↥K_sub.range]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{V₁ : Type u_3}
[AddCommGroup V₁]
[Module ℂ V₁]
[LieRingModule 𝔤 V₁]
[LieModule ℂ 𝔤 V₁]
{V₂ : Type u_4}
[AddCommGroup V₂]
[Module ℂ V₂]
[LieRingModule 𝔤 V₂]
[LieModule ℂ 𝔤 V₂]
(M₁ : GKModule 𝔤 K 𝔨 Ad V₁)
(M₂ : GKModule 𝔤 K 𝔨 Ad V₂)
(hfl₁ : M₁.IsFiniteLength)
(hunit₁ : M₁.IsUnitary)
(hfl₂ : M₂.IsFiniteLength)
(hunit₂ : M₂.IsUnitary)
(G₁ : Globalization SG.G K_sub M₁)
(G₂ : Globalization SG.G K_sub M₂)
:
(∀ (φ : GKModuleHom M₁ M₂),
∃! T : G₁.Ŵ → G₂.Ŵ, Continuous T ∧ IsGIntertwiner G₁ G₂ T ∧ ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ.toLinearMap v)) ∧ ∀ (T : G₁.Ŵ → G₂.Ŵ),
IsGIntertwiner G₁ G₂ T →
IsGlobAdditive G₁ G₂ T →
IsGlobLinear G₁ G₂ T → ∃ (φ : GKModuleHom M₁ M₂), ∀ (v : V₁), T (G₁.ι v) = G₂.ι (φ.toLinearMap v)