def conjHomeomorph {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : G ≃ₜ G

Conjugation by $g$ as a self-homeomorphism of a topological group $G$.

def conjSet {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (S : Set G) : Set G

The conjugate $gSg^{-1}$ of a subset $S \subseteq G$.

theorem conjSet_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (S : Set G) : conjSet g S = (fun (x : G) => g * x * g⁻¹) '' S

$gSg^{-1}$ as the image of $S$ under the conjugation map.

theorem isCompact_conjSet {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (S : Set G) (hS : IsCompact S) : IsCompact (conjSet g S)

Conjugation preserves compactness.

theorem isOpen_conjSet {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (S : Set G) (hS : IsOpen S) : IsOpen (conjSet g S)

Conjugation preserves openness.

theorem isClosed_conjSet {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (S : Set G) (hS : IsClosed S) : IsClosed (conjSet g S)

Conjugation preserves closedness.

def pointwiseFixer {G : Type u_1} {X : Type u_2} (act : G → X → X) (Y : Set X) : Set G

The pointwise fixer of a subset $Y \subseteq X$ under a group action: the set of group elements that fix every point of $Y$.

theorem one_mem_pointwiseFixer {G : Type u_1} [Group G] {X : Type u_2} (act : G → X → X) (hact_one : ∀ (x : X), act 1 x = x) (Y : Set X) : 1 ∈ pointwiseFixer act Y

The identity belongs to every pointwise fixer.

theorem inv_mem_pointwiseFixer {G : Type u_1} [Group G] {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (hact_one : ∀ (x : X), act 1 x = x) {Y : Set X} {g : G} (hg : g ∈ pointwiseFixer act Y) : g⁻¹ ∈ pointwiseFixer act Y

The pointwise fixer is closed under inversion.

theorem pointwiseFixer_iUnion {G : Type u_1} {X : Type u_2} {ι : Type u_3} (act : G → X → X) (C : ι → Set X) : pointwiseFixer act (⋃ (i : ι), C i) = ⋂ (i : ι), pointwiseFixer act (C i)

The fixer of a union is the intersection of fixers: $\mathrm{Fix}(\bigcup_i C_i) = \bigcap_i \mathrm{Fix}(C_i)$.

theorem pointwiseFixer_image_eq_conj {G : Type u_1} [Group G] {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (hact_one : ∀ (x : X), act 1 x = x) (h : G) (C₀ : Set X) : pointwiseFixer act (act h '' C₀) = (fun (b : G) => h * b * h⁻¹) '' pointwiseFixer act C₀

The fixer of a translated set equals the conjugate of the fixer: $\mathrm{Fix}(h \cdot C_0) = h \,\mathrm{Fix}(C_0)\, h^{-1}$.

theorem pointwise_fixer_compact_open {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (B : Subgroup G) (hB_compact : IsCompact ↑B) (hB_open : IsOpen ↑B) {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (hact_one : ∀ (x : X), act 1 x = x) (C₀ : Set X) (hB_fixer : ↑B = pointwiseFixer act C₀) (Y : Set X) (IsChamber : Set X → Prop) (hY_contains_chamber : ∃ (C : Set X), IsChamber C ∧ C ⊆ Y) {n : ℕ} (hn : 0 < n) (chambers : Fin n → Set X) (chambers_cover_Y : Y ⊆ ⋃ (i : Fin n), chambers i) (fixer_covers_chambers : ∀ g ∈ pointwiseFixer act Y, ∀ (i : Fin n), ∀ x ∈ chambers i, act g x = x) (chamber_transit : ∀ (i : Fin n), ∃ (h : G), chambers i = act h '' C₀) : IsOpen (pointwiseFixer act Y) ∧ IsCompact (pointwiseFixer act Y)

The pointwise fixer of a finite union of $G$-translates of the base chamber $C_0$ is both open and compact, given that the Borel subgroup $B$ fixes $C_0$ and is itself compact open.

theorem compact_subgroup_cluster_point {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (B : Subgroup G) (hB_compact : IsCompact ↑B) (u : ℕ → G) (hu : ∀ (i : ℕ), u i ∈ B) : ∃ β ∈ ↑B, MapClusterPt β Filter.atTop u

Any sequence valued in a compact subgroup $B$ has a cluster point in $B$.

theorem mapClusterPt_frequently_in_nhds {G : Type u_1} [TopologicalSpace G] {β : G} {u : ℕ → G} (hβ : MapClusterPt β Filter.atTop u) {V : Set G} (hV : V ∈ nhds β) (N : ℕ) : ∃ i ≥ N, u i ∈ V

A cluster point of $u_n$ has neighbourhoods $V$ which contain $u_i$ for arbitrarily large $i$.

theorem act_eq_of_mul_fixer {G : Type u_1} [Group G] {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (bⱼ f : G) {Y : Set X} (hf : f ∈ pointwiseFixer act Y) {x : X} (hx : x ∈ Y) : act (bⱼ * f) x = act bⱼ x

Right-multiplying by an element of the fixer of $Y$ does not change the action on points of $Y$.

theorem image_sub_from_fixer_chain {G : Type u_1} [Group G] {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) {Y : ℕ → Set X} {A₀ : Set X} {b : ℕ → G} (hb_maps : ∀ (i j : ℕ), i ≤ j → ∀ x ∈ Y i, act (b j) x ∈ A₀) {g : G} (hg_coset : ∀ (i : ℕ), ∃ j ≥ i, ∃ f ∈ pointwiseFixer act (Y i), g = b j * f) (x : X) : x ∈ ⋃ (i : ℕ), Y i → act g x ∈ A₀

A coset-of-fixer argument: if $g$ can be written as $b_j f$ with $f$ in the fixer of each $Y_i$, and the $b_j$ send $Y_i$ into $A_0$, then $g$ sends the union $\bigcup_i Y_i$ into $A_0$.

theorem maximally_strong_transitivity_core {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (B : Subgroup G) (hB_compact : IsCompact ↑B) (hB_open : IsOpen ↑B) {X : Type u_2} (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (hact_one : ∀ (x : X), act 1 x = x) (A₀ C₀ : Set X) (hC₀_sub : C₀ ⊆ A₀) (hB_fixer : ↑B = pointwiseFixer act C₀) (A' : Set X) (hC₀_in_A' : C₀ ⊆ A') (Y : ℕ → Set X) (hY_mono : ∀ (i : ℕ), Y i ⊆ Y (i + 1)) (hC₀_in_Y : C₀ ⊆ Y 0) (hY_union : A' = ⋃ (i : ℕ), Y i) (A_chain : ℕ → Set X) (hY_in_A : ∀ (i : ℕ), Y i ⊆ A_chain i) (b : ℕ → G) (hb : ∀ (i : ℕ), b i ∈ B) (hb_maps_apt : ∀ (i : ℕ), ∀ x ∈ A_chain i, act (b i) x ∈ A₀) (hY_in_Aj : ∀ (i j : ℕ), i ≤ j → Y i ⊆ A_chain j) (hF_open : ∀ (i : ℕ), IsOpen (pointwiseFixer act (Y i))) (hapt_surj : ∀ (g : G), (∀ x ∈ A', act g x ∈ A₀) → (fun (x : X) => act g x) '' A' = A₀) : ∃ g ∈ ↑B, (fun (x : X) => act g x) '' A' = A₀

Core technical lemma for strong transitivity: given a compact-open Borel $B$ acting on a topological building, an apartment $A'$ exhausted by an ascending chain $Y_i$ each mapped into the base apartment $A_0$ by elements $b_i \in B$, one finds a single $g \in B$ with $g \cdot A' = A_0$.

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

A bundle of data abstracting a thick building $X$ with a strongly transitive topological group action: the action and base chamber $C_0 \subseteq A_0$, a compact-open Borel $B$ that fixes $C_0$ pointwise, the notion of chamber, the maximal apartment system, chamber transitivity, and exhaustion data for each apartment.

• 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 = pointwiseFixer self.act self.C₀
• 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 (pointwiseFixer self.act (Y i))) (_ : ∀ (g : G), (∀ x ∈ A', self.act g x ∈ self.A₀) → (fun (x : X) => self.act g x) '' A' = self.A₀), True

theorem maximally_strong_transitivity_theorem {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (Δ : ThickBuildingData G X) (A' : Set X) : A' ∈ Δ.maxAptSystem → ∀ (C' : Set X), Δ.IsChamber C' → C' ⊆ A' → ∃ (g : G), (fun (x : X) => Δ.act g x) '' C' = Δ.C₀ ∧ (fun (x : X) => Δ.act g x) '' A' = Δ.A₀

Maximally strong transitivity (Bourbaki/Tits): the group $G$ acts transitively on pairs $(C', A')$ where $C'$ is a chamber contained in an apartment $A'$ of the maximal system — there is $g \in G$ sending the pair $(C', A')$ to the base pair $(C_0, A_0)$.

theorem ascending_chain_fixer_property {G : Type u_1} [Group G] {Apt : Type u_2} (act : G → Apt → Apt) (hact_mul : ∀ (g₁ g₂ : G) (a : Apt), act (g₁ * g₂) a = act g₁ (act g₂ a)) (hact_one : ∀ (a : Apt), act 1 a = a) (A₀ : Apt) (A : ℕ → Apt) (b : ℕ → G) (hb_map : ∀ (i : ℕ), act (b i) (A i) = A₀) (i j : ℕ) (hij : i ≤ j) : act ((b i)⁻¹ * b j) (A j) = A i

For an ascending chain of apartments $A_i$ each sent to $A_0$ by $b_i$, the composite $(b_i)^{-1} b_j$ sends $A_j$ back to $A_i$.

theorem preimage_of_image_eq {G : Type u_1} {X : Type u_2} [Group G] (act : G → X → X) (hact_mul : ∀ (g₁ g₂ : G) (x : X), act (g₁ * g₂) x = act g₁ (act g₂ x)) (hact_one : ∀ (x : X), act 1 x = x) (g : G) (A A₀ : Set X) (hg : (fun (x : X) => act g x) '' A = A₀) : A = (fun (x : X) => act g⁻¹ x) '' A₀

If $g \cdot A = A_0$, then $A = g^{-1} \cdot A_0$.

theorem strong_transitivity_on_max_system {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (Δ : ThickBuildingData G X) (A' : Set X) : A' ∈ Δ.maxAptSystem → ∃ (g : G), (fun (x : X) => Δ.act g x) '' A' = Δ.A₀

Strong transitivity on apartments: every apartment of the maximal system is $G$-translated to the base apartment $A_0$.

theorem G_stable_is_maximal_apartment_system {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (Δ : ThickBuildingData G X) (𝒜 : Set (Set X)) (h𝒜_stable : ∀ (g : G), ∀ A ∈ 𝒜, (fun (x : X) => Δ.act g x) '' A ∈ 𝒜) (hA₀_in_𝒜 : Δ.A₀ ∈ 𝒜) (h𝒜_sub_max : 𝒜 ⊆ Δ.maxAptSystem) : 𝒜 = Δ.maxAptSystem

Maximality corollary: any $G$-stable apartment system $\mathcal{A}$ containing $A_0$ and lying inside the maximal apartment system already equals the maximal apartment system.