def
ContinuousRep.IsWeaklyAnalytic
{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]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(v : F)
:
Instances For
def
EllipticOperator.IsEllipticAt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(symbolAt : E → ℝ)
:
Instances For
def
EllipticOperator.IsElliptic
{X : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(σ : X → E → ℝ)
:
Instances For
theorem
lie_iter_vanish_implies_re_vanishes_near_identity_axiom
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(w : ↥(π.kFiniteSubspace K_sub))
(v : F)
(hv : v = (π.kFiniteSubspace K_sub).subtype w)
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π v)
(h : F →L[ℂ] ℂ)
(hh_lie_iter_vanish :
∀ (Xs : List 𝔤),
h
((π.kFiniteSubspace K_sub).subtype
(List.foldr (fun (X : 𝔤) (acc : ↥(π.kFiniteSubspace K_sub)) => ⁅X, acc⁆) w Xs)) = 0)
:
theorem
lie_iter_vanish_implies_re_vanishes_near_identity
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(w : ↥(π.kFiniteSubspace K_sub))
(v : F)
(hv : v = (π.kFiniteSubspace K_sub).subtype w)
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π v)
(h : F →L[ℂ] ℂ)
(hh_lie_iter_vanish :
∀ (Xs : List 𝔤),
h
((π.kFiniteSubspace K_sub).subtype
(List.foldr (fun (X : 𝔤) (acc : ↥(π.kFiniteSubspace K_sub)) => ⁅X, acc⁆) w Xs)) = 0)
:
theorem
analytic_matcoeff_re_vanishes_globally_of_locally_axiom
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(v : F)
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π v)
(h : F →L[ℂ] ℂ)
(U : Set G)
(hU_open : IsOpen U)
(hU_mem : 1 ∈ U)
(hU_vanish : ∀ g ∈ U, (h ((π.toMonoidHom g) v)).re = 0)
(g : G)
:
theorem
analytic_matcoeff_re_vanishes_globally_of_locally
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(v : F)
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π v)
(h : F →L[ℂ] ℂ)
(U : Set G)
(hU_open : IsOpen U)
(hU_mem : 1 ∈ U)
(hU_vanish : ∀ g ∈ U, (h ((π.toMonoidHom g) v)).re = 0)
(g : G)
:
theorem
matrix_coeff_re_vanishes_of_lie_iter_vanish
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(w : ↥(π.kFiniteSubspace K_sub))
(v : F)
(hv : v = (π.kFiniteSubspace K_sub).subtype w)
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π v)
(h : F →L[ℂ] ℂ)
(hh_lie_iter_vanish :
∀ (Xs : List 𝔤),
h
((π.kFiniteSubspace K_sub).subtype
(List.foldr (fun (X : 𝔤) (acc : ↥(π.kFiniteSubspace K_sub)) => ⁅X, acc⁆) w Xs)) = 0)
(g : G)
:
theorem
analytic_continuation_connected_lie_group
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(w : ↥(π.kFiniteSubspace K_sub))
(hv_analytic : ContinuousRep.IsWeaklyAnalyticVector I π ((π.kFiniteSubspace K_sub).subtype w))
(h : F →L[ℂ] ℂ)
(hh_lie_iter_vanish :
∀ (Xs : List 𝔤),
h
((π.kFiniteSubspace K_sub).subtype
(List.foldr (fun (X : 𝔤) (acc : ↥(π.kFiniteSubspace K_sub)) => ⁅X, acc⁆) w Xs)) = 0)
(g : G)
:
theorem
analytic_continuation_from_gInvariance
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ 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]
[SecondCountableTopology G]
{F : Type uFw}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[CompleteSpace F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(hK_max : IsMaximalCompactSubgroup K_sub)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W)
(w : ↥(π.kFiniteSubspace K_sub))
(hw : w ∈ W)
(h : F →L[ℂ] ℂ)
(hh_vanish : ∀ v ∈ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W), h v = 0)
(g : G)
:
theorem
gkSubmodule_closure_isInvariant_analyticity_step
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ 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]
[SecondCountableTopology G]
{F : Type uFw}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[CompleteSpace F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(hK_max : IsMaximalCompactSubgroup K_sub)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W)
(g : G)
:
⇑(π.toMonoidHom g) '' (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W) ⊆ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W)
theorem
gkSubmodule_closure_isInvariant
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ 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]
[SecondCountableTopology G]
{F : Type uFw}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[CompleteSpace F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
(hG_ss : ContinuousRep.IsSemisimpleLieGroup I G)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(hK_max : IsMaximalCompactSubgroup K_sub)
(𝔤 : Type u_4)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W)
(g : G)
(v : F)
:
v ∈ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W) →
(π.toMonoidHom g) v ∈ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W)
theorem
subrep_orbit_image
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(U : Submodule ℂ F)
(hU : π.IsInvariantSubspace U)
(v : ↥U)
:
(⇑U.subtype '' Set.range fun (k : ↥K_sub) => ((π.subrepresentation U hU).toMonoidHom ↑k) v) = Set.range fun (k : ↥K_sub) => (π.toMonoidHom ↑k) ↑v
theorem
kFinite_subrep_to_full
{G : Type u_1}
[Group G]
[TopologicalSpace G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(U : Submodule ℂ F)
(hU : π.IsInvariantSubspace U)
(v : ↥U)
(hv : v ∈ (π.subrepresentation U hU).kFiniteSubspace K_sub)
:
theorem
subrep_kFinite_image_subset
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(U : Submodule ℂ F)
(hU : π.IsInvariantSubspace U)
:
⇑U.subtype '' ↑((π.subrepresentation U hU).kFiniteSubspace K_sub) ⊆ ⇑(π.kFiniteSubspace K_sub).subtype '' ↑(Submodule.comap (π.kFiniteSubspace K_sub).subtype U)
theorem
kFinite_dense_in_invariant_subspace
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(_hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(U : Submodule ℂ F)
(hU : π.IsInvariantSubspace U)
:
closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑(Submodule.comap (π.kFiniteSubspace K_sub).subtype U)) = ↑U
theorem
isotypic_projector_preserves_K_invariant_image
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(P : F →L[ℂ] F)
(_hP_kfin : ∀ (w : F), P w ∈ π.kFiniteSubspace K_sub)
(_hP_comm : ∀ (k : ↥K_sub), P.comp (π.toMonoidHom ↑k) = (π.toMonoidHom ↑k).comp P)
(hP_preserves :
∀ (S : Submodule ℂ F),
(∀ (k : ↥K_sub), ∀ s ∈ S, (π.toMonoidHom ↑k) s ∈ S) → ∀ s ∈ S, s ∈ π.kFiniteSubspace K_sub → P s ∈ S)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW_inv : ∀ (k : ↥K_sub), ∀ w ∈ W, ((kFiniteSubspace_kAction π K_sub) k) w ∈ W)
(w : F)
:
w ∈ ⇑(π.kFiniteSubspace K_sub).subtype '' ↑W → P w ∈ ⇑(π.kFiniteSubspace K_sub).subtype '' ↑W
theorem
isotypic_projector_image_closed
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(P : F →L[ℂ] F)
(hP_fin : FiniteDimensional ℂ ↥(↑P).range)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
:
IsClosed (⇑P '' (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W))
theorem
kFinite_isotypic_decomposition_with_invariance
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W)
(v : ↥(π.kFiniteSubspace K_sub))
:
∃ (n : ℕ) (Ps : Fin n → F →L[ℂ] F),
(∀ (i : Fin n) (w : F), (Ps i) w ∈ π.kFiniteSubspace K_sub) ∧ ↑v = ∑ i : Fin n, (Ps i) ↑v ∧ (∀ (i : Fin n),
∀ w ∈ ⇑(π.kFiniteSubspace K_sub).subtype '' ↑W, (Ps i) w ∈ ⇑(π.kFiniteSubspace K_sub).subtype '' ↑W) ∧ ∀ (i : Fin n), IsClosed (⇑(Ps i) '' (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W))
theorem
closure_gkSubmodule_kfinite_subset
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(W : Submodule ℂ ↥(π.kFiniteSubspace K_sub))
(hW : (harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W)
(v : ↥(π.kFiniteSubspace K_sub))
(hv : ↑v ∈ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W))
:
theorem
subrep_gkSubmodule_bijection
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
:
(∀ (U : Submodule ℂ F),
π.IsInvariantSubspace U →
closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑(Submodule.comap (π.kFiniteSubspace K_sub).subtype U)) = ↑U) ∧ (∀ (W : Submodule ℂ ↥(π.kFiniteSubspace K_sub)),
(harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsSubmodule W →
∀ (v : ↥(π.kFiniteSubspace K_sub)), v ∈ W ↔ ↑v ∈ closure (⇑(π.kFiniteSubspace K_sub).subtype '' ↑W)) ∧ ∀ (U₁ U₂ : Submodule ℂ F),
π.IsInvariantSubspace U₁ →
π.IsInvariantSubspace U₂ →
Submodule.comap (π.kFiniteSubspace K_sub).subtype U₁ = Submodule.comap (π.kFiniteSubspace K_sub).subtype U₂ →
U₁ = U₂
def
ContinuousRep.IsFiniteLength
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℂ V]
(π : ContinuousRep G V)
:
Instances For
theorem
kFiniteSubspace_finiteLength_of_rep_finiteLength
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(hfl : π.IsFiniteLength)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(hι_compat :
∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)),
(π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w))
(_hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U)
:
(harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsFiniteLength
theorem
GKModule.finiteLength_finitelyGenerated
{𝔤 : 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)
(hfl : M.IsFiniteLength)
:
∃ (S : Finset V), ∀ (v : V), v ∈ Submodule.span ℂ (⋃ s ∈ S, ⋃ (Xs : List 𝔤), {lieIterate Xs s})
theorem
finiteLength_implies_harishChandraModule
{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]
[NormedSpace ℂ F]
(π : ContinuousRep G F)
(K_sub : Subgroup G)
(hadm : π.IsAdmissible K_sub)
[CompactSpace ↥K_sub]
[T2Space ↥K_sub]
(hfl : π.IsFiniteLength)
(𝔤 : Type u_5)
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
(𝔨 : LieSubalgebra ℂ 𝔤)
(Ad : ↥K_sub →* 𝔤 →ₗ[ℂ] 𝔤)
(ι : 𝔤 →ₗ⁅ℂ⁆ F →ₗ[ℂ] F)
[LieRingModule 𝔤 ↥(π.kFiniteSubspace K_sub)]
[LieModule ℂ 𝔤 ↥(π.kFiniteSubspace K_sub)]
(hequiv :
∀ (k : ↥K_sub) (X : 𝔤) (v : ↥(π.kFiniteSubspace K_sub)),
((kFiniteSubspace_kAction π K_sub) k) ⁅X, v⁆ = ⁅(Ad k) X, ((kFiniteSubspace_kAction π K_sub) k) v⁆)
(hι_compat :
∀ (X : 𝔤) (w : ↥(π.kFiniteSubspace K_sub)),
(π.kFiniteSubspace K_sub).subtype ⁅X, w⁆ = (ι X) ((π.kFiniteSubspace K_sub).subtype w))
(hι_preserves : ∀ (U : Submodule ℂ F), π.IsInvariantSubspace U → ∀ (X : 𝔤), ∀ v ∈ U, (ι X) v ∈ U)
:
(harishChandraGKModule I π K_sub hadm 𝔤 𝔨 Ad ι hequiv).IsHarishChandraModule