structure
PrincipalSeriesBridge
{𝔤 : Type u_1}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{K : Type u_2}
[Group K]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
(ν : ℂ)
(ε : ZMod 2)
(R : (SL2IrredGKModule.principalSeries ν ε).Realization 𝔤 K 𝔨 Ad)
:
Type u_3
- compat_H (w : R.W) : self.toModel ⁅sl2_canonical_H 𝔤, w⁆ = (principalSeries_ρH ν ε) (self.toModel w)
- compat_E (w : R.W) : self.toModel ⁅sl2_canonical_E 𝔤, w⁆ = (principalSeries_ρE ν ε) (self.toModel w)
- compat_F (w : R.W) : self.toModel ⁅sl2_canonical_F 𝔤, w⁆ = (principalSeries_ρF ν ε) (self.toModel w)
Instances For
noncomputable def
PrincipalSeriesBridge.neg_intertwining_linearMap
{𝔤 : Type u_1}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{K : Type u_2}
[Group K]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{s : ℂ}
{ε : ZMod 2}
{R₁ : (SL2IrredGKModule.principalSeries s ε).Realization 𝔤 K 𝔨 Ad}
{R₂ : (SL2IrredGKModule.principalSeries (-s) ε).Realization 𝔤 K 𝔨 Ad}
(b₁ : PrincipalSeriesBridge s ε R₁)
(b₂ : PrincipalSeriesBridge (-s) ε R₂)
(c : ℤ → ℂ)
:
Instances For
theorem
PrincipalSeriesBridge.neg_intertwining_bijective
{𝔤 : Type u_1}
[LieRing 𝔤]
[LieAlgebra ℂ 𝔤]
{K : Type u_2}
[Group K]
{𝔨 : LieSubalgebra ℂ 𝔤}
{Ad : K →* 𝔤 →ₗ[ℂ] 𝔤}
{s : ℂ}
{ε : ZMod 2}
{R₁ : (SL2IrredGKModule.principalSeries s ε).Realization 𝔤 K 𝔨 Ad}
{R₂ : (SL2IrredGKModule.principalSeries (-s) ε).Realization 𝔤 K 𝔨 Ad}
(b₁ : PrincipalSeriesBridge s ε R₁)
(b₂ : PrincipalSeriesBridge (-s) ε R₂)
(c : ℤ → ℂ)
(hc : ∀ (m : ℤ), c m ≠ 0)
:
Function.Bijective ⇑(b₁.neg_intertwining_linearMap b₂ c)