class AffineBuildingSLVStrong.DVRTopologicalAssumptions (C : DVRContext) [TopologicalSpace C.k] : Prop

Topological hypotheses on the fraction field $k$ of a complete DVR: the valuation ring $\mathfrak{o}$ is open and compact in $k$, its maximal ideal is open, $k$ is a $T_1$ topological ring. This is the package of assumptions needed to make the Iwahori subgroup compact-open in $SL_V(k)$.

• isOpen_valRing : IsOpen {x : C.k | C.isInO x}
• isOpen_maxIdeal : IsOpen {x : C.k | C.isInMaxIdeal x}
• isTopologicalRing : IsTopologicalRing C.k
• isCompact_valRing : IsCompact {x : C.k | C.isInO x}
• t1Space : T1Space C.k

noncomputable def AffineBuildingSLVStrong.stdBasisVec (C : DVRContext) (j : Fin C.n) : Fin C.n → C.k

The $j$-th standard basis vector $e_j \in k^n$.

theorem AffineBuildingSLVStrong.stdBasisVec_ne_zero (C : DVRContext) (j : Fin C.n) : stdBasisVec C j ≠ 0

Each standard basis vector $e_j$ is nonzero.

noncomputable def AffineBuildingSLVStrong.stdLine (C : DVRContext) (j : Fin C.n) : AffineBuildingSLV.Line C

The $j$-th coordinate line $k \cdot e_j$ in $k^n$, packaged as a Line.

theorem AffineBuildingSLVStrong.sum_std_basis_apply (C : DVRContext) (coeffs : Fin C.n → C.k) (i : Fin C.n) : ∑ j : Fin C.n, coeffs j * stdBasisVec C j i = coeffs i

Pointwise evaluation: $(\sum_j c_j e_j)(i) = c_i$.

theorem AffineBuildingSLVStrong.sum_std_basis_eq (C : DVRContext) (coeffs : Fin C.n → C.k) : (fun (i : Fin C.n) => ∑ j : Fin C.n, coeffs j * stdBasisVec C j i) = coeffs

Functional form: $\sum_j c_j e_j = c$ as vectors in $k^n$.

noncomputable def AffineBuildingSLVStrong.stdFrame (C : DVRContext) : AffineBuildingSLV.Frame C

The standard frame in $k^n$ consisting of the coordinate lines $k \cdot e_j$.

@[reducible, inline]

abbrev AffineBuildingSLVStrong.SLV (C : DVRContext) : Type u_1

The special linear group $SL_n(k) = SL_V(k)$ acting on the affine building of type $\tilde A_{n-1}$.

def AffineBuildingSLVStrong.matEntryProj (C : DVRContext) (i j : Fin C.n) : SLV C → C.k

The $(i,j)$-th matrix entry of an element of $SL_n(k)$, as a function $SL_n(k) \to k$.

def AffineBuildingSLVStrong.iwahoriEntryCondition (C : DVRContext) (i j : Fin C.n) : Set C.k

The Iwahori condition on the $(i,j)$-entry: lies in the maximal ideal $\mathfrak{m}$ if $i > j$ (strictly below the diagonal) and in $\mathfrak{o}$ otherwise.

def AffineBuildingSLVStrong.IwahoriSetSLV (C : DVRContext) : Set (SLV C)

The Iwahori subset of $SL_n(k)$: matrices in $SL_n(\mathfrak{o})$ whose reduction modulo $\mathfrak{m}$ is upper-triangular.

structure AffineBuildingSLVStrong.SLVAction (C : DVRContext) : Type u_1

Axiomatic action of $SL_V(k)$ on the Bruhat-Tits building of $SL_V$: a simplicial action together with the induced action on apartments and frames, and sufficient hypotheses to run strong-transitivity arguments (preservation of maximal simplices, frame/apartment compatibility, building chain data and within-apartment chamber transitivity).

• act_simplex : SLV C → AffineBuildingSLV.Simplex C → AffineBuildingSLV.Simplex C
• act_mul (g₁ g₂ : SLV C) (σ : AffineBuildingSLV.Simplex C) : self.act_simplex (g₁ * g₂) σ = self.act_simplex g₁ (self.act_simplex g₂ σ)
• act_one (σ : AffineBuildingSLV.Simplex C) : self.act_simplex 1 σ = σ
• act_apartment : SLV C → Set (AffineBuildingSLV.Simplex C) → Set (AffineBuildingSLV.Simplex C)
• act_apartment_eq (g : SLV C) (A : Set (AffineBuildingSLV.Simplex C)) : self.act_apartment g A = self.act_simplex g '' A
• act_preserves_maximal (g : SLV C) (σ : AffineBuildingSLV.Simplex C) : AffineBuildingSLV.Simplex.IsMaximal C σ → AffineBuildingSLV.Simplex.IsMaximal C (self.act_simplex g σ)
• act_frame : SLV C → AffineBuildingSLV.Frame C → AffineBuildingSLV.Frame C
• act_apartment_frame_compat (g : SLV C) (F : AffineBuildingSLV.Frame C) : self.act_apartment g (AffineBuildingSLV.Apartment C F) = AffineBuildingSLV.Apartment C (self.act_frame g F)
• act_apartment_surj (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) : (∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) → ∀ (A' A₀ : Set (AffineBuildingSLV.Simplex C)), A' ∈ max_apts → A₀ ∈ max_apts → ∀ (g : SLV C), (∀ x ∈ A', self.act_simplex g x ∈ A₀) → (fun (x : AffineBuildingSLV.Simplex C) => self.act_simplex g x) '' A' = A₀
• act_building_chain_data (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) : (∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) → ∀ (B : Subgroup (SLV C)), ∀ A₀ ∈ max_apts, ∀ C₀ ⊆ A₀, ↑B = pointwiseFixer self.act_simplex C₀ → ∀ A' ∈ max_apts, C₀ ⊆ A' ∧ ∃ (enum : ℕ → AffineBuildingSLV.Simplex C), (∀ σ ∈ A', ∃ (n : ℕ), enum n = σ) ∧ (∀ (n : ℕ), enum n ∈ A') ∧ ∀ (Y : Set (AffineBuildingSLV.Simplex C)), C₀ ⊆ Y → Y ⊆ A' → ∃ (A_i : Set (AffineBuildingSLV.Simplex C)) (b_i : SLV C), Y ⊆ A_i ∧ b_i ∈ B ∧ ∀ x ∈ A_i, self.act_simplex b_i x ∈ A₀
• act_frame_chamber_trans (F : AffineBuildingSLV.Frame C) (C₁ C₂ : AffineBuildingSLV.Simplex C) : AffineBuildingSLV.Simplex.IsMaximal C C₁ → AffineBuildingSLV.Simplex.IsMaximal C C₂ → C₁ ∈ AffineBuildingSLV.Apartment C F → C₂ ∈ AffineBuildingSLV.Apartment C F → ∃ (g : SLV C), self.act_simplex g C₁ = C₂ ∧ self.act_apartment g (AffineBuildingSLV.Apartment C F) = AffineBuildingSLV.Apartment C F

def AffineBuildingSLVStrong.IsStronglyTransitive (C : DVRContext) (α : SLVAction C) (𝒜 : Set (Set (AffineBuildingSLV.Simplex C))) : Prop

An $SL_V$-action on the building is strongly transitive with respect to an apartment system $\mathcal A$ if for any two flagged pairs $(C_1, A_1)$ and $(C_2, A_2)$ (maximal simplex in an apartment) some $g$ carries the first to the second.

theorem AffineBuildingSLVStrong.iwahori_is_open_in_SLV (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) [htg : IsTopologicalGroup (SLV C)] (hB_iwahori : ↑B = IwahoriSetSLV C) (h_entry_cont : ∀ (i j : Fin C.n), Continuous (matEntryProj C i j)) (h_valring_open : IsOpen {x : C.k | C.isInO x}) (h_maxideal_open : IsOpen {x : C.k | C.isInMaxIdeal x}) : IsOpen ↑B

The Iwahori subgroup is open in $SL_n(k)$: it is the intersection over finitely many entries of preimages of open sets ($\mathfrak{o}$ or $\mathfrak{m}$) under continuous entry projections.

theorem AffineBuildingSLVStrong.iwahori_is_closed_in_SLV (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) [htg : IsTopologicalGroup (SLV C)] (hB_open : IsOpen ↑B) : IsClosed ↑B

The Iwahori subgroup is closed in $SL_n(k)$: any open subgroup of a topological group is automatically closed.

theorem AffineBuildingSLVStrong.iwahori_is_compact_in_SLV (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) [htg : IsTopologicalGroup (SLV C)] (hB_closed : IsClosed ↑B) (hB_in_compact : ∃ (K : Set (SLV C)), IsCompact K ∧ ↑B ⊆ K) : IsCompact ↑B

The Iwahori subgroup is compact in $SL_n(k)$, since a closed subset of a compact set in a topological group is compact.

noncomputable def AffineBuildingSLVStrong.imageSubring (C : DVRContext) : Subring C.k

The image of the valuation ring embedding $\mathfrak{o} \hookrightarrow k$ as a subring of $k$.

theorem AffineBuildingSLVStrong.mem_imageSubring_iff (C : DVRContext) (x : C.k) : x ∈ imageSubring C ↔ C.isInO x

An element of $k$ lies in the image of $\mathfrak{o}$ iff it is integral.

theorem AffineBuildingSLVStrong.isInMaxIdeal_add' (C : DVRContext) {x y : C.k} (hx : C.isInMaxIdeal x) (hy : C.isInMaxIdeal y) : C.isInMaxIdeal (x + y)

The maximal ideal $\mathfrak{m}$ is closed under addition.

theorem AffineBuildingSLVStrong.isInO_mul_isInMaxIdeal' (C : DVRContext) {x y : C.k} (hx : C.isInO x) (hy : C.isInMaxIdeal y) : C.isInMaxIdeal (x * y)

The maximal ideal $\mathfrak{m}$ absorbs multiplication by $\mathfrak{o}$ on the left: $\mathfrak{o} \cdot \mathfrak{m} \subseteq \mathfrak{m}$.

theorem AffineBuildingSLVStrong.isInMaxIdeal_mul_isInO' (C : DVRContext) {x y : C.k} (hx : C.isInMaxIdeal x) (hy : C.isInO y) : C.isInMaxIdeal (x * y)

The maximal ideal $\mathfrak{m}$ absorbs multiplication by $\mathfrak{o}$ on the right: $\mathfrak{m} \cdot \mathfrak{o} \subseteq \mathfrak{m}$.

theorem AffineBuildingSLVStrong.isInMaxIdeal_zero' (C : DVRContext) : C.isInMaxIdeal 0

Zero lies in $\mathfrak{m}$.

theorem AffineBuildingSLVStrong.isInO_one' (C : DVRContext) : C.isInO 1

One is integral.

theorem AffineBuildingSLVStrong.isInO_zero' (C : DVRContext) : C.isInO 0

Zero is integral.

theorem AffineBuildingSLVStrong.isInO_neg' (C : DVRContext) {x : C.k} (hx : C.isInO x) : C.isInO (-x)

The negation of an integral element is integral.

theorem AffineBuildingSLVStrong.isInO_finset_sum (C : DVRContext) {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ x ∈ s, C.isInO (f x)) : C.isInO (∑ x ∈ s, f x)

A finite sum of integral elements is integral.

theorem AffineBuildingSLVStrong.isInMaxIdeal_finset_sum (C : DVRContext) {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ x ∈ s, C.isInMaxIdeal (f x)) : C.isInMaxIdeal (∑ x ∈ s, f x)

A finite sum of elements in $\mathfrak{m}$ is in $\mathfrak{m}$.

theorem AffineBuildingSLVStrong.isInO_finset_prod (C : DVRContext) {ι : Type u_1} {s : Finset ι} {f : ι → C.k} (hf : ∀ x ∈ s, C.isInO (f x)) : C.isInO (∏ x ∈ s, f x)

A finite product of integral elements is integral.

theorem AffineBuildingSLVStrong.mem_IwahoriSetSLV_iff (C : DVRContext) (g : SLV C) : g ∈ IwahoriSetSLV C ↔ ∀ (i j : Fin C.n), ↑g i j ∈ iwahoriEntryCondition C i j

Membership in the Iwahori set unwound entrywise.

theorem AffineBuildingSLVStrong.iwahori_entry_isInO (C : DVRContext) [IsDiscreteValuationRing C.𝔬] {g : SLV C} (hg : g ∈ IwahoriSetSLV C) (i j : Fin C.n) : C.isInO (↑g i j)

Every entry of an Iwahori matrix is integral, since each entry is either in $\mathfrak{m} \subseteq \mathfrak{o}$ or directly in $\mathfrak{o}$.

theorem AffineBuildingSLVStrong.iwahori_entry_below (C : DVRContext) [IsDiscreteValuationRing C.𝔬] {g : SLV C} (hg : g ∈ IwahoriSetSLV C) {i j : Fin C.n} (hij : ↑i > ↑j) : C.isInMaxIdeal (↑g i j)

The subdiagonal entries of an Iwahori matrix lie in the maximal ideal $\mathfrak{m}$.

theorem AffineBuildingSLVStrong.sign_isInO (C : DVRContext) (σ : Equiv.Perm (Fin C.n)) : C.isInO ↑↑(Equiv.Perm.sign σ)

The sign of any permutation, viewed in $k$, is integral.

theorem AffineBuildingSLVStrong.isInO_smul_of_isInO (C : DVRContext) (z : ℤ) {x : C.k} (hz : C.isInO ↑z) (hx : C.isInO x) : C.isInO (z • x)

An integer scalar multiple of an integral element is integral.

theorem AffineBuildingSLVStrong.isInO_det (C : DVRContext) {M : Matrix (Fin C.n) (Fin C.n) C.k} (hM : ∀ (i j : Fin C.n), C.isInO (M i j)) : C.isInO M.det

If every entry of $M$ is integral then $\det M$ is integral.

theorem AffineBuildingSLVStrong.perm_has_ascent {n : ℕ} {σ : Equiv.Perm (Fin n)} {i : Fin n} (hi : ↑(σ i) < ↑i) : ∃ (l : Fin n), l ≠ i ∧ ↑(σ l) > ↑l

Combinatorial fact: if a permutation strictly decreases some index $i$ ($\sigma(i) < i$), then somewhere else it must strictly increase.

theorem AffineBuildingSLVStrong.updateRow_isInO (C : DVRContext) [IsDiscreteValuationRing C.𝔬] {g : SLV C} (hg : g ∈ IwahoriSetSLV C) (i j l m : Fin C.n) : C.isInO ((↑g).updateRow j (Pi.single i 1) l m)

Replacing the $j$-th row of an Iwahori matrix by the standard basis vector $e_i$ still gives a matrix with all entries integral.

theorem AffineBuildingSLVStrong.adjugate_isInO (C : DVRContext) [IsDiscreteValuationRing C.𝔬] {g : SLV C} (hg : g ∈ IwahoriSetSLV C) (i j : Fin C.n) : C.isInO ((↑g).adjugate i j)

Every entry of the adjugate of an Iwahori matrix is integral.

theorem AffineBuildingSLVStrong.adjugate_below_isInMaxIdeal (C : DVRContext) [IsDiscreteValuationRing C.𝔬] {g : SLV C} (hg : g ∈ IwahoriSetSLV C) {i j : Fin C.n} (hij : ↑i > ↑j) : C.isInMaxIdeal ((↑g).adjugate i j)

The strictly-below-diagonal entries of the adjugate of an Iwahori matrix lie in $\mathfrak{m}$, the key step in showing the Iwahori set is closed under inversion.

theorem AffineBuildingSLVStrong.iwahori_set_is_subgroup (C : DVRContext) [IsDiscreteValuationRing C.𝔬] : ∃ (B : Subgroup (SLV C)), ↑B = IwahoriSetSLV C

The Iwahori set is a subgroup of $SL_n(k)$: it contains the identity and is closed under multiplication and inversion. The inversion step uses the formula $g^{-1} = \mathrm{adj}(g)/\det g$ and the adjugate bounds above.

theorem AffineBuildingSLVStrong.valuation_ring_is_open (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] : IsOpen {x : C.k | C.isInO x}

The valuation ring $\mathfrak{o}$ is open in $k$ under the topological assumptions.

theorem AffineBuildingSLVStrong.maximal_ideal_is_open (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] : IsOpen {x : C.k | C.isInMaxIdeal x}

The maximal ideal $\mathfrak{m}$ is open in $k$ under the topological assumptions.

theorem AffineBuildingSLVStrong.iwahori_in_compact_set (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (B : Subgroup (SLV C)) (hB_iwahori : ↑B = IwahoriSetSLV C) : ∃ (K : Set (SLV C)), IsCompact K ∧ ↑B ⊆ K

The Iwahori subgroup lies inside the compact set of matrices with all entries in $\mathfrak{o}$, namely $SL_n(k) \cap M_n(\mathfrak{o})$.

theorem AffineBuildingSLVStrong.iwahori_is_compact_open (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) : ∃ (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) (_ : IsTopologicalGroup (SLV C)), IsCompact ↑B ∧ IsOpen ↑B

The Iwahori subgroup of $SL_n(k)$ is compact-open in the natural topology on $SL_n(k)$. This is the crucial ingredient for applying strong-transitivity methods to the Bruhat-Tits building.

theorem AffineBuildingSLVStrong.finite_subcomplex_chamber_decomposition (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (α : SLVAction C) (C₀ Y : Set (AffineBuildingSLV.Simplex C)) (hC₀_sub : C₀ ⊆ Y) (hC₀_ne : C₀.Nonempty) (B : Subgroup (SLV C)) (hB_eq : ↑B = pointwiseFixer α.act_simplex C₀) : ∃ (n : ℕ) (_ : 0 < n) (chambers : Fin n → Set (AffineBuildingSLV.Simplex C)) (h_conj : Fin n → SLV C), Y = ⋃ (i : Fin n), chambers i ∧ ∀ (i : Fin n), chambers i = α.act_simplex (h_conj i) '' C₀

Finite subcomplex decomposition: any subcomplex $Y$ of the building that contains the fundamental chamber $C_0$ can be written as a finite union of chambers, each obtained as a $G$-translate of $C_0$.

theorem AffineBuildingSLVStrong.pointwise_fixer_of_fund_alcove_sub_iwahori (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (α : SLVAction C) (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) [IsTopologicalGroup (SLV C)] (hB_compact : IsCompact ↑B) (hB_open : IsOpen ↑B) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀ : A₀ ∈ max_apts) : pointwiseFixer α.act_simplex {σ : AffineBuildingSLV.Simplex C | σ ∈ A₀ ∧ ∀ g ∈ B, α.act_simplex g σ = σ} ⊆ ↑B

The pointwise stabiliser of the fundamental alcove (the subset of $A_0$ fixed by all of $B$) is contained in the Iwahori subgroup $B$.

theorem AffineBuildingSLVStrong.fund_alcove_nonempty (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (α : SLVAction C) (C₀ A₀ : Set (AffineBuildingSLV.Simplex C)) (hC₀_sub : C₀ ⊆ A₀) (B : Subgroup (SLV C)) (hB_eq : ↑B = pointwiseFixer α.act_simplex C₀) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (hA₀ : A₀ ∈ max_apts) : C₀.Nonempty

The fundamental alcove $C_0$ is nonempty: there is at least one simplex in $A_0$ that is fixed by every element of the Iwahori subgroup.

theorem AffineBuildingSLVStrong.slv_building_data_for_thm_17_7 (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (α : SLVAction C) (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) [htg : IsTopologicalGroup (SLV C)] (hB_compact : IsCompact ↑B) (hB_open : IsOpen ↑B) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀ : A₀ ∈ max_apts) : ∃ (C₀ : Set (AffineBuildingSLV.Simplex C)) (_ : C₀ ⊆ A₀) (_ : ↑B = pointwiseFixer α.act_simplex C₀), ∀ A' ∈ max_apts, ∃ (_ : C₀ ⊆ A') (Y : ℕ → Set (AffineBuildingSLV.Simplex C)) (_ : ∀ (i : ℕ), Y i ⊆ Y (i + 1)) (_ : C₀ ⊆ Y 0) (_ : A' = ⋃ (i : ℕ), Y i) (A_chain : ℕ → Set (AffineBuildingSLV.Simplex C)) (_ : ∀ (i : ℕ), Y i ⊆ A_chain i) (b : ℕ → SLV C) (_ : ∀ (i : ℕ), b i ∈ B) (_ : ∀ (i : ℕ), ∀ x ∈ A_chain i, α.act_simplex (b i) x ∈ A₀) (_ : ∀ (i j : ℕ), i ≤ j → Y i ⊆ A_chain j) (_ : ∀ (i : ℕ), IsOpen (pointwiseFixer α.act_simplex (Y i))) (_ : ∀ (g : SLV C), (∀ x ∈ A', α.act_simplex g x ∈ A₀) → (fun (x : AffineBuildingSLV.Simplex C) => α.act_simplex g x) '' A' = A₀), True

Packaging step for Theorem 17.7: from an $SL_V$-action, a compact-open Iwahori $B$, and a maximal apartment system, produce the fundamental alcove $C_0$, the exhaustion $(Y_i)$ of every apartment $A'$, a $B$-conjugacy chain $(A_i, b_i)$ taking each $Y_i$ inside $A_0$, openness of the pointwise fixers, and apartment-mapping surjectivity.

theorem AffineBuildingSLVStrong.frame_chamber_transitivity (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (α : SLVAction C) (F : AffineBuildingSLV.Frame C) (C₁ C₂ : AffineBuildingSLV.Simplex C) (hC₁_max : AffineBuildingSLV.Simplex.IsMaximal C C₁) (hC₂_max : AffineBuildingSLV.Simplex.IsMaximal C C₂) (hC₁ : C₁ ∈ AffineBuildingSLV.Apartment C F) (hC₂ : C₂ ∈ AffineBuildingSLV.Apartment C F) : ∃ (g : SLV C), α.act_simplex g C₁ = C₂ ∧ α.act_apartment g (AffineBuildingSLV.Apartment C F) = AffineBuildingSLV.Apartment C F

Within an apartment $A_F$ coming from a frame $F$, the group $SL_V(k)$ acts transitively on (maximal-chamber, $A_F$) pairs, preserving the apartment.

theorem AffineBuildingSLVStrong.apartment_transitivity_on_max_apts (C : DVRContext) [TopologicalSpace C.k] [hDVR : IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) [hk_lc : LocallyCompactSpace C.k] (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀ : A₀ ∈ max_apts) (A' : Set (AffineBuildingSLV.Simplex C)) : A' ∈ max_apts → ∃ (g : SLV C), α.act_apartment g A' = A₀

$SL_V(k)$ acts transitively on the maximal apartment system: every apartment in the system can be sent to the reference apartment $A_0$ by some element of $SL_V(k)$.

theorem AffineBuildingSLVStrong.act_apartment_one (C : DVRContext) (α : SLVAction C) (A : Set (AffineBuildingSLV.Simplex C)) : α.act_apartment 1 A = A

The identity element acts trivially on apartments.

theorem AffineBuildingSLVStrong.act_apartment_mul (C : DVRContext) (α : SLVAction C) (g₁ g₂ : SLV C) (A : Set (AffineBuildingSLV.Simplex C)) : α.act_apartment (g₁ * g₂) A = α.act_apartment g₁ (α.act_apartment g₂ A)

The action on apartments respects group multiplication.

theorem AffineBuildingSLVStrong.max_apts_to_frames (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (A : Set (AffineBuildingSLV.Simplex C)) : A ∈ max_apts → ∃ (F : AffineBuildingSLV.Frame C), A = AffineBuildingSLV.Apartment C F

Every apartment in a maximal apartment system comes from a frame: $A = A_F$ for some frame $F$ of $V$. This follows from frame-apartment transitivity of $SL_V$.

theorem AffineBuildingSLVStrong.chamber_transitivity_within_apartment (C : DVRContext) [TopologicalSpace C.k] [LocallyCompactSpace C.k] [IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (C₁ C₂ : AffineBuildingSLV.Simplex C) (A : Set (AffineBuildingSLV.Simplex C)) : AffineBuildingSLV.Simplex.IsMaximal C C₁ → AffineBuildingSLV.Simplex.IsMaximal C C₂ → A ∈ max_apts → C₁ ∈ A → C₂ ∈ A → ∃ (g : SLV C), α.act_simplex g C₁ = C₂ ∧ α.act_apartment g A = A

Chamber transitivity within any maximal apartment: for any two maximal chambers in any apartment of the system, some $g \in SL_V$ takes the first to the second while fixing the apartment setwise.

theorem AffineBuildingSLVStrong.strong_transitivity_from_apt_and_chamber_transit (C : DVRContext) [TopologicalSpace C.k] [hDVR : IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) [hk_lc : LocallyCompactSpace C.k] (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (apt_transit : ∀ (A₁ A₂ : Set (AffineBuildingSLV.Simplex C)), A₁ ∈ max_apts → A₂ ∈ max_apts → ∃ (g : SLV C), α.act_apartment g A₁ = A₂) (chamber_transit : ∀ (C₁ C₂ : AffineBuildingSLV.Simplex C) (A : Set (AffineBuildingSLV.Simplex C)), AffineBuildingSLV.Simplex.IsMaximal C C₁ → AffineBuildingSLV.Simplex.IsMaximal C C₂ → A ∈ max_apts → C₁ ∈ A → C₂ ∈ A → ∃ (g : SLV C), α.act_simplex g C₁ = C₂ ∧ α.act_apartment g A = A) : IsStronglyTransitive C α max_apts

Strong transitivity follows formally from apartment-transitivity together with chamber-transitivity within each apartment: any flagged pair $(C_1, A_1)$ can be moved to any other $(C_2, A_2)$.

theorem AffineBuildingSLVStrong.slv_strongly_transitive_maximal_apartment_system (C : DVRContext) [TopologicalSpace C.k] [hDVR : IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) [hk_lc : LocallyCompactSpace C.k] (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀ : A₀ ∈ max_apts) : IsStronglyTransitive C α max_apts

Main strong-transitivity theorem for $SL_V$: the action of $SL_V(k)$ on the Bruhat-Tits building of type $\tilde A_{n-1}$ over a complete DVR is strongly transitive on every maximal apartment system.

theorem AffineBuildingSLVStrong.constructed_apartment_system_is_maximal_of_stable_and_transitive {C : DVRContext} {G : Type u_1} [Group G] [TopologicalSpace G] (act : G → Set (AffineBuildingSLV.Simplex C) → Set (AffineBuildingSLV.Simplex C)) (hact_mul : ∀ (g₁ g₂ : G) (A : Set (AffineBuildingSLV.Simplex C)), act (g₁ * g₂) A = act g₁ (act g₂ A)) (hact_one : ∀ (A : Set (AffineBuildingSLV.Simplex C)), act 1 A = A) (𝒜 max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀_in_𝒜 : A₀ ∈ 𝒜) (hA₀_in_max : A₀ ∈ max_apts) (h𝒜_stable : ∀ (g : G), ∀ A ∈ 𝒜, act g A ∈ 𝒜) (h𝒜_sub_max : 𝒜 ⊆ max_apts) (strong_transit_max : ∀ A' ∈ max_apts, ∃ (g : G), act g A' = A₀) : 𝒜 = max_apts

Abstract lemma: if a $G$-stable apartment system $\mathcal{A} \subseteq \mathrm{max\_apts}$ contains some apartment $A_0$ that the $G$-action sends to every maximal apartment, then $\mathcal{A} = \mathrm{max\_apts}$.

theorem AffineBuildingSLVStrong.maximal_apt_system_slv_helper (C : DVRContext) (α : SLVAction C) (𝒜 max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (A₀ : Set (AffineBuildingSLV.Simplex C)) (hA₀_in_𝒜 : A₀ ∈ 𝒜) (hA₀_in_max : A₀ ∈ max_apts) (h𝒜_stable : ∀ (g : SLV C), ∀ A ∈ 𝒜, α.act_apartment g A ∈ 𝒜) (h𝒜_sub_max : 𝒜 ⊆ max_apts) (strong_transit_max : ∀ A' ∈ max_apts, ∃ (g : SLV C), α.act_apartment g A' = A₀) : 𝒜 = max_apts

Specialisation of the abstract maximality lemma to the $SL_V$ apartment action: a stable, contained apartment system that intersects every $SL_V$-orbit of $A_0$ in the maximal system actually equals the maximal system.

def AffineBuildingSLVStrong.frameApartmentSystem (C : DVRContext) : Set (Set (AffineBuildingSLV.Simplex C))

The canonical apartment system: apartments $A_F$ indexed by frames $F$ of $V$. This is the maximal apartment system for the Bruhat-Tits building of $SL_V$.

def AffineBuildingSLVStrong.IsApartmentSystem (C : DVRContext) (sys : Set (Set (AffineBuildingSLV.Simplex C))) : Prop

A family of apartments is an apartment system if every member arises from a frame and any two simplices lie together in some apartment of the system.

def AffineBuildingSLVStrong.IsMaximalApartmentSystem (C : DVRContext) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) : Prop

An apartment system is maximal if it is an apartment system and contains every other apartment system.

theorem AffineBuildingSLVStrong.frame_apartment_mem_frameApartmentSystem (C : DVRContext) (F : AffineBuildingSLV.Frame C) : AffineBuildingSLV.Apartment C F ∈ frameApartmentSystem C

Each frame apartment $A_F$ is a member of the frame apartment system.

theorem AffineBuildingSLVStrong.frame_apartment_system_stable (C : DVRContext) [TopologicalSpace C.k] [IsDiscreteValuationRing C.𝔬] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) [LocallyCompactSpace C.k] (α : SLVAction C) (g : SLV C) (A : Set (AffineBuildingSLV.Simplex C)) : A ∈ frameApartmentSystem C → α.act_apartment g A ∈ frameApartmentSystem C

The frame apartment system is $SL_V$-stable: the translate of any frame apartment $A_F$ by $g \in SL_V$ is again a frame apartment, namely $A_{gF}$.

theorem AffineBuildingSLVStrong.frame_apartment_system_sub_maximal (C : DVRContext) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) : frameApartmentSystem C ⊆ max_apts

The frame apartment system is contained in any apartment system that contains all frame apartments.

theorem AffineBuildingSLVStrong.constructed_apartment_system_is_maximal (C : DVRContext) [TopologicalSpace C.k] [hDVR : IsDiscreteValuationRing C.𝔬] [DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) [hk_lc : LocallyCompactSpace C.k] (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (hmax : IsMaximalApartmentSystem C max_apts) : frameApartmentSystem C = max_apts

The frame apartment system equals every maximal apartment system: the canonical $SL_V$-system of frame apartments is automatically maximal.

theorem AffineBuildingSLVStrong.iwahori_maximal_apartment_chain (C : DVRContext) [TopologicalSpace C.k] [hk_lc : LocallyCompactSpace C.k] [hDVR : IsDiscreteValuationRing C.𝔬] [hta : DVRTopologicalAssumptions C] (ho_complete : IsAdicComplete C.maxIdeal C.𝔬) (α : SLVAction C) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (hmax : IsMaximalApartmentSystem C max_apts) : ∃ (B : Subgroup (SLV C)) (τ : TopologicalSpace (SLV C)) (_ : IsTopologicalGroup (SLV C)), IsOpen ↑B ∧ IsClosed ↑B ∧ IsCompact ↑B ∧ ∃ (max_apts' : Set (Set (AffineBuildingSLV.Simplex C))), (∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts') ∧ ∀ (σ τ' : AffineBuildingSLV.Simplex C), AffineBuildingSLV.Simplex.IsMaximal C σ → AffineBuildingSLV.Simplex.IsMaximal C τ' → ∃ A ∈ max_apts', σ ∈ A ∧ τ' ∈ A

Combined result: the Iwahori subgroup is open, closed, and compact, and the building of $SL_V$ over a complete DVR has a maximal apartment system in which any two maximal simplices lie in some common apartment.

theorem AffineBuildingSLVStrong.strong_transitivity_from_compact_open_iwahori (C : DVRContext) [TopologicalSpace (Fin C.n → Fin C.n → C.𝔬)] (_hB_open : IsOpen (AffineBuildingSLVAxioms.IwahoriSubgroup C)) (_hB_compact : IsCompact (AffineBuildingSLVAxioms.IwahoriSubgroup C)) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (hmax : IsMaximalApartmentSystem C max_apts) : ∃ (max_apts' : Set (Set (AffineBuildingSLV.Simplex C))), (∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts') ∧ ∀ (σ τ : AffineBuildingSLV.Simplex C), AffineBuildingSLV.Simplex.IsMaximal C σ → AffineBuildingSLV.Simplex.IsMaximal C τ → ∃ A ∈ max_apts', σ ∈ A ∧ τ ∈ A

From a compact-open Iwahori subgroup, deduce that the maximal apartment system contains any two maximal simplices in a common apartment (formulation without an explicit topology on $SL_V$).

theorem AffineBuildingSLVStrong.slv_maximal_apartment_system (C : DVRContext) [TopologicalSpace (Fin C.n → Fin C.n → C.𝔬)] (hB_open : IsOpen (AffineBuildingSLVAxioms.IwahoriSubgroup C)) (hBruhat : ∃ (I : Type u_1) (cells : I → Set (Fin C.n → Fin C.n → C.𝔬)), (∀ (i : I), IsOpen (cells i)) ∧ Set.univ = ⋃ (i : I), cells i ∧ (∀ (i j : I), i ≠ j → Disjoint (cells i) (cells j)) ∧ ∃ (i₀ : I), cells i₀ = AffineBuildingSLVAxioms.IwahoriSubgroup C) (K : Set (Fin C.n → Fin C.n → C.𝔬)) (hBK : AffineBuildingSLVAxioms.IwahoriSubgroup C ⊆ K) (hK : IsCompact K) (max_apts : Set (Set (AffineBuildingSLV.Simplex C))) (hframes : ∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts) (hmax : IsMaximalApartmentSystem C max_apts) : IsClosed (AffineBuildingSLVAxioms.IwahoriSubgroup C) ∧ IsCompact (AffineBuildingSLVAxioms.IwahoriSubgroup C) ∧ ∃ (max_apts' : Set (Set (AffineBuildingSLV.Simplex C))), (∀ (F : AffineBuildingSLV.Frame C), AffineBuildingSLV.Apartment C F ∈ max_apts') ∧ ∀ (σ τ : AffineBuildingSLV.Simplex C), AffineBuildingSLV.Simplex.IsMaximal C σ → AffineBuildingSLV.Simplex.IsMaximal C τ → ∃ A ∈ max_apts', σ ∈ A ∧ τ ∈ A

Final theorem on the maximal apartment system of $SL_V$: given that the Iwahori subgroup is open, the Bruhat decomposition holds, and there is a compact set containing it, the Iwahori is automatically closed and compact, and the building has a maximal apartment system covering any pair of maximal simplices.