def restrictIsometricAction {G : Type u_1} [Group G] {X : Type u_2} [MetricSpace X] (act : IsometricAction G X) (K : Subgroup G) : IsometricAction (↥K) X

Restrict an isometric action of $G$ on $X$ to an action of a subgroup $K \leq G$.

def FixedPointSubgroups.orbitSet {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (E : Set Gt) (x : X) : Set X

The orbit $E \cdot x = \{g \cdot x \mid g \in E\}$ of a point $x$ under a subset $E$ of the group.

def FixedPointSubgroups.actionOnSet {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (E : Set Gt) (Y : Set X) : Set X

The image $E \cdot Y = \{g \cdot y \mid g \in E,\, y \in Y\}$ of a subset $Y \subseteq X$ under a subset $E$ of the group.

def FixedPointSubgroups.pointStabilizer {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (x : X) : Subgroup Gt

The stabilizer subgroup $\mathrm{Stab}(x) = \{g \in G \mid g \cdot x = x\}$ of a point $x \in X$.

structure FixedPointSubgroups.BuildingGroupContext (Gt : Type u_3) [Group Gt] (B_idx : Type u_4) (M : CoxeterMatrix B_idx) : Type (max (max u_3 u_4) (u_5 + 1))

A package of data and axioms needed to relate bounded subgroups of a group $G^t$ acting on a $\mathrm{CAT}(0)$ space $X$ to point stabilizers: an isometric action satisfying the negative-curvature inequality, a generalised BN-pair, a group bornology, a base chamber point, and compatibility axioms ensuring boundedness is equivalent to having a bounded orbit.

• X : Type u_5
• metricSpace : MetricSpace self.X
• completeSpace : CompleteSpace self.X
• nonempty : Nonempty self.X
• nci : NegativeCurvatureInequality self.X
• action : IsometricAction Gt self.X
• gbnpair : GeneralizedBNPair Gt M
• bruhatProps : self.gbnpair.strictBNPair.BruhatProperties
• born : CompactSubgroups.GroupBornology Gt
• chamber_point : self.X
• borel_fixes_chamber_point (b : Gt) : b ∈ Subgroup.map self.gbnpair.G.subtype self.gbnpair.strictBNPair.B → self.action.smul b self.chamber_point = self.chamber_point
• Tt_fixes_chamber_point (t : Gt) : t ∈ self.gbnpair.Tt → self.action.smul t self.chamber_point = self.chamber_point
• born_bounded_orbit_at_chamber_point (E : Set Gt) : self.born.isBounded E → Bornology.IsBounded (orbitSet self.action E self.chamber_point)
• orbit_bounded_at_chamber_point_born_bounded (E : Set Gt) : Bornology.IsBounded (orbitSet self.action E self.chamber_point) → self.born.isBounded E
• Tt_in_every_maximal_bounded (K : Subgroup Gt) : CompactSubgroups.IsMaximalBounded self.born K → ∀ t ∈ self.gbnpair.Tt, t ∈ K
• stabilizer_of_bounded_orbit (x : self.X) (H : Subgroup Gt) : pointStabilizer self.action x ≤ H → Bornology.IsBounded (orbitSet self.action (↑H) x) → H ≤ pointStabilizer self.action x

theorem FixedPointSubgroups.orbit_nonempty {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (K : Subgroup Gt) (x : X) : (orbitSet act (↑K) x).Nonempty

The orbit of $x$ under a subgroup $K$ is non-empty (it contains $x$ itself).

theorem FixedPointSubgroups.orbit_stable_restricted {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (K : Subgroup Gt) (x : X) : (restrictIsometricAction act K).IsStable (orbitSet act (↑K) x)

The orbit $K \cdot x$ is stable under the restricted action of $K$ on $X$.

theorem FixedPointSubgroups.subgroup_le_stabilizer_of_restricted_fixed {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (K : Subgroup Gt) (x₀ : X) (hfix : (restrictIsometricAction act K).IsFixedPoint x₀) : K ≤ pointStabilizer act x₀

If $x_0$ is a fixed point of the restricted action of $K$, then $K$ is contained in the stabilizer of $x_0$.

theorem FixedPointSubgroups.stabilizer_orbit_eq_singleton {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (x : X) : orbitSet act (↑(pointStabilizer act x)) x = {x}

The orbit of $x$ under its stabilizer is exactly $\{x\}$.

theorem FixedPointSubgroups.born_bounded_orbit_bounded {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (E : Set Gt) (hE : ctx.born.isBounded E) (x : ctx.X) : Bornology.IsBounded (orbitSet ctx.action E x)

If a subset $E \subseteq G^t$ is bounded with respect to the group bornology, then its orbit $E \cdot x$ is bounded in $X$ for every point $x$.

theorem FixedPointSubgroups.orbit_bounded_born_bounded {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (E : Set Gt) (h : ∃ (x : ctx.X), Bornology.IsBounded (orbitSet ctx.action E x)) : ctx.born.isBounded E

Converse: if some orbit $E \cdot x$ is bounded in $X$, then $E$ itself is bounded in the group bornology.

theorem FixedPointSubgroups.stabilizer_maximal_born_ax {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (x : ctx.X) (H : Subgroup Gt) : pointStabilizer ctx.action x < H → ¬ctx.born.isBounded ↑H

Maximality of stabilizers: any strictly larger subgroup $H$ than $\mathrm{Stab}(x)$ fails to be bounded.

theorem FixedPointSubgroups.decomp_stable_in_stabilizer {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (K : Subgroup Gt) (hK : CompactSubgroups.IsMaximalBounded ctx.born K) (σ : Gt) (hσ : σ ∈ ctx.gbnpair.Tt) (g : Gt) (_hg : g ∈ ctx.gbnpair.G) (k : Gt) (hk : k ∈ K) (hk_eq : k = σ * g) : g ∈ K

If $K$ is a maximal bounded subgroup and $k = \sigma g$ with $\sigma$ in the small torus $T^t$, then $g \in K$ — left factors from $T^t$ can be absorbed into $K$.

theorem FixedPointSubgroups.stabilizer_born_bounded_thm {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (x : ctx.X) : ctx.born.isBounded ↑(pointStabilizer ctx.action x)

Every point stabilizer is bounded in the group bornology.

theorem FixedPointSubgroups.orbit_bounded_implies_action_bounded {Gt : Type u_3} [Group Gt] {X : Type u_4} [MetricSpace X] (act : IsometricAction Gt X) (E : Set Gt) (x₀ : X) (h_orbit_bdd : Bornology.IsBounded (orbitSet act E x₀)) (Y : Set X) (hY : Bornology.IsBounded Y) : Bornology.IsBounded (actionOnSet act E Y)

If both $E \cdot x_0$ and a set $Y$ are bounded, then the action set $E \cdot Y$ is bounded as well.

theorem FixedPointSubgroups.actionOnSet_singleton {Gt : Type u_1} [Group Gt] {X : Type u_2} [MetricSpace X] (act : IsometricAction Gt X) (E : Set Gt) (x : X) : actionOnSet act E {x} = orbitSet act E x

Acting on the singleton $\{x\}$ recovers the orbit $E \cdot x$.

theorem FixedPointSubgroups.BoundedSubsetsEquivalence {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (E : Set Gt) : (ctx.born.isBounded E → ∀ (x : ctx.X), Bornology.IsBounded (orbitSet ctx.action E x)) ∧ ((∃ (x : ctx.X), Bornology.IsBounded (orbitSet ctx.action E x)) → ∀ (Y : Set ctx.X), Bornology.IsBounded Y → Bornology.IsBounded (actionOnSet ctx.action E Y)) ∧ ((∀ (Y : Set ctx.X), Bornology.IsBounded Y → Bornology.IsBounded (actionOnSet ctx.action E Y)) → ctx.born.isBounded E)

A cyclic equivalence of three notions of boundedness for a subset $E \subseteq G^t$: boundedness in the group bornology, having a bounded orbit, and producing only bounded images of bounded subsets of $X$.

theorem FixedPointSubgroups.stabilizer_is_maximal_bounded {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (x₀ : ctx.X) : CompactSubgroups.IsMaximalBounded ctx.born (pointStabilizer ctx.action x₀)

Every point stabilizer $\mathrm{Stab}(x_0)$ is a maximal bounded subgroup in the group bornology.

theorem FixedPointSubgroups.stabilizer_Gt_decomp_mem_right {Gt : Type u_3} [Group Gt] {B_idx : Type u_4} [Fintype B_idx] [DecidableEq B_idx] {M : CoxeterMatrix B_idx} (ctx : BuildingGroupContext Gt B_idx M) (K : Subgroup Gt) (hK : CompactSubgroups.IsMaximalBounded ctx.born K) (σ : Gt) (hσ : σ ∈ ctx.gbnpair.Tt) (g : Gt) (hg : g ∈ ctx.gbnpair.G) (k : Gt) (hk : k ∈ K) (hk_eq : k = σ * g) : g ∈ K

Restatement of decomp_stable_in_stabilizer in the finite-type $B_{\mathrm{idx}}$ setting: $T^t$-factors can be absorbed into a maximal bounded subgroup.