structure GeneralizedHecke.GeneralizedBNPairData (G : Type u_1) [Group G] : Type u_1

Data of a generalized BN-pair on a group G: subgroups recording the label-preserving subgroup, Borel, normalizer $N$, restricted normalizer $N ∩$ labelPreserving, the torus $N ∩ B$, and the restricted torus, together with their intersection axioms.

• labelPreserving : Subgroup G
• borel : Subgroup G
• normalizerN : Subgroup G
• normalizerRestricted : Subgroup G
• torus : Subgroup G
• torusRestricted : Subgroup G
• borel_in_labelPreserving : self.borel ≤ self.labelPreserving
• normalizerRestricted_eq : self.normalizerRestricted = self.normalizerN ⊓ self.labelPreserving
• torus_eq : self.torus = self.normalizerN ⊓ self.borel
• torusRestricted_eq : self.torusRestricted = self.normalizerRestricted ⊓ self.borel

def GeneralizedHecke.GeneralizedBNPairData.BorelInLabelPreserving {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : Prop

Property: the Borel sits inside the label-preserving subgroup.

def GeneralizedHecke.GeneralizedBNPairData.NormalizerRestrictedIsIntersection {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : Prop

Property: the restricted normalizer is exactly the intersection of $N$ with the label-preserving subgroup.

def GeneralizedHecke.GeneralizedBNPairData.TorusIsIntersection {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : Prop

Property: the torus $T = N ∩ B$.

def GeneralizedHecke.GeneralizedBNPairData.TorusRestrictedIsIntersection {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : Prop

Property: the restricted torus equals $N_{\text{res}} ∩ B$.

theorem GeneralizedHecke.GeneralizedBNPairData.borelInLabelPreserving_holds {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : d.BorelInLabelPreserving

Repackages the axiom borel_in_labelPreserving as the predicate BorelInLabelPreserving.

theorem GeneralizedHecke.GeneralizedBNPairData.normalizerRestrictedIsIntersection_holds {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : d.NormalizerRestrictedIsIntersection

Unfolds normalizerRestricted = N ⊓ labelPreserving membership pointwise.

theorem GeneralizedHecke.GeneralizedBNPairData.torusIsIntersection_holds {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : d.TorusIsIntersection

Unfolds torus = N ⊓ B membership pointwise.

theorem GeneralizedHecke.GeneralizedBNPairData.torusRestrictedIsIntersection_holds {G : Type u_1} [Group G] (d : GeneralizedBNPairData G) : d.TorusRestrictedIsIntersection

Unfolds torusRestricted = N_{\text{res}} ⊓ B membership pointwise.

def GeneralizedHecke.BiInvariantFunction {G : Type u_1} {R : Type u_2} [Group G] (B : Subgroup G) (f : G → R) : Prop

A function $f : G → R$ is $B$-bi-invariant if $f(b_1 g b_2) = f(g)$ for all $b_1, b_2 ∈ B$ and all $g ∈ G$.

structure GeneralizedHecke.HeckeAlgebraData (G : Type u_1) (R : Type u_2) [Group G] [CommRing R] : Type (max (max u_1 u_2) (u_3 + 1))

Abstract data of a Hecke algebra associated to a Borel subgroup $B ⊆ G$: an $R$-module carrier with a convolution product making it into an $R$-algebra.

• borel : Subgroup G
• carrier : Type u_3
• add : self.carrier → self.carrier → self.carrier
• zero : self.carrier
• smul : R → self.carrier → self.carrier
• convolution : self.carrier → self.carrier → self.carrier
• one : self.carrier
• conv_assoc (f g h : self.carrier) : self.convolution (self.convolution f g) h = self.convolution f (self.convolution g h)
• one_conv (f : self.carrier) : self.convolution self.one f = f
• conv_one (f : self.carrier) : self.convolution f self.one = f
• conv_add (f g h : self.carrier) : self.convolution f (self.add g h) = self.add (self.convolution f g) (self.convolution f h)
• add_conv (f g h : self.carrier) : self.convolution (self.add f g) h = self.add (self.convolution f h) (self.convolution g h)
• smul_conv (r : R) (f g : self.carrier) : self.convolution (self.smul r f) g = self.smul r (self.convolution f g)

structure GeneralizedHecke.OmegaQuotient (G : Type u_1) [Group G] : Type u_1

The quotient datum $Ω = T / T_{\text{res}}$ as a chain of subgroup inclusions.

• torus : Subgroup G
• torusRestricted : Subgroup G
• le : self.torusRestricted ≤ self.torus

structure GeneralizedHecke.SemidirectDecomposition (G : Type u_1) (W : Type u_2) (Ω : Type u_3) [Group G] [Group W] [Group Ω] : Type (max (max u_1 u_2) u_3)

Abstract semidirect-product decomposition data for $N$ inside $G$ as a product of $W$ and $Ω$, with chosen projections to each factor.

• normalizerN : Subgroup G
• torusRestricted : Subgroup G
• le : self.torusRestricted ≤ self.normalizerN
• projW : G → W
• projΩ : G → Ω

theorem GeneralizedHecke.biInvariant_const {G : Type u_1} {R : Type u_2} [Group G] (B : Subgroup G) (c : R) : BiInvariantFunction B fun (x : G) => c

The constant function is bi-invariant for any Borel subgroup.

structure GeneralizedHecke.OmegaConvolutionData (k : Type u) [CommRing k] (Ω : Type u) [Group Ω] : Type (u + 1)

Data of a convolution embedding $Ω → H$ into a $k$-algebra: the character map ch is a $k$-linearly independent monoid homomorphism.

• 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 GeneralizedHecke.OmegaConvolutionData.chMonoidHom {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (d : OmegaConvolutionData k Ω) : Ω →* d.H

Packages ch : Ω → H as a monoid homomorphism.

noncomputable def GeneralizedHecke.OmegaConvolutionData.algHomToH {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (d : OmegaConvolutionData k Ω) : MonoidAlgebra k Ω →ₐ[k] d.H

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

theorem GeneralizedHecke.OmegaConvolutionData.algHomToH_injective {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (d : OmegaConvolutionData k Ω) : Function.Injective ⇑d.algHomToH

Linear independence of ch implies the algebra map $k[Ω] → H$ is injective.

noncomputable def GeneralizedHecke.OmegaConvolutionData.proposition_HOmega_iso_groupAlgebra {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] (d : OmegaConvolutionData k Ω) : MonoidAlgebra k Ω ≃ₐ[k] ↥d.algHomToH.range

The proposition that $k[Ω] ≃ₐ H_Ω$, the subalgebra of $H$ generated by the image of $Ω$.

structure GeneralizedHecke.HeckeConvolutionIdentities (k : Type u) [CommRing k] (Ω : Type u) [Group Ω] (W : Type u) [Group W] : Type (u + 1)

Convolution identities relating the $Ω$-characters, $W$-characters, and the joint characters in a generalized Hecke algebra, including the conjugation action omegaConj.

• H : Type u
• ringH : Ring self.H
• algH : Algebra k self.H
• ch_omega : Ω → self.H
• ch_weyl : W → self.H
• ch_full : Ω → W → self.H
• omegaConj : Ω → W → W
• conv_left (σ : Ω) (w : W) : self.ch_omega σ * self.ch_weyl w = self.ch_full σ w
• conv_right (w : W) (σ : Ω) : self.ch_weyl w * self.ch_omega σ = self.ch_full σ (self.omegaConj σ w)

theorem GeneralizedHecke.HeckeConvolutionIdentities.commutation_relation {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (d : HeckeConvolutionIdentities k Ω W) (σ : Ω) (w : W) : d.ch_weyl w * d.ch_omega σ = d.ch_omega σ * d.ch_weyl (d.omegaConj σ w)

The commutation relation $T_w · T_σ = T_σ · T_{σ·w}$ obtained from the two factorizations of ch_full σ (omegaConj σ w).

theorem GeneralizedHecke.HeckeConvolutionIdentities.ch_full_factorization {k : Type u} [CommRing k] {Ω : Type u} [Group Ω] {W : Type u} [Group W] (d : HeckeConvolutionIdentities k Ω W) (σ : Ω) (w : W) : d.ch_full σ w = d.ch_omega σ * d.ch_weyl w

Restates conv_left as a factorization ch_full σ w = ch_omega σ * ch_weyl w.