structure PeriodicChainAlternating (ctx : AlternatingBuildingContext) : Type

A periodic lattice chain in the alternating-form setting (type $\tilde C_n$): an $\mathbb{Z}$-indexed family of $\mathfrak{o}$-lattices ascending, periodic with period $2n$ up to scaling by $\pi$, with the prescribed isotropy/duality relations under the alternating form.

• chain : ℤ → ctx.C.OLattice
• primitive_at_zero (v : Fin ctx.C.n → ctx.C.k) : v ∈ (self.chain 0).carrier → ∀ w ∈ (self.chain 0).carrier, ctx.C.isInO (ctx.form v w)
• ascending (i : ℤ) : AffineIsometryBuilding.latticeContained ctx.C (self.chain i) (self.chain (i + 1))
• periodic (i : ℤ) (v : Fin ctx.C.n → ctx.C.k) : v ∈ (self.chain (i + 2 * ↑ctx.wittIndex)).carrier → ctx.C.oscal ctx.C.uniformizer v ∈ (self.chain i).carrier
• duality (j : ℕ) : 1 ≤ j → j ≤ ctx.wittIndex - 1 → ∀ v ∈ (self.chain (↑ctx.wittIndex + ↑j)).carrier, ∀ w ∈ (self.chain (↑ctx.wittIndex - ↑j)).carrier, ctx.C.isInMaxIdeal (ctx.form v w)
• flag_isotropic (i : ℕ) : 1 ≤ i → i ≤ ctx.wittIndex → AffineIsometryBuilding.formValuesInMaxIdeal ctx.C ctx.form (self.chain ↑i)

structure PeriodicChainDoubleOriflamme (ctx : DoubleOriflammeContext) : Type

A periodic lattice chain for the double oriflamme building (type $\tilde D_n$): two unimodular lattices at level $0$ and at the top level $N$, with intermediate lattices in between.

• lat0_1 : ctx.C.OLattice
• lat0_2 : ctx.C.OLattice
• latN_1 : ctx.C.OLattice
• latN_2 : ctx.C.OLattice
• chain_mid (i : ℕ) : 2 ≤ i → i ≤ ctx.halfDim - 2 → ctx.C.OLattice
• prim0_1 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_1.carrier → ∀ w ∈ self.lat0_1.carrier, ctx.C.isInO (ctx.form v w)
• prim0_2 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_2.carrier → ∀ w ∈ self.lat0_2.carrier, ctx.C.isInO (ctx.form v w)
• contain_01 (i : ℕ) (h1 : 2 ≤ i) (h2 : i ≤ ctx.halfDim - 2) : AffineIsometryBuilding.latticeContained ctx.C self.lat0_1 (self.chain_mid i h1 h2)
• contain_02 (i : ℕ) (h1 : 2 ≤ i) (h2 : i ≤ ctx.halfDim - 2) : AffineIsometryBuilding.latticeContained ctx.C self.lat0_2 (self.chain_mid i h1 h2)
• lat0_distinct : self.lat0_1.carrier ≠ self.lat0_2.carrier
• latN_distinct : self.latN_1.carrier ≠ self.latN_2.carrier

structure PeriodicChainSingleOriflamme (ctx : SingleOriflammeContext) : Type

A periodic lattice chain for the single oriflamme building (type $\tilde B_n$): two unimodular lattices at level $0$ and a chain of intermediate lattices indexed by $2 \le i \le n$.

• lat0_1 : ctx.C.OLattice
• lat0_2 : ctx.C.OLattice
• chain (i : ℕ) : 2 ≤ i → i ≤ ctx.wittIndex → ctx.C.OLattice
• prim0_1 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_1.carrier → ∀ w ∈ self.lat0_1.carrier, ctx.C.isInO (ctx.form v w)
• prim0_2 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_2.carrier → ∀ w ∈ self.lat0_2.carrier, ctx.C.isInO (ctx.form v w)
• contain_01 (i : ℕ) (h1 : 2 ≤ i) (h2 : i ≤ ctx.wittIndex) : AffineIsometryBuilding.latticeContained ctx.C self.lat0_1 (self.chain i h1 h2)
• lat0_distinct : self.lat0_1.carrier ≠ self.lat0_2.carrier

structure MaxSimplexAlternating (ctx : AlternatingBuildingContext) : Type

A maximal simplex (chamber) of the alternating-form building: an $(n+1)$-tuple of $\mathfrak{o}$-lattices with $\Lambda_0$ primitive (form integral) and each $\Lambda_i$ contained in $\Lambda_0$ but with prescribed scaling and isotropy properties.

• lats : Fin (ctx.wittIndex + 1) → ctx.C.OLattice
• prim (v : Fin ctx.C.n → ctx.C.k) : v ∈ (self.lats 0).carrier → ∀ w ∈ (self.lats 0).carrier, ctx.C.isInO (ctx.form v w)
• contain (i : Fin (ctx.wittIndex + 1)) : 0 < ↑i → AffineIsometryBuilding.latticeContained ctx.C (self.lats 0) (self.lats i)
• scale_contain (i : Fin (ctx.wittIndex + 1)) : 0 < ↑i → ∀ v ∈ (self.lats i).carrier, ctx.C.oscal ctx.C.uniformizer v ∈ (self.lats 0).carrier
• iso (i : Fin (ctx.wittIndex + 1)) : 0 < ↑i → AffineIsometryBuilding.formValuesInMaxIdeal ctx.C ctx.form (self.lats i)

structure MaxSimplexDoubleOriflamme (ctx : DoubleOriflammeContext) : Type

A maximal simplex in the double oriflamme building, consisting of a pair of primitive lattices at level $0$, intermediate lattices for $2 \le i \le N-2$, and a pair of top-level lattices.

• lat0_1 : ctx.C.OLattice
• lat0_2 : ctx.C.OLattice
• lat_mid (i : ℕ) : 2 ≤ i → i ≤ ctx.halfDim - 2 → ctx.C.OLattice
• latN_1 : ctx.C.OLattice
• latN_2 : ctx.C.OLattice
• prim_1 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_1.carrier → ∀ w ∈ self.lat0_1.carrier, ctx.C.isInO (ctx.form v w)
• prim_2 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_2.carrier → ∀ w ∈ self.lat0_2.carrier, ctx.C.isInO (ctx.form v w)

structure MaxSimplexSingleOriflamme (ctx : SingleOriflammeContext) : Type

A maximal simplex in the single oriflamme building: a pair of primitive lattices $\Lambda_0^{(1)}, \Lambda_0^{(2)}$ at level $0$ together with the remainder of the lattice chain.

• lat0_1 : ctx.C.OLattice
• lat0_2 : ctx.C.OLattice
• lat_rest (i : ℕ) : 2 ≤ i → i ≤ ctx.wittIndex → ctx.C.OLattice
• prim_1 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_1.carrier → ∀ w ∈ self.lat0_1.carrier, ctx.C.isInO (ctx.form v w)
• prim_2 (v : Fin ctx.C.n → ctx.C.k) : v ∈ self.lat0_2.carrier → ∀ w ∈ self.lat0_2.carrier, ctx.C.isInO (ctx.form v w)