def AffineBuildingSLV.IsHomothetic (C : DVRContext) (Λ Λ' : C.OLattice) : Prop

Two $\mathfrak{o}$-lattices $\Lambda, \Lambda'$ in $V = k^n$ are homothetic if $\Lambda' = c \Lambda$ for some $c \in k^\times$.

def AffineBuildingSLV.πLattice (C : DVRContext) (hπ : C.embed C.uniformizer ≠ 0) (Λ : C.OLattice) : C.OLattice

The scaled lattice $\pi \Lambda = \{\pi v : v \in \Lambda\}$ obtained by scaling $\Lambda$ by the uniformizer $\pi$.

theorem AffineBuildingSLV.πLattice_homothetic (C : DVRContext) (hπ : C.embed C.uniformizer ≠ 0) (Λ : C.OLattice) : IsHomothetic C (πLattice C hπ Λ) Λ

The scaled lattice $\pi \Lambda$ is homothetic to $\Lambda$ with scaling factor $\pi$.

def AffineBuildingSLV.OLattice.IsIncident (C : DVRContext) (x y : C.OLattice) : Prop

Incidence of $\mathfrak{o}$-lattices: $y \subseteq x$ and $\pi x \subseteq y$. This makes $x/y$ an $\mathfrak{o}/\mathfrak{m}$-vector space, encoding the simplicial relation in the Bruhat-Tits building.

theorem AffineBuildingSLV.OLattice.incident_symm_lattice (C : DVRContext) (hπ : C.embed C.uniformizer ≠ 0) (x y : C.OLattice) (h : IsIncident C x y) : IsIncident C y (πLattice C hπ x)

Symmetry of incidence at the level of lattices (up to scaling by $\pi$): if $x \supseteq y \supseteq \pi x$, then $y \supseteq \pi x \supseteq \pi y$.

def AffineBuildingSLV.IncidenceRel (C : DVRContext) (ξ η : C.HomothetyClass) : Prop

Incidence relation on homothety classes: two classes $[\Lambda], [\Lambda']$ are incident if they are equal or have representatives $x \in [\Lambda]$, $y \in [\Lambda']$ that are incident in the lattice sense.

structure AffineBuildingSLV.Simplex (C : DVRContext) : Type u_1

A simplex of the Bruhat-Tits building of $SL_V$ is a finite set of pairwise incident homothety classes of $\mathfrak{o}$-lattices in $V$.

• vertices : Finset C.HomothetyClass
• mutually_incident (ξ : C.HomothetyClass) : ξ ∈ self.vertices → ∀ η ∈ self.vertices, IncidenceRel C ξ η

structure AffineBuildingSLV.Line (C : DVRContext) : Type u_1

A line in $V = k^n$ is a one-dimensional subspace, represented here by a nonzero generator.

• generator : Fin C.n → C.k
• generator_ne_zero : self.generator ≠ 0

structure AffineBuildingSLV.Frame (C : DVRContext) : Type u_1

A frame in $V = k^n$ is an ordered family of $n$ lines that spans $V$ and is linearly independent: a decomposition $V = L_1 \oplus \cdots \oplus L_n$ into lines.

• lines : Fin C.n → Line C
• spans (v : Fin C.n → C.k) : ∃ (coeffs : Fin C.n → C.k), v = fun (i : Fin C.n) => ∑ j : Fin C.n, coeffs j * (self.lines j).generator i
• independent (coeffs : Fin C.n → C.k) : (fun (i : Fin C.n) => ∑ j : Fin C.n, coeffs j * (self.lines j).generator i) = 0 → ∀ (j : Fin C.n), coeffs j = 0

def AffineBuildingSLV.IsDecomposableWrtFrame (C : DVRContext) (F : Frame C) (Λ : C.OLattice) : Prop

A lattice $\Lambda$ is decomposable with respect to a frame $F = (L_1, \ldots, L_n)$ if $\Lambda = \bigoplus_j s_j \mathfrak{o} v_j$ for some scalars $s_j \in k^\times$ and chosen generators $v_j$ of the lines.

def AffineBuildingSLV.Apartment (C : DVRContext) (F : Frame C) : Set (Simplex C)

The apartment $A_F$ associated to a frame $F$: the set of simplices all of whose vertices are classes of frame-decomposable lattices.

structure AffineBuildingSLV.PeriodicFlag (C : DVRContext) : Type u_1

A periodic flag of $\mathfrak{o}$-lattices: a $\mathbb{Z}$-indexed ascending chain $\cdots \subset \Lambda_i \subset \Lambda_{i+1} \subset \cdots$ in $V = k^n$, periodic with period $n$ up to scaling by $\pi$, with one-dimensional consecutive quotients.

• lattice : ℤ → C.OLattice
• ascending (i : ℤ) : (self.lattice i).carrier ⊆ (self.lattice (i + 1)).carrier
• periodic (i : ℤ) : (self.lattice (i + ↑C.n)).carrier = {v : Fin C.n → C.k | ∃ w ∈ (self.lattice i).carrier, v = C.oscal C.uniformizer w}
• quotient_annihilated (i : ℤ) (v : Fin C.n → C.k) : v ∈ (self.lattice (i + 1)).carrier → C.oscal C.uniformizer v ∈ (self.lattice i).carrier
• quotient_one_dim (i : ℤ) : ∃ w ∈ (self.lattice (i + 1)).carrier, w ∉ (self.lattice i).carrier ∧ ∀ v ∈ (self.lattice (i + 1)).carrier, ∃ (r : C.𝔬), (fun (j : Fin C.n) => v j - C.embed r * w j) ∈ (self.lattice i).carrier

def AffineBuildingSLV.PeriodicFlag.toVertices (C : DVRContext) (pf : PeriodicFlag C) : Fin C.n → C.HomothetyClass

The vertices of a maximal simplex extracted from a periodic flag: take the homothety classes of $\Lambda_0, \ldots, \Lambda_{n-1}$.

def AffineBuildingSLV.Simplex.IsMaximal (C : DVRContext) (σ : Simplex C) : Prop

A simplex is maximal (a chamber) if it has exactly $n$ vertices and cannot be extended: any further vertex fails to be incident to at least one vertex of $\sigma$.

def AffineBuildingSLVAxioms.CoxeterMatrixAffineA (n : ℕ) (i j : ZMod n) : ℕ

The Coxeter matrix of the affine type $\tilde A_{n-1}$ on $\mathbb{Z}/n$ generators: label $1$ on the diagonal, $3$ on edges of the cyclic Dynkin diagram, and $2$ elsewhere.

def AffineBuildingSLVAxioms.IsValidReplacement (C : DVRContext) (pf : AffineBuildingSLV.PeriodicFlag C) (i : Fin C.n) (Λ' : C.OLattice) : Prop

A lattice $\Lambda'$ is a valid replacement for the $i$-th lattice of a periodic flag $\mathit{pf}$ if it lies between $\mathit{pf}_{i-1}$ and $\mathit{pf}_{i+1}$.

def AffineBuildingSLVAxioms.FacetReflection (n : ℕ) (i : Fin n) : Fin n → Fin n

The transposition $(i\ i+1)$ swapping the $i$-th and $(i+1)$-th vertices, representing reflection in the facet opposite vertex $i$ of a chamber.

def AffineBuildingSLVAxioms.VertexLabel (C : DVRContext) (_base Λ : C.OLattice) (inv_factor_sum : ℕ) : ZMod C.n

The vertex label of $\Lambda$ relative to a base lattice: a class in $\mathbb{Z}/n$ encoding the "level" of $\Lambda$ in the lattice chain.

theorem AffineBuildingSLVAxioms.strong_transitivity (C : DVRContext) (common_apt : ∀ (σ τ : AffineBuildingSLV.Simplex C), AffineBuildingSLV.Simplex.IsMaximal C σ → AffineBuildingSLV.Simplex.IsMaximal C τ → ∃ (F : AffineBuildingSLV.Frame C), σ ∈ AffineBuildingSLV.Apartment C F ∧ τ ∈ AffineBuildingSLV.Apartment C F) (apt_iso : ∀ (F₁ F₂ : AffineBuildingSLV.Frame C), ∀ σ ∈ AffineBuildingSLV.Apartment C F₁, σ ∈ AffineBuildingSLV.Apartment C F₂ → ∃ (φ : AffineBuildingSLV.Simplex C → AffineBuildingSLV.Simplex C), (∀ τ ∈ AffineBuildingSLV.Apartment C F₁, φ τ ∈ AffineBuildingSLV.Apartment C F₂) ∧ φ σ = σ) (σ : AffineBuildingSLV.Simplex C) (hσ : AffineBuildingSLV.Simplex.IsMaximal C σ) (F₀ : AffineBuildingSLV.Frame C) (hσF₀ : σ ∈ AffineBuildingSLV.Apartment C F₀) (τ : AffineBuildingSLV.Simplex C) (hτ : AffineBuildingSLV.Simplex.IsMaximal C τ) : ∃ (φ : AffineBuildingSLV.Simplex C → AffineBuildingSLV.Simplex C), φ τ ∈ AffineBuildingSLV.Apartment C F₀ ∧ φ σ = σ

Abstract strong-transitivity statement: given that any two maximal simplices share a common apartment, and that apartment isomorphisms fixing a common chamber can be extended, any chamber $\tau$ can be mapped into the reference apartment $A_{F_0}$ by an isomorphism that fixes a chosen chamber $\sigma$.

def AffineBuildingSLVAxioms.IsUpperTriangularModM (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) : Prop

A matrix over $\mathfrak{o}$ is upper-triangular modulo $\mathfrak{m}$ if every strictly below-diagonal entry is a multiple of the uniformizer $\pi$.

def AffineBuildingSLVAxioms.IsCongruentToIdentityModM (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) : Prop

A matrix over $\mathfrak{o}$ is congruent to the identity modulo $\mathfrak{m}$ if each entry equals the corresponding entry of the identity matrix modulo $\pi$.

def AffineBuildingSLVAxioms.StabilizesStandardFlag (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) (pf : AffineBuildingSLV.PeriodicFlag C) : Prop

A matrix $g$ stabilises the standard periodic flag $(\Lambda_i)_i$ if its linear action preserves each $\Lambda_i$ setwise.

structure AffineBuildingSLVAxioms.IwahoriIdentification (C : DVRContext) (pf : AffineBuildingSLV.PeriodicFlag C) : Prop

The identification of the Iwahori subgroup with the stabiliser of the standard periodic flag: a pair of mutual implications between "upper triangular mod $\pi$" and "stabilises the flag".

• stabilizer_implies_upper_tri (g : Fin C.n → Fin C.n → C.𝔬) : StabilizesStandardFlag C g pf → IsUpperTriangularModM C g
• upper_tri_implies_stabilizer (g : Fin C.n → Fin C.n → C.𝔬) : IsUpperTriangularModM C g → StabilizesStandardFlag C g pf

def AffineBuildingSLVAxioms.IwahoriSubgroup (C : DVRContext) : Set (Fin C.n → Fin C.n → C.𝔬)

The Iwahori subgroup as a subset of $M_n(\mathfrak{o})$: matrices that are upper triangular modulo $\mathfrak{m}$.

theorem AffineBuildingSLVAxioms.congruent_to_identity_is_upper_tri (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) (hg : IsCongruentToIdentityModM C g) : IsUpperTriangularModM C g

A matrix congruent to the identity mod $\mathfrak{m}$ is, in particular, upper-triangular mod $\mathfrak{m}$.

def AffineBuildingSLVAxioms.StandardLatticeCarrier (C : DVRContext) (i : Fin C.n) : Set (Fin C.n → C.k)

The carrier of the $i$-th standard lattice in the standard periodic flag, parametrising vectors whose first $i$ coordinates are in $\pi^{-1} \mathfrak{o}$ and the remaining ones in $\mathfrak{o}$.

theorem AffineBuildingSLVAxioms.open_plus_decomp_implies_closed {α : Type u_1} [TopologicalSpace α] (B : Set α) (_hopen : IsOpen B) (hdecomp : ∃ (I : Type u_2) (cells : I → Set α), (∀ (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₀ = B) : IsClosed B

Abstract topology lemma: a set $B$ that equals one cell of an open-cell partition is closed, since its complement is the open union of the other cells.

theorem AffineBuildingSLVAxioms.closed_in_compact_is_compact {α : Type u_1} [TopologicalSpace α] (B K : Set α) (hB_closed : IsClosed B) (hBK : B ⊆ K) (hK_compact : IsCompact K) : IsCompact B

Abstract topology lemma: a closed subset of a compact set is compact.