structure AlternatingBuildingContext : Type 1

Data for the Bruhat-Tits building of type $\tilde C_n$ associated to a non-degenerate alternating bilinear form on a $2n$-dimensional space over a complete DVR $k$. The structure bundles the form, its hyperbolic basis $(e_i, f_i)$, the standard $\mathfrak{o}$-lattice $\Lambda_0$ on which the form is integral and unimodular, and the requisite non-degeneracy hypothesis modulo $\mathfrak{m}$.

• C : DVRContext
• form : (Fin self.C.n → self.C.k) → (Fin self.C.n → self.C.k) → self.C.k
• wittIndex : ℕ
• dim_eq : self.C.n = 2 * self.wittIndex
• form_alt (v : Fin self.C.n → self.C.k) : self.form v v = 0
• form_add_left (v₁ v₂ w : Fin self.C.n → self.C.k) : self.form (v₁ + v₂) w = self.form v₁ w + self.form v₂ w
• form_add_right (v w₁ w₂ : Fin self.C.n → self.C.k) : self.form v (w₁ + w₂) = self.form v w₁ + self.form v w₂
• form_smul_left (c : self.C.k) (v w : Fin self.C.n → self.C.k) : self.form (c • v) w = c * self.form v w
• form_nondeg (v : Fin self.C.n → self.C.k) : (∀ (w : Fin self.C.n → self.C.k), self.form v w = 0) → v = 0
• hyp_pairs : Fin self.wittIndex → (Fin self.C.n → self.C.k) × (Fin self.C.n → self.C.k)
• pairs_unit (i : Fin self.wittIndex) : self.C.isUnitInO (self.form (self.hyp_pairs i).1 (self.hyp_pairs i).2)
• pairs_iso_e (i : Fin self.wittIndex) : self.form (self.hyp_pairs i).1 (self.hyp_pairs i).1 = 0
• pairs_iso_f (i : Fin self.wittIndex) : self.form (self.hyp_pairs i).2 (self.hyp_pairs i).2 = 0
• pairs_ortho (i j : Fin self.wittIndex) : i ≠ j → self.form (self.hyp_pairs i).1 (self.hyp_pairs j).1 = 0 ∧ self.form (self.hyp_pairs i).1 (self.hyp_pairs j).2 = 0 ∧ self.form (self.hyp_pairs i).2 (self.hyp_pairs j).1 = 0 ∧ self.form (self.hyp_pairs i).2 (self.hyp_pairs j).2 = 0
• stdLattice : self.C.OLattice
• std_contains_e (i : Fin self.wittIndex) : (self.hyp_pairs i).1 ∈ self.stdLattice.carrier
• std_contains_f (i : Fin self.wittIndex) : (self.hyp_pairs i).2 ∈ self.stdLattice.carrier
• std_form_integral (v : Fin self.C.n → self.C.k) : v ∈ self.stdLattice.carrier → ∀ w ∈ self.stdLattice.carrier, self.C.isInO (self.form v w)
• std_nondeg_mod (v : Fin self.C.n → self.C.k) : v ∈ self.stdLattice.carrier → (¬∃ w ∈ self.stdLattice.carrier, v = self.C.oscal self.C.uniformizer w) → ∃ w ∈ self.stdLattice.carrier, self.C.isUnitInO (self.form v w)

structure DoubleOriflammeContext : Type 1

Data for the double oriflamme building (type $\tilde D_n$, $n \ge 4$): a symmetric bilinear form with a hyperbolic basis of half-dimension $\ge 4$, together with a standard unimodular lattice and the modular non-degeneracy condition.

• C : DVRContext
• form : (Fin self.C.n → self.C.k) → (Fin self.C.n → self.C.k) → self.C.k
• halfDim : ℕ
• halfDim_ge_4 : self.halfDim ≥ 4
• dim_eq : self.C.n = 2 * self.halfDim
• form_symm (v w : Fin self.C.n → self.C.k) : self.form v w = self.form w v
• form_add_left (v₁ v₂ w : Fin self.C.n → self.C.k) : self.form (v₁ + v₂) w = self.form v₁ w + self.form v₂ w
• form_smul_left (c : self.C.k) (v w : Fin self.C.n → self.C.k) : self.form (c • v) w = c * self.form v w
• form_nondeg (v : Fin self.C.n → self.C.k) : (∀ (w : Fin self.C.n → self.C.k), self.form v w = 0) → v = 0
• hyp_pairs : Fin self.halfDim → (Fin self.C.n → self.C.k) × (Fin self.C.n → self.C.k)
• pairs_unit (i : Fin self.halfDim) : self.C.isUnitInO (self.form (self.hyp_pairs i).1 (self.hyp_pairs i).2)
• pairs_iso_e (i : Fin self.halfDim) : self.form (self.hyp_pairs i).1 (self.hyp_pairs i).1 = 0
• pairs_iso_f (i : Fin self.halfDim) : self.form (self.hyp_pairs i).2 (self.hyp_pairs i).2 = 0
• pairs_ortho (i j : Fin self.halfDim) : i ≠ j → self.form (self.hyp_pairs i).1 (self.hyp_pairs j).1 = 0 ∧ self.form (self.hyp_pairs i).1 (self.hyp_pairs j).2 = 0 ∧ self.form (self.hyp_pairs i).2 (self.hyp_pairs j).1 = 0 ∧ self.form (self.hyp_pairs i).2 (self.hyp_pairs j).2 = 0
• stdLattice : self.C.OLattice
• std_contains_e (i : Fin self.halfDim) : (self.hyp_pairs i).1 ∈ self.stdLattice.carrier
• std_contains_f (i : Fin self.halfDim) : (self.hyp_pairs i).2 ∈ self.stdLattice.carrier
• std_form_integral (v : Fin self.C.n → self.C.k) : v ∈ self.stdLattice.carrier → ∀ w ∈ self.stdLattice.carrier, self.C.isInO (self.form v w)
• std_nondeg_mod (v : Fin self.C.n → self.C.k) : v ∈ self.stdLattice.carrier → (¬∃ w ∈ self.stdLattice.carrier, v = self.C.oscal self.C.uniformizer w) → ∃ w ∈ self.stdLattice.carrier, self.C.isUnitInO (self.form v w)

structure SingleOriflammeContext : Type 1

Data for the single oriflamme building (type $\tilde B_n$): a symmetric bilinear form with an anisotropic vector, a primitive lattice on which the form is integral, Hensel's lemma for the quadratic form, and the assumption that $2$ is a unit.

• C : DVRContext
• form : (Fin self.C.n → self.C.k) → (Fin self.C.n → self.C.k) → self.C.k
• wittIndex : ℕ
• form_symm (v w : Fin self.C.n → self.C.k) : self.form v w = self.form w v
• form_add_left (v₁ v₂ w : Fin self.C.n → self.C.k) : self.form (v₁ + v₂) w = self.form v₁ w + self.form v₂ w
• form_smul_left (c : self.C.k) (v w : Fin self.C.n → self.C.k) : self.form (c • v) w = c * self.form v w
• form_nondeg (v : Fin self.C.n → self.C.k) : (∀ (w : Fin self.C.n → self.C.k), self.form v w = 0) → v = 0
• primLat : self.C.OLattice
• primLat_integral (v : Fin self.C.n → self.C.k) : v ∈ self.primLat.carrier → ∀ w ∈ self.primLat.carrier, self.C.isInO (self.form v w)
• primLat_nondeg (v : Fin self.C.n → self.C.k) : v ∈ self.primLat.carrier → (¬∃ w ∈ self.primLat.carrier, v = self.C.oscal self.C.uniformizer w) → ∃ w ∈ self.primLat.carrier, self.C.isUnitInO (self.form v w)
• anisotropic_exists : ∃ v ∈ self.primLat.carrier, (¬∃ w ∈ self.primLat.carrier, v = self.C.oscal self.C.uniformizer w) ∧ self.C.isUnitInO (self.form v v)
• aniso_nondeg (v : Fin self.C.n → self.C.k) : (∀ w ∈ self.primLat.carrier, self.form w w = 0 → self.form v w = 0) → self.form v v = 0 → v = 0
• two_is_unit : self.C.isUnitInO (self.C.embed (1 + 1))
• hensel (b c : self.C.k) : self.C.isUnitInO b → self.C.isInMaxIdeal c → ∃ (α : self.C.k), α * α + b * α + c = 0