structure AffineIsometryBuilding.PrimitiveLatticeAlternating (C : DVRContext) extends C.PrimitiveLattice : Type u_1

A primitive lattice $\Lambda$ over $\mathfrak{o}$ on which the bilinear form $B$ is alternating: $B(v, v) = 0$ for every $v$.

• carrier : Set (Fin C.n → C.k)
• zero_mem : 0 ∈ self.carrier
• add_mem {x y : Fin C.n → C.k} : x ∈ self.carrier → y ∈ self.carrier → x + y ∈ self.carrier
• smul_mem (r : C.𝔬) {x : Fin C.n → C.k} : x ∈ self.carrier → C.oscal r x ∈ self.carrier
• spans_V (v : Fin C.n → C.k) : ∃ (m : ℕ) (cs : Fin m → C.k) (vs : Fin m → Fin C.n → C.k), (∀ (j : Fin m), vs j ∈ self.carrier) ∧ v = ∑ j : Fin m, cs j • vs j
• closed_under_o_combination (coeffs : Fin C.n → C.k) (vectors : Fin C.n → Fin C.n → C.k) : (∀ (i : Fin C.n), C.isInO (coeffs i)) → (∀ (i : Fin C.n), vectors i ∈ self.carrier) → ∑ i : Fin C.n, coeffs i • vectors i ∈ self.carrier
• form : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k
• form_linear_left (r : C.k) (v w : Fin C.n → C.k) : self.form (r • v) w = r * self.form v w
• form_linear_right (r : C.k) (v w : Fin C.n → C.k) : self.form v (r • w) = r * self.form v w
• form_integral {v w : Fin C.n → C.k} : v ∈ self.carrier → w ∈ self.carrier → C.isInO (self.form v w)
• form_nondeg {v : Fin C.n → C.k} : v ∈ self.carrier → (¬∃ w ∈ self.carrier, v = C.oscal C.uniformizer w) → ∃ w ∈ self.carrier, C.isUnitInO (self.form v w)
• form_alternating (v : Fin C.n → C.k) : self.form v v = 0

def AffineIsometryBuilding.dualLattice (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ : C.OLattice) : Set (Fin C.n → C.k)

The dual of an $\mathfrak{o}$-lattice $\Lambda$ with respect to $B$: $\Lambda^\# = \{v : B(v, w) \in \mathfrak{m} \text{ for all } w \in \Lambda\}$.

def AffineIsometryBuilding.latticeContained (C : DVRContext) (Λ₁ Λ₂ : C.OLattice) : Prop

$\Lambda_1 \subseteq \Lambda_2$ as sets of vectors in $k^n$.

def AffineIsometryBuilding.formValuesInMaxIdeal (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ : C.OLattice) : Prop

The bilinear form $B$ takes values in the maximal ideal on $\Lambda$: $B(v, w) \in \mathfrak{m}$ for all $v, w \in \Lambda$.

def AffineIsometryBuilding.IsAffineAlternatingVertex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ : C.OLattice) : Prop

A lattice $\Lambda$ is a vertex of the affine alternating-form building if there exists a sublattice $\Lambda_0 \subseteq \Lambda$ such that $B$ is integral on $\Lambda_0$, takes values in $\mathfrak{m}$ on $\Lambda$, and the uniformizer multiplied by any element of $\Lambda$ lands in $\Lambda_0$ (so $\Lambda / \Lambda_0$ has bounded denominator).

def AffineIsometryBuilding.AffineAlternatingIncidence (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ₁ Λ₂ : C.OLattice) : Prop

Incidence relation for the affine alternating-form building: two lattices $\Lambda_1, \Lambda_2$ are incident if there is a common $\Lambda_0$ on which $B$ is integral, the uniformizer maps either $\Lambda_i$ into $\Lambda_0$, and one of $\Lambda_1, \Lambda_2$ is contained in the other.

structure AffineIsometryBuilding.AffineAlternatingComplex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) : Type u_1

The affine alternating-form building: a simplicial complex of $\mathfrak{o}$-lattices in $k^n$ whose vertices satisfy IsAffineAlternatingVertex, whose simplices are pairwise incident, and whose face set is downward closed under nonempty subsets.

• simplices : Set (Finset C.OLattice)
• vertex_condition (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ ∈ σ, IsAffineAlternatingVertex C B Λ
• pairwise_incident (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ₁ ∈ σ, ∀ Λ₂ ∈ σ, AffineAlternatingIncidence C B Λ₁ Λ₂
• face_closed (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ τ ⊆ σ, τ.Nonempty → τ ∈ self.simplices

structure AffineIsometryBuilding.FrameAlternating (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (m : ℕ) : Type u_1

A symplectic frame for an alternating form $B$: $m$ pairs of isotropic lines indexed by $\mathrm{Fin}\,m \times \mathrm{Bool}$ such that within each pair $(i, \mathrm{true}), (i, \mathrm{false})$ the pairing $B(\ell_{i,\mathrm{true}}, \ell_{i,\mathrm{false}})$ is a unit, and lines with different indices are orthogonal.

• lines : Fin m × Bool → Fin C.n → C.k
• lines_isotropic (ib : Fin m × Bool) : B (self.lines ib) (self.lines ib) = 0
• lines_pairing (i : Fin m) : C.isUnitInO (B (self.lines (i, true)) (self.lines (i, false)))
• lines_orthogonal (i j : Fin m) : i ≠ j → ∀ (s t : Bool), B (self.lines (i, s)) (self.lines (j, t)) = 0

def AffineIsometryBuilding.IsInAlternatingApartment (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (m : ℕ) (F : FrameAlternating C B m) (Λ : C.OLattice) : Prop

A lattice $\Lambda$ lies in the apartment of a symplectic frame $F$ if it admits a description as $\mathfrak{o}$-span of the frame lines scaled by nonzero scalars (one per frame line).

def AffineIsometryBuilding.IsDoubleOriflammeVertex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ : C.OLattice) (_halfDim : ℕ) : Prop

A lattice $\Lambda$ is a vertex of the double oriflamme building (type $\tilde D_n$) of $B$ if it admits a sublattice $\Lambda_0$ satisfying the same containment / integrality / uniformizer conditions as in the alternating case, plus a "doubling" condition certifying that $\Lambda$ is one of the two lattices arising in an oriflamme split.

def AffineIsometryBuilding.DoubleOriflammeIncidence (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ₁ Λ₂ : C.OLattice) : Prop

Incidence relation for the double oriflamme building: either the underlying alternating-form incidence, or an oriflamme incidence where $\Lambda_1, \Lambda_2$ share a common $\Lambda_0$ and differ by a single direction $d \in \Lambda_1 \setminus \Lambda_2$.

structure AffineIsometryBuilding.DoubleOriflammeComplex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (halfDim : ℕ) : Type u_1

The double oriflamme building of $B$ (type $\tilde D_n$): a simplicial complex of $\mathfrak{o}$-lattices whose vertices are IsDoubleOriflammeVertex, simplices are pairwise oriflamme-incident, and faces are closed under nonempty subsets.

• simplices : Set (Finset C.OLattice)
• vertex_condition (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ ∈ σ, IsDoubleOriflammeVertex C B Λ halfDim
• pairwise_incident (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ₁ ∈ σ, ∀ Λ₂ ∈ σ, DoubleOriflammeIncidence C B Λ₁ Λ₂
• face_closed (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ τ ⊆ σ, τ.Nonempty → τ ∈ self.simplices

def AffineIsometryBuilding.IsSingleOriflammeVertex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ : C.OLattice) : Prop

A lattice $\Lambda$ is a vertex of the single oriflamme building (type $\tilde B_n$) of $B$ if there is a superlattice $\Lambda_0 \supseteq \Lambda$ such that the uniformizer maps $\Lambda_0$ into $\Lambda$, $B$ is integral on $\Lambda_0$, every non-divisible element of $\Lambda_0$ has a unit pairing with some other element, and $B$ takes values in $\mathfrak{m}$ on $\Lambda$.

def AffineIsometryBuilding.SingleOriflammeIncidence (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (Λ₁ Λ₂ : C.OLattice) : Prop

Incidence in the single oriflamme building: either the alternating incidence relation, or both lattices are integral for $B$ and differ by exactly one direction $d \in \Lambda_1 \setminus \Lambda_2$.

structure AffineIsometryBuilding.SingleOriflammeComplex (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) : Type u_1

The single oriflamme building of $B$ (type $\tilde B_n$): a simplicial complex of lattices whose vertices are IsSingleOriflammeVertex, simplices are pairwise single-oriflamme incident, and faces are downward closed under nonempty subsets.

• simplices : Set (Finset C.OLattice)
• vertex_condition (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ ∈ σ, IsSingleOriflammeVertex C B Λ
• pairwise_incident (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ Λ₁ ∈ σ, ∀ Λ₂ ∈ σ, SingleOriflammeIncidence C B Λ₁ Λ₂
• face_closed (σ : Finset C.OLattice) : σ ∈ self.simplices → ∀ τ ⊆ σ, τ.Nonempty → τ ∈ self.simplices

def AffineIsometryBuilding.AlternatingIsThickBuilding (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (X : AffineAlternatingComplex C B) : Prop

The alternating-form simplicial complex is a thick building: any two simplices lie in a common apartment described by some symplectic frame, and every panel is contained in at least three distinct chambers.

def AffineIsometryBuilding.DoubleOriflammeIsThickBuilding (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (halfDim : ℕ) (X : DoubleOriflammeComplex C B halfDim) : Prop

Thickness for the double oriflamme building: every panel is contained in at least three pairwise-distinct chambers.

def AffineIsometryBuilding.SingleOriflammeIsThickBuilding (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (X : SingleOriflammeComplex C B) : Prop

Thickness for the single oriflamme building: every panel is contained in at least three pairwise-distinct chambers.

def AffineIsometryBuilding.IsIsometry (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (g : GL (Fin C.n) C.k) : Prop

An element $g \in GL_n(k)$ is an isometry of the bilinear form $B$ if $B(gv, gw) = B(v, w)$ for all $v, w \in k^n$.

def AffineIsometryBuilding.IsometryGroupSet (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) : Set C.GL_n_k

The isometry group of $B$ as a subset of $GL_n(k)$.

def AffineIsometryBuilding.GLImageLatticeCarrier (C : DVRContext) (g : C.GL_n_k) (Λ : C.OLattice) : Set (Fin C.n → C.k)

The image $g \cdot \Lambda$ of a lattice $\Lambda$ under $g \in GL_n(k)$, as a set of vectors.

def AffineIsometryBuilding.GLMapsSimplex (C : DVRContext) (g : C.GL_n_k) (σ₁ σ₂ : Finset C.OLattice) : Prop

$g \in GL_n(k)$ maps simplex $\sigma_1$ to simplex $\sigma_2$ if for every lattice $\Lambda \in \sigma_1$ there is some $\Lambda' \in \sigma_2$ with $g \cdot \Lambda = \Lambda'$ as sets.

def AffineIsometryBuilding.GLMapsAlternatingApartment (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (m : ℕ) (g : C.GL_n_k) (F₁ F₂ : FrameAlternating C B m) : Prop

$g \in GL_n(k)$ maps the apartment of frame $F_1$ to that of $F_2$ if every lattice in the $F_1$-apartment has its $g$-image in the $F_2$-apartment.

def AffineIsometryBuilding.StrongTransitivityAlternating (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (X : AffineAlternatingComplex C B) (m : ℕ) : Prop

Strong transitivity for the alternating-form building: the isometry group acts transitively on pairs (apartment, simplex inside that apartment).

def AffineIsometryBuilding.StrongTransitivityDoubleOriflamme (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (halfDim : ℕ) (X : DoubleOriflammeComplex C B halfDim) : Prop

Strong transitivity for the double oriflamme building: the isometry group acts transitively on simplices of the complex.

def AffineIsometryBuilding.StrongTransitivitySingleOriflamme (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (X : SingleOriflammeComplex C B) : Prop

Strong transitivity for the single oriflamme building: the isometry group acts transitively on simplices of the complex.