structure BNPairOmegaContext (k : Type u) [CommRing k] (Ω : Type u) [Group Ω] : Type (u + 1)

Context for the $H_Ω ≃ k[Ω]$ structure result: an algebra $H$ over $k$ together with a $k$-linearly independent monoid homomorphism ch : Ω → H.

• H : Type u
• ringH : Ring self.H
• algH : Algebra k self.H
• ch : Ω → self.H
• ch_mul (σ τ : Ω) : self.ch σ * self.ch τ = self.ch (σ * τ)
• ch_one : self.ch 1 = 1
• ch_linearIndependent : LinearIndependent k self.ch

def BNPairOmegaContext.chMonoidHom {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (ctx : BNPairOmegaContext k Ω) : Ω →* ctx.H

Packages ch : Ω → H as a monoid homomorphism.

noncomputable def BNPairOmegaContext.algHomOmega {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (ctx : BNPairOmegaContext k Ω) : MonoidAlgebra k Ω →ₐ[k] ctx.H

Induced $k$-algebra homomorphism $k[Ω] → H$ extending chMonoidHom.

theorem BNPairOmegaContext.algHomOmega_injective {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (ctx : BNPairOmegaContext k Ω) : Function.Injective ⇑ctx.algHomOmega

Injectivity of the algebra map $k[Ω] → H$, which follows from linear independence of ch.

noncomputable def BNPairOmegaContext.HOmega_algEquiv {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (ctx : BNPairOmegaContext k Ω) : MonoidAlgebra k Ω ≃ₐ[k] ↥ctx.algHomOmega.range

The algebra isomorphism $k[Ω] ≃ₐ H_Ω$, where $H_Ω$ is the image subalgebra.

structure FullBNPairContext (k : Type u) [CommRing k] (Ω : Type u) [Group Ω] (W : Type u) [Group W] : Type (u + 1)

Full BN-pair context recording the data needed for the generalized Hecke-algebra structure theorem $H ≅ k[Ω] ⊗ H_o$: characters of $Ω$ and $W$, an inclusion $H_o → H$, a joint basis indexed by $Ω × W$, and the conjugation action omegaConj.

• H : Type u
• ringH : Ring self.H
• algH : Algebra k self.H
• H_o : Type u
• ringHo : Ring self.H_o
• algHo : Algebra k self.H_o
• ch : Ω → self.H
• ch_o : W → self.H_o
• incl : self.H_o →ₐ[k] self.H
• ch_full : Ω × W → self.H
• H_basis : Module.Basis (Ω × W) k self.H
• H_basis_eq (σw : Ω × W) : self.H_basis σw = self.ch_full σw
• ch_full_one (σ : Ω) : self.ch_full (σ, 1) = self.ch σ
• ch_full_incl (w : W) : self.ch_full (1, w) = self.incl (self.ch_o w)
• omegaConj : Ω → W → W
• omegaConj_one (w : W) : self.omegaConj 1 w = w
• omegaConj_mul (σ τ : Ω) (w : W) : self.omegaConj (σ * τ) w = self.omegaConj τ (self.omegaConj σ w)
• omegaConj_action_one (σ : Ω) : self.omegaConj σ 1 = 1
• omegaConj_action_mul (σ : Ω) (w w' : W) : self.omegaConj σ (w * w') = self.omegaConj σ w * self.omegaConj σ w'
• ch_mul_omega (σ τ : Ω) : self.ch σ * self.ch τ = self.ch (σ * τ)
• incl_mul (a b : self.H_o) : self.incl (a * b) = self.incl a * self.incl b
• ch_one : self.ch 1 = 1
• ch_o_one : self.ch_o 1 = 1
• incl_one : self.incl 1 = 1

theorem sigma_normalizes_left {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.ch_full (σ, w) = ctx.ch_full (σ, 1) * ctx.ch_full (1, w)

Axiom-level statement that $T_{(σ,w)} = T_σ · T_w$ on the joint basis.

theorem sigma_normalizes_right {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (w : W) (σ : Ω) : ctx.ch_full (1, w) * ctx.ch_full (σ, 1) = ctx.ch_full (σ, ctx.omegaConj σ w)

Axiom-level commutation: $T_w · T_σ = T_{(σ, σ·w)}$ encoding the action of $Ω$ on $W$.

theorem FullBNPairContext.ch_full_factorization {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.ch_full (σ, w) = ctx.ch σ * ctx.incl (ctx.ch_o w)

Joint-basis factorization: $T_{(σ,w)} = \mathrm{ch}_Ω(σ) · \iota(\mathrm{ch}_o(w))$.

theorem FullBNPairContext.omega_comm {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.incl (ctx.ch_o w) * ctx.ch σ = ctx.ch σ * ctx.incl (ctx.ch_o (ctx.omegaConj σ w))

Commutation rule $\iota(\mathrm{ch}_o(w)) · \mathrm{ch}_Ω(σ) = \mathrm{ch}_Ω(σ) · \iota(\mathrm{ch}_o(σ·w))$ mirroring omegaConj.

theorem FullBNPairContext.chH_conv_left_norm {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.ch σ * ctx.incl (ctx.ch_o w) = ctx.ch_full (σ, w)

Left-convolution form of the joint basis factorization.

theorem FullBNPairContext.chH_conv_right_norm {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (w : W) (σ : Ω) : ctx.incl (ctx.ch_o w) * ctx.ch σ = ctx.ch_full (σ, ctx.omegaConj σ w)

Right-convolution form: $\iota(\mathrm{ch}_o(w)) · \mathrm{ch}_Ω(σ) = T_{(σ, σ·w)}$.

theorem FullBNPairContext.full_commutation_relation {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.incl (ctx.ch_o w) * ctx.ch σ = ctx.ch σ * ctx.incl (ctx.ch_o (ctx.omegaConj σ w))

Restatement of omega_comm as the full commutation relation.

theorem FullBNPairContext.full_basis_factorization {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ : Ω) (w : W) : ctx.ch_full (σ, w) = ctx.ch σ * ctx.incl (ctx.ch_o w)

Alias for ch_full_factorization: $T_{(σ,w)} = \mathrm{ch}_Ω(σ) · \iota(\mathrm{ch}_o(w))$.

theorem FullBNPairContext.mul_basis_full {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) (σ τ : Ω) (w w' : W) : ctx.ch_full (σ, w) * ctx.ch_full (τ, w') = ctx.ch_full (σ * τ, 1) * ctx.incl (ctx.ch_o (ctx.omegaConj τ w) * ctx.ch_o w')

Product formula on the joint basis: $T_{(σ,w)} · T_{(τ,w')} = T_{(στ,1)} · \iota(\mathrm{ch}_o(τ·w) · \mathrm{ch}_o(w'))$.

def FullBNPairContext.structureIso {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) : ctx.H ≃ₗ[k] Ω × W →₀ k

Linear equivalence $H ≃ k^{(Ω × W)}$ given by the joint basis.

theorem FullBNPairContext.ch_full_injective {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) [Nontrivial k] : Function.Injective ctx.ch_full

The joint character map ch_full is injective.

theorem FullBNPairContext.hecke_structure_theorem {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (ctx : FullBNPairContext k Ω W) [Nontrivial k] : (∃ (b : Module.Basis (Ω × W) k ctx.H), ∀ (σw : Ω × W), b σw = ctx.ch_full σw) ∧ (∀ (σ τ : Ω) (w w' : W), ctx.ch_full (σ, w) * ctx.ch_full (τ, w') = ctx.ch_full (σ * τ, 1) * ctx.incl (ctx.ch_o (ctx.omegaConj τ w) * ctx.ch_o w')) ∧ (∀ (σ : Ω) (w : W), ctx.ch_full (σ, w) = ctx.ch σ * ctx.incl (ctx.ch_o w)) ∧ Function.Injective ctx.ch_full ∧ ctx.ch_full (1, 1) = 1 ∧ ctx.ch 1 = 1

The Hecke structure theorem for a generalized BN-pair (Section 6.3 of Garrett): $H$ has a $k$-basis indexed by $Ω × W$, multiplication splits as $T_{(σ,w)} · T_{(τ,w')} = T_{(στ,1)} · \iota(\mathrm{ch}_o(τ·w) · \mathrm{ch}_o(w'))$, the joint basis factors as $T_{(σ,w)} = \mathrm{ch}_Ω(σ) · \iota(\mathrm{ch}_o(w))$, ch_full is injective, and $T_{(1,1)} = 1 = \mathrm{ch}_Ω(1)$.