structure Building.GroupAction {V : Type u_1} [DecidableEq V] (G : Type u_2) [Group G] (b : Building V) : Type (max u_1 u_2)

A group action on a building: a group $G$ acting on the vertex set $V$ that respects the simplicial structure (faces map to faces) and the apartment system (apartments map to apartments), plus the usual group action axioms. This packages the geometric "type II" action of a group on a building used to build a BN-pair from a strongly transitive action.

• smul : G → V → V
• smul_one (v : V) : self.smul 1 v = v
• smul_mul (g₁ g₂ : G) (v : V) : self.smul (g₁ * g₂) v = self.smul g₁ (self.smul g₂ v)
• smul_face (g : G) (s : Finset V) : s ∈ b.faces → Finset.image (self.smul g) s ∈ b.faces
• smul_apartment (g : G) (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∃ A' ∈ b.apartmentSystem.apartments, A'.faces = {s : Finset V | ∃ t ∈ A.faces, s = Finset.image (self.smul g) t}

def Building.GroupAction.smulFace {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (g : G) (s : Finset V) : Finset V

The action of $g \in G$ on a finite face $s$: the image of $s$ under $v \mapsto g \cdot v$.

def Building.GroupAction.smulFaces {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (g : G) (F : Set (Finset V)) : Set (Finset V)

The action of $g \in G$ on a set of faces $F$: image of $F$ under smulFace g.

theorem Building.GroupAction.smulFace_mul {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (g₁ g₂ : G) (s : Finset V) : act.smulFace (g₁ * g₂) s = act.smulFace g₁ (act.smulFace g₂ s)

Compatibility with multiplication: $(g_1 g_2) \cdot s = g_1 \cdot (g_2 \cdot s)$ on faces.

theorem Building.GroupAction.smulFace_one {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (s : Finset V) : act.smulFace 1 s = s

Identity acts trivially on faces: $1 \cdot s = s$.

theorem Building.GroupAction.smulFaces_mul {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (g₁ g₂ : G) (F : Set (Finset V)) : act.smulFaces (g₁ * g₂) F = act.smulFaces g₁ (act.smulFaces g₂ F)

Compatibility with multiplication on sets of faces: $(g_1 g_2) \cdot F = g_1 \cdot (g_2 \cdot F)$.

theorem Building.GroupAction.smulFaces_one {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (F : Set (Finset V)) : act.smulFaces 1 F = F

Identity acts trivially on sets of faces: $1 \cdot F = F$.

def Building.GroupAction.IsTypePreserving {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) {L : Type u_3} [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) : Prop

The action is type-preserving with respect to a labelling $\lambda : \text{faces} \to L$ if every $g \in G$ sends each face to one with the same label. This is the property that forces the BN-pair built from the action to have its $\pi$-projection well-defined.

def Building.GroupAction.IsStronglyTransitive {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) : Prop

The action is strongly transitive: for any two pairs $(A_1, C_1)$, $(A_2, C_2)$ of an apartment together with one of its chambers, some $g \in G$ sends $A_1 \to A_2$ and $C_1 \to C_2$. This is the geometric hypothesis used to build a BN-pair from the action.

def Building.GroupAction.chamberStabilizer {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (C₀ : Finset V) : Subgroup G

The chamber stabilizer $\mathrm{Stab}_G(C_0) = \{g \in G : g \cdot C_0 = C_0\}$, the subgroup that fixes the chamber $C_0$ setwise. This will become the Borel subgroup $B$.

def Building.GroupAction.apartmentStabilizer {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (A₀ : SimplicialComplex V) : Subgroup G

The apartment stabilizer $\mathrm{Stab}_G(A_0)$: the subgroup of $G$ that maps the apartment $A_0$ to itself setwise. This will become the subgroup $N$ of the BN-pair.

def Building.GroupAction.torus {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (C₀ : Finset V) (A₀ : SimplicialComplex V) : Subgroup G

The torus $T = \mathrm{Stab}_G(C_0) \cap \mathrm{Stab}_G(A_0)$: the subgroup fixing both the base chamber and the base apartment. This will become the torus $T = B \cap N$.

def Building.GroupAction.faceStabilizer {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (F : Finset V) : Subgroup G

The face stabilizer of an arbitrary face $F$: $\mathrm{Stab}_G(F) = \{g \in G : g \cdot F = F\}$. Specializes to chamberStabilizer when $F$ is a chamber.

def Building.GroupAction.standardParabolic {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) {L : Type u_3} [DecidableEq L] (lab : Labelling b.toSimplicialComplex L) (C₀ : Finset V) (S' : Finset L) : Subgroup G

The geometric standard parabolic $P_{S'}$ as the stabilizer of the subface of $C_0$ spanned by the vertices whose label lies in $S' \subseteq L$. Matches the algebraic $P_{S'} = BW_{S'}B$ under the BN-pair built from the action.

def Building.GroupAction.bruhatCosetFromRetraction {V : Type u_1} [DecidableEq V] {G : Type u_2} [Group G] {b : Building V} (act : GroupAction G b) (ρ : BuildingRetraction b) (C₀ : Finset V) (g w : G) : Prop

Predicate: $g$ and $w$ land in the same Bruhat double coset $BwB$ as measured by the retraction $\rho$ onto the base apartment; specifically, $\rho(g \cdot C_0) = w \cdot C_0$ in the apartment.

structure BNPairFromBuildingData {V : Type u_2} [DecidableEq V] (G : Type u_3) [Group G] (b : Building V) (ct : b.CoxeterTypeOfBuilding) : Type (max u_2 u_3)

The data needed to build a BN-pair from a strongly transitive action on a building. Packages: a GroupAction of $G$ on the building $b$, a chosen base apartment $A_0$ with chamber $C_0$, a bijection $\varphi : \text{chambers of } A_0 \to W$ with $\varphi(C_0) = 1$ that intertwines the $N$-action with left multiplication, and the Bruhat-style hypothesis $G = B \cdot N \cdot B$. From this data one extracts the strict BN-pair $(B, N, T, \pi)$.

• act : Building.GroupAction G b
• A₀ : SimplicialComplex V
• hA₀ : self.A₀ ∈ b.apartmentSystem.apartments
• C₀ : Finset V
• hC₀_max_A₀ : self.A₀.IsMaximal self.C₀
• φ : Finset V → ct.matrix.Group
• φ_inj (C : Finset V) : self.A₀.IsMaximal C → ∀ (D : Finset V), self.A₀.IsMaximal D → self.φ C = self.φ D → C = D
• φ_surj (w : ct.matrix.Group) : ∃ (C : Finset V), self.A₀.IsMaximal C ∧ self.φ C = w
• φ_base : self.φ self.C₀ = 1
• strongly_transitive : self.act.IsStronglyTransitive
• smul_preserves_apt_max (n : G) : self.act.smulFaces n self.A₀.faces = self.A₀.faces → ∀ (C : Finset V), self.A₀.IsMaximal C → self.A₀.IsMaximal (self.act.smulFace n C)
• φ_equivariant (n : G) : self.act.smulFaces n self.A₀.faces = self.A₀.faces → ∀ (C : Finset V), self.A₀.IsMaximal C → self.φ (self.act.smulFace n C) = self.φ (self.act.smulFace n self.C₀) * self.φ C
• bruhat_decomp (g : G) : ∃ (b₁ : G) (_ : self.act.smulFace b₁ self.C₀ = self.C₀) (n : G) (_ : self.act.smulFaces n self.A₀.faces = self.A₀.faces) (b₂ : G) (_ : self.act.smulFace b₂ self.C₀ = self.C₀), g = b₁ * n * b₂

def BNPairFromBuildingData.B {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : Subgroup G

The Borel subgroup $B$: the stabilizer of the base chamber $C_0$.

def BNPairFromBuildingData.N {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : Subgroup G

The subgroup $N$: the stabilizer of the base apartment $A_0$.

def BNPairFromBuildingData.T {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : Subgroup G

The torus $T$: stabilizer of both $C_0$ and $A_0$, i.e. $T = B \cap N$.

theorem BNPairFromBuildingData.T_eq_inf {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : data.T = data.B ⊓ data.N

Definitional unfolding: $T = B \cap N$.

def BNPairFromBuildingData.πFun {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) (n : ↥data.N) : ct.matrix.Group

The underlying function of the projection $\pi : N \to W$: send $n \in N$ to $\varphi(n \cdot C_0)$, i.e. the chamber of $A_0$ that $n$ maps $C_0$ to, read off as a Weyl group element via $\varphi$.

theorem BNPairFromBuildingData.πFun_mul {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) (n₁ n₂ : ↥data.N) : data.πFun (n₁ * n₂) = data.πFun n₁ * data.πFun n₂

Multiplicativity of $\pi$: $\pi(n_1 n_2) = \pi(n_1) \pi(n_2)$, using the equivariance of $\varphi$ under the $N$-action on the chambers of $A_0$.

def BNPairFromBuildingData.π {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : ↥data.N →* ct.matrix.Group

The Weyl projection $\pi : N \to W$ as a group homomorphism, packaging πFun with its multiplicativity and unit-preservation.

theorem BNPairFromBuildingData.π_surj {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : Function.Surjective ⇑data.π

Surjectivity of $\pi$: every $w \in W$ is realized by some $n \in N$. Uses strong transitivity of $G$ on apartment-chamber pairs to find an element moving $C_0$ to the chamber corresponding to $w$ in $A_0$.

theorem BNPairFromBuildingData.π_ker {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) (n : ↥data.N) : data.π n = 1 ↔ ↑n ∈ data.T

Kernel of $\pi$ equals $T$. $\pi(n) = 1$ iff $n$ fixes $C_0$ (forwards: $\varphi$ is injective on chambers, so $n \cdot C_0 = C_0$; backwards: $T = B \cap N$ fixes $C_0$ and $\varphi(C_0) = 1$).

theorem BNPairFromBuildingData.generates {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : Subgroup.closure (↑data.B ∪ ↑data.N) = ⊤

$B$ and $N$ generate $G$: a direct consequence of the Bruhat-style decomposition $G = B \cdot N \cdot B$ supplied by bruhat_decomp.

def BNPairFromBuildingData.toBNPair {V : Type u_2} [DecidableEq V] {G : Type u_3} [Group G] {b : Building V} {ct : b.CoxeterTypeOfBuilding} (data : BNPairFromBuildingData G b ct) : BNPair G ct.matrix

The strict BN-pair built from the building data. Bundles $B$, $N$, $T = B \cap N$, the surjective homomorphism $\pi : N \to W$ with kernel $T$, and the generation property $\langle B, N \rangle = G$, producing a BNPair G ct.matrix.