structure ParahoricSubgroup (G : Type u_3) [Group G] {B_idx : Type u_4} (M : CoxeterMatrix B_idx) : Type (max u_3 u_4)

A parahoric subgroup of $G$ from a BN-pair of indecomposable affine Coxeter type, bundled with a chosen subset $J \subseteq B$ of simple generators. The underlying subgroup is the standard parabolic $P_J$.

• bnpair : BNPair G M
• generatorSubset : Set B_idx
• indecomposable : M.IsIndecomposable
• affine : M.IsAffine

def ParahoricSubgroup.toSet {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (P : ParahoricSubgroup G M) : Set G

The underlying set of a parahoric subgroup, namely the standard parabolic $P_J$.

structure ParabolicSubgroupAtInfinity (G : Type u_3) [Group G] {B_idx : Type u_4} (M : CoxeterMatrix B_idx) : Type (max u_3 u_4)

A "parabolic subgroup at infinity" of $G$: a subgroup that is parabolic with respect to the BN-pair, conceptually corresponding to a parabolic associated to the spherical building at infinity of an affine building.

• bnpair : BNPair G M
• subgroup : Subgroup G
• isParabolic : self.bnpair.IsParabolic self.subgroup

def ParahoricParabolicCorrespondence {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Prop

The parahoric/parabolic correspondence asserts that for every subset $J \subseteq B$ there is a (typically smaller) subset $J_0 \subseteq J$ with $P_J \subseteq P_{J_0}$.

def BruhatDecomposition {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Prop

The Bruhat decomposition predicate on a BN-pair: $G$ is the disjoint union of the Bruhat cells $BwB$ indexed by $w \in W$.

def CartanDecomposition {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (_bp : BNPair G M) (K : Subgroup G) (A : Set G) : Prop

The Cartan decomposition $G = KAK$: every $g \in G$ factors as $g = k_1 a k_2$ with $k_1, k_2 \in K$ and $a \in A$, where $K$ is a maximal compact subgroup and $A$ is a chosen torus or split component.

def IwasawaDecomposition {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (_bp : BNPair G M) (K : Subgroup G) (A N_unip : Set G) : Prop

The Iwasawa decomposition $G = KAN$: every $g \in G$ factors as $g = kan$ with $k \in K$, $a \in A$ and $n \in N$ unipotent.

structure TopologicalGroupDef (G : Type u_1) [TopologicalSpace G] [Group G] : Prop

Bundled definition of a topological group: continuous multiplication and inversion.

• mul_continuous : Continuous fun (p : G × G) => p.1 * p.2
• inv_continuous : Continuous Inv.inv

theorem TopologicalGroupDef.of_isTopologicalGroup (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : TopologicalGroupDef G

Extract the bundled TopologicalGroupDef from Mathlib's IsTopologicalGroup.

theorem TopologicalGroupDef.toIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] (h : TopologicalGroupDef G) : IsTopologicalGroup G

Convert the bundled TopologicalGroupDef to Mathlib's IsTopologicalGroup.

theorem pointwiseFixer_compact_open_prop {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (B : Subgroup G) (hB_compact : IsCompact ↑B) (hB_open : IsOpen ↑B) (G_Y : Set G) {n : ℕ} (hn : 0 < n) (h_conj : Fin n → G) (hG_Y_eq : G_Y = ⋂ (i : Fin n), (fun (x : G) => h_conj i * x * (h_conj i)⁻¹) '' ↑B) : IsOpen G_Y ∧ IsCompact G_Y

A finite intersection of conjugates $\bigcap_i g_i B g_i^{-1}$ of a compact-open subgroup $B$ in a topological group $G$ is again open and compact. This is the topological backbone for showing that pointwise fixers of finite sets of chambers in a building are compact-open, as needed for strong transitivity arguments.

def IsMaximallyStronglyTransitive {G : Type u_1} {X : Type u_2} (act : G → X → X) (IsChamber : Set X → Prop) (aptSystem : Set (Set X)) (C₀ A₀ : Set X) : Prop

A group action is maximally strongly transitive if, for every apartment $A'$ in the system and every chamber $C' \subseteq A'$, some $g \in G$ simultaneously sends $C'$ to the fixed reference chamber $C_0$ and $A'$ to the fixed reference apartment $A_0$. This is the relevant transitivity hypothesis for maximal apartment systems in non-spherical buildings.

structure MaxStrongTransData (G : Type u_1) (X : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type (max u_1 u_2)

Bundle of data witnessing a maximally strongly transitive action of a topological group $G$ on a building-like set $X$. It records the action, a reference chamber $C_0 \subseteq A_0$ inside a reference apartment, the compact-open stabiliser $B$ of $C_0$, the system of maximal apartments and its $G$-invariance, chamber-transitivity of $G$, and an exhaustion of each apartment by $B$-conjugable pieces that together force a translating element back into $A_0$. This is the precise hypothesis package used to prove strong transitivity on maximal apartment systems.

• act : G → X → X
• act_mul (g₁ g₂ : G) (x : X) : self.act (g₁ * g₂) x = self.act g₁ (self.act g₂ x)
• act_one (x : X) : self.act 1 x = x
• C₀ : Set X
• A₀ : Set X
• chamber_sub_apt : self.C₀ ⊆ self.A₀
• B : Subgroup G
• B_eq_fixer : ↑self.B = {g : G | ∀ x ∈ self.C₀, self.act g x = x}
• B_compact : IsCompact ↑self.B
• B_open : IsOpen ↑self.B
• IsChamber : Set X → Prop
• C₀_is_chamber : self.IsChamber self.C₀
• maxAptSystem : Set (Set X)
• A₀_in_max : self.A₀ ∈ self.maxAptSystem
• maxAptSystem_invariant (g : G) (A' : Set X) : A' ∈ self.maxAptSystem → (fun (x : X) => self.act g x) '' A' ∈ self.maxAptSystem
• apt_contains_chamber (A' : Set X) : A' ∈ self.maxAptSystem → ∃ (C' : Set X), self.IsChamber C' ∧ C' ⊆ A'
• chamber_transitive (C' : Set X) : self.IsChamber C' → ∃ (h : G), (fun (x : X) => self.act h x) '' self.C₀ = C'
• exhaustion_data (A' : Set X) : A' ∈ self.maxAptSystem → self.C₀ ⊆ A' → ∃ (Y : ℕ → Set X) (_ : ∀ (i : ℕ), Y i ⊆ Y (i + 1)) (_ : self.C₀ ⊆ Y 0) (_ : A' = ⋃ (i : ℕ), Y i) (A_chain : ℕ → Set X) (_ : ∀ (i : ℕ), Y i ⊆ A_chain i) (b : ℕ → G) (_ : ∀ (i : ℕ), b i ∈ self.B) (_ : ∀ (i : ℕ), ∀ x ∈ A_chain i, self.act (b i) x ∈ self.A₀) (_ : ∀ (i j : ℕ), i ≤ j → Y i ⊆ A_chain j) (_ : ∀ (i : ℕ), IsOpen {g : G | ∀ y ∈ Y i, self.act g y = y}) (_ : ∀ (g : G), (∀ x ∈ A', self.act g x ∈ self.A₀) → (fun (x : X) => self.act g x) '' A' = self.A₀), True

structure CanonicalTranslation (G : Type u_3) [Group G] {B_idx : Type u_4} (M : CoxeterMatrix B_idx) (bp : BNPair G M) : Type u_4

A canonical translation in an affine Coxeter system: an element of the Coxeter group that conjugates the set of simple reflections to itself and has infinite order. Such elements act as translations on the geometric realisation of the affine apartment.

• element : M.Group
• permutes_simples (s : B_idx) : ∃ (s' : B_idx), self.element * M.toCoxeterSystem.simple s * self.element⁻¹ = M.toCoxeterSystem.simple s'
• infinite_order (n : ℕ) : n ≠ 0 → self.element ^ n ≠ 1

structure LeviFiltration (G : Type u_3) [Group G] {B_idx : Type u_4} (M : CoxeterMatrix B_idx) : Type (max u_3 u_4)

A descending filtration $P_J = F_0 \supseteq F_1 \supseteq \cdots$ on a standard parabolic subgroup $P_J$ of a BN-pair, abstracting the Moy-Prasad / Levi filtrations used in the structure theory of $p$-adic groups.

• bnpair : BNPair G M
• generatorSubset : Set B_idx
• filtration : ℕ → Set G
• level_zero : self.filtration 0 = self.bnpair.standardParabolic self.generatorSubset
• descending (n : ℕ) : self.filtration (n + 1) ⊆ self.filtration n