def Oriflamme.IsTotallyIsotropic (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) : Prop

A subspace $W \le V$ is totally isotropic for $B$ if $B(v, w) = 0$ for all $v, w \in W$.

def Oriflamme.IsMaximalTotallyIsotropic (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) : Prop

A totally isotropic subspace $W$ is maximal if it is not properly contained in any larger totally isotropic subspace.

@[reducible, inline]

abbrev Oriflamme.MaxIsotropicClass : Type

The two $\mathrm{SO}(n, n)$-orbits of maximal isotropic $n$-subspaces, indexed by Bool ($V_1$ and $V_2$ in the oriflamme construction).

def Oriflamme.IsOriflammeVertex (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (W : Submodule k V) : Prop

An oriflamme vertex: a nonzero totally isotropic subspace whose dimension is not $n - 1$ (this dimension is excluded by the oriflamme construction).

def Oriflamme.OriflammeIncident (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (n : ℕ) (x y : Submodule k V) : Prop

Oriflamme incidence: two oriflamme vertices $x, y$ are incident if $x \subsetneq y$, $y \subsetneq x$, or both are $n$-dimensional with $\dim(x \cap y) = n - 1$.

structure Oriflamme.OriflammeComplex (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

The oriflamme complex on $(V, B)$: a flag complex of oriflamme vertices, pairwise incident, closed under nonempty subsets.

• simplices : Set (Finset (Submodule k V))
• simplex_vertices (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ W ∈ σ, IsOriflammeVertex k V B n W
• simplex_incident (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ W₁ ∈ σ, ∀ W₂ ∈ σ, OriflammeIncident k V n W₁ W₂
• face_closed (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ τ ⊆ σ, τ.Nonempty → τ ∈ self.simplices

structure Oriflamme.OriflammeChamber (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

An oriflamme chamber: a maximal simplex in the oriflamme complex, consisting of an isotropic chain $W_1 \subsetneq \cdots \subsetneq W_{n-2}$ of dimensions $1, \dots, n-2$ together with two distinct maximal isotropic $n$-subspaces $V_1 \ne V_2$ both containing $W_{n-2}$ and meeting in dimension $n - 1$.

• chain : Fin (n - 2) → Submodule k V
• top₁ : Submodule k V
• top₂ : Submodule k V
• chain_strictMono : StrictMono self.chain
• chain_isotropic (i : Fin (n - 2)) : IsTotallyIsotropic k V B (self.chain i)
• chain_dim (i : Fin (n - 2)) : Module.finrank k ↥(self.chain i) = ↑i + 1
• top₁_isotropic : IsTotallyIsotropic k V B self.top₁
• top₂_isotropic : IsTotallyIsotropic k V B self.top₂
• top₁_dim : Module.finrank k ↥self.top₁ = n
• top₂_dim : Module.finrank k ↥self.top₂ = n
• top₁_ne_top₂ : self.top₁ ≠ self.top₂
• chain_sub_tops (h : 0 < n - 2) : self.chain ⟨n - 3, ⋯⟩ ≤ self.top₁ ⊓ self.top₂
• inter_dim : Module.finrank k ↥(self.top₁ ⊓ self.top₂) = n - 1

structure Oriflamme.OriflammeFrame (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

An oriflamme frame of $(V, B)$: a hyperbolic frame as a decomposition into $n$ hyperbolic planes (one per index $i \in \mathrm{Fin}\, n$), each plane spanned by two isotropic lines indexed by Bool.

• lines : Fin n × Bool → Submodule k V
• lines_isotropic (ib : Fin n × Bool) : IsTotallyIsotropic k V B (self.lines ib)
• lines_dim_one (ib : Fin n × Bool) : Module.finrank k ↥(self.lines ib) = 1
• planes : Fin n → Submodule k V
• planes_eq (i : Fin n) : self.planes i = self.lines (i, true) ⊔ self.lines (i, false)
• span_top : ⨆ (i : Fin n), self.planes i = ⊤

def Oriflamme.OriflammeApartment (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (X : OriflammeComplex k V B n) (F : OriflammeFrame k V B n) : Set (Finset (Submodule k V))

The apartment of the oriflamme complex $X$ associated to a frame $F$: the simplices all of whose vertices are sums of frame lines.

structure Oriflamme.OriflammeIsBuilding (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (X : OriflammeComplex k V B n) : Type u_2

Witness that the oriflamme complex $X$ is a building of type $D_n$: a family of apartments satisfying the common-apartment and apartment-exchange axioms.

• apartments : Set (OriflammeFrame k V B n)
• common_apartment (σ₁ : Finset (Submodule k V)) : σ₁ ∈ X.simplices → ∀ σ₂ ∈ X.simplices, ∃ F ∈ self.apartments, σ₁ ∈ OriflammeApartment k V B n X F ∧ σ₂ ∈ OriflammeApartment k V B n X F
• apartment_exchange (F₁ : OriflammeFrame k V B n) : F₁ ∈ self.apartments → ∀ F₂ ∈ self.apartments, (∃ C ∈ OriflammeApartment k V B n X F₁, C ∈ OriflammeApartment k V B n X F₂) → ∃ (f : Submodule k V → Submodule k V), (∀ σ ∈ OriflammeApartment k V B n X F₁, Finset.image f σ ∈ OriflammeApartment k V B n X F₂) ∧ ∀ (W : Submodule k V), (∃ σ ∈ OriflammeApartment k V B n X F₁ ∩ OriflammeApartment k V B n X F₂, W ∈ σ) → f W = W

def Oriflamme.OriflammeIsometryGroup (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Set (V ≃ₗ[k] V)

The isometry group $O(V, B)$ of the bilinear form: all $k$-linear automorphisms of $V$ preserving $B$.

def Oriflamme.SO_StronglyTransitive (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (X : OriflammeComplex k V B n) (bldg : OriflammeIsBuilding k V B n X) : Prop

The oriflamme building is strongly transitive under $\mathrm{SO}(V, B)$ if any pair of frame/chamber data in two apartments can be mapped one to the other by an isometry.

structure Oriflamme.BNPairData (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

B-N pair data for the oriflamme building: Borel and frame-stabiliser subsets of the isometry group, an oriflamme chamber, a frame, and the Bruhat decomposition $G = B \cdot W \cdot B$.

• borelSet : Set (V ≃ₗ[k] V)
• frameStabSet : Set (V ≃ₗ[k] V)
• borel_sub : self.borelSet ⊆ OriflammeIsometryGroup k V B
• frameStab_sub : self.frameStabSet ⊆ OriflammeIsometryGroup k V B
• chamber : OriflammeChamber k V B n
• borel_stab_chain (g : V ≃ₗ[k] V) : g ∈ self.borelSet → ∀ (i : Fin (n - 2)), Submodule.map (↑g) (self.chamber.chain i) = self.chamber.chain i
• borel_stab_top₁ (g : V ≃ₗ[k] V) : g ∈ self.borelSet → Submodule.map (↑g) self.chamber.top₁ = self.chamber.top₁
• borel_stab_top₂ (g : V ≃ₗ[k] V) : g ∈ self.borelSet → Submodule.map (↑g) self.chamber.top₂ = self.chamber.top₂
• frame : OriflammeFrame k V B n
• frameStab_permutes (g : V ≃ₗ[k] V) : g ∈ self.frameStabSet → ∀ (ib : Fin n × Bool), ∃ (jb : Fin n × Bool), Submodule.map (↑g) (self.frame.lines ib) = self.frame.lines jb
• bruhat (g : V ≃ₗ[k] V) : g ∈ OriflammeIsometryGroup k V B → ∃ w ∈ self.frameStabSet, ∃ b₁ ∈ self.borelSet, ∃ b₂ ∈ self.borelSet, g = b₁ ≪≫ₗ (w ≪≫ₗ b₂)

def Oriflamme.TypeDn (n : ℕ) (hn : n ≥ 3) : Prop

A Coxeter matrix is of type $D_n$ ($n \ge 3$): linear $A_{n-2}$ chain $1 - 2 - \cdots - (n-2)$ with two extra nodes branching off node $n-3$ at angle $3$ and commuting with each other ($m = 2$).

def Oriflamme.IsInOrbitClass (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (F : OriflammeFrame k V B n) (W : Submodule k V) (cls : MaxIsotropicClass) : Prop

The maximal isotropic $n$-subspace $W$ belongs to orbit class $\mathrm{cls}$ relative to the frame $F$ if $W$ is a sum of $n$ frame lines whose parity of false-indexed lines matches $\mathrm{cls}$ (even for true, odd for false).

theorem Oriflamme.isometry_det_sq_eq_one {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (g : V' ≃ₗ[k'] V') (hiso : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) : LinearMap.det ↑g ^ 2 = 1

Any isometry $g$ of a finite-dimensional non-degenerate bilinear form satisfies $(\det g)^2 = 1$.

theorem Oriflamme.isometry_det_eq_one_or_neg_one {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (g : V' ≃ₗ[k'] V') (hiso : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) : LinearMap.det ↑g = 1 ∨ LinearMap.det ↑g = -1

Consequence of $(\det g)^2 = 1$: every isometry has determinant $\pm 1$.

def Oriflamme.SpecialIsometryGroup {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] (B' : LinearMap.BilinForm k' V') : Set (V' ≃ₗ[k'] V')

The special isometry group $\mathrm{SO}(V, B) = \{g : g \text{ isometry}, \det g = 1\}$.

theorem Oriflamme.hyp_swap_det_neg_one {k' : Type u_3} [Field k'] : !![0, 1; 1, 0].det = -1

The hyperbolic swap matrix $\begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$ has determinant $-1$.

theorem Oriflamme.hyp_plane_swap_isometry_det {k' : Type u_3} [Field k'] (e₁ e₂ : Fin 2 → k') (b : Module.Basis (Fin 2) k' (Fin 2 → k')) (hb1 : b 0 = e₁) (hb2 : b 1 = e₂) (g : (Fin 2 → k') ≃ₗ[k'] Fin 2 → k') (a : k') (ha : a ≠ 0) (hge1 : g e₁ = a • e₂) (hge2 : g e₂ = a⁻¹ • e₁) : LinearMap.det ↑g = -1

A hyperbolic-plane swap isometry $g(e_1) = a \cdot e_2$, $g(e_2) = a^{-1} \cdot e_1$ has determinant $-1$.

theorem Oriflamme.witt_extension_theorem {k' : Type u_5} [Field k'] {V' : Type u_6} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (W₁ W₂ Y : Submodule k' V') (hY_le_W₁ : Y ≤ W₁) (hY_le_W₂ : Y ≤ W₂) (hY_dim : Module.finrank k' ↥Y = n - 1) (hW₁_dim : Module.finrank k' ↥W₁ = n) (g : V' ≃ₗ[k'] V') (hg_isom : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) (hg_onto : Submodule.map (↑g) W₁ = W₂) : ∃ (Φ : V' ≃ₗ[k'] V'), (∀ v ∈ Y, Φ (g v) = v) ∧ (∀ (v w : V'), (B' (Φ v)) (Φ w) = (B' v) w) ∧ LinearMap.det ↑Φ = 1

Witt's extension theorem: any isometry between maximal isotropic subspaces fixing a hyperplane $Y$ extends to an isometry of $V$ of determinant $1$.

theorem Oriflamme.witt_extension_preserves_W₂ {k' : Type u_5} [Field k'] {V' : Type u_6} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (W₁ W₂ Y : Submodule k' V') (hY_le_W₁ : Y ≤ W₁) (hY_le_W₂ : Y ≤ W₂) (hY_dim : Module.finrank k' ↥Y = n - 1) (hW₁_dim : Module.finrank k' ↥W₁ = n) (g : V' ≃ₗ[k'] V') (hg_isom : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) (hg_onto : Submodule.map (↑g) W₁ = W₂) : ∃ (Φ : V' ≃ₗ[k'] V'), (∀ v ∈ Y, Φ (g v) = v) ∧ Submodule.map (↑Φ) W₂ = W₂ ∧ (∀ (v w : V'), (B' (Φ v)) (Φ w) = (B' v) w) ∧ LinearMap.det ↑Φ = 1

Refinement of Witt's extension: the extension $\Phi$ can be chosen to additionally preserve the target subspace $W_2$ setwise.

theorem Oriflamme.extend_auto_to_SO {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (W₁ W₂ Y : Submodule k' V') (hY_le_W₁ : Y ≤ W₁) (hY_le_W₂ : Y ≤ W₂) (hY_dim : Module.finrank k' ↥Y = n - 1) (hW₁_dim : Module.finrank k' ↥W₁ = n) (g : V' ≃ₗ[k'] V') (hg_isom : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) (hg_onto : Submodule.map (↑g) W₁ = W₂) : ∃ (h : V' ≃ₗ[k'] V'), (∀ v ∈ Y, h (g v) = v) ∧ Submodule.map (↑h) W₂ = W₂ ∧ (∀ (v w : V'), (B' (h v)) (h w) = (B' v) w) ∧ LinearMap.det ↑h = 1

Wrapper: extending an isometry $g : W_1 \to W_2$ fixing $Y$ to an element of $\mathrm{SO}(V)$ preserving $W_2$.

theorem Oriflamme.witt_adjust_isometry {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (g : V' ≃ₗ[k'] V') (hiso : ∀ (v w : V'), (B' (g v)) (g w) = (B' v) w) (hmaps : Submodule.map (↑g) V₁ = V₂) : ∃ (g' : V' ≃ₗ[k'] V'), (∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) ∧ Submodule.map (↑g') V₁ = V₂ ∧ (∀ v ∈ Y, g' v = v) ∧ LinearMap.det ↑g' = LinearMap.det ↑g

Witt adjustment: given an isometry $g$ mapping $V_1$ to $V_2$, produce an isometry $g'$ with the same determinant that additionally fixes $Y$ pointwise.

theorem Oriflamme.det_quotient_VmodYperp_eq_one {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (_hnd : B'.Nondegenerate) (Y : Submodule k' V') (g' : V' ≃ₗ[k'] V') (hiso' : ∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) (hfix : ∀ v ∈ Y, g' v = v) (he' : B'.orthogonal Y ≤ Submodule.comap (↑g') (B'.orthogonal Y)) : LinearMap.det ((B'.orthogonal Y).mapQ (B'.orthogonal Y) (↑g') he') = 1

For an isometry $g'$ fixing $Y$, the induced map on $V / Y^\perp$ is the identity, hence has determinant $1$.

theorem Oriflamme.hyp_swap_basis_exists {k' : Type u_5} [Field k'] {V' : Type u_6} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (hV_dim : Module.finrank k' V' = 2 * n) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (g' : V' ≃ₗ[k'] V') (hiso' : ∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) (hmaps' : Submodule.map (↑g') V₁ = V₂) (hfix : ∀ v ∈ Y, g' v = v) (he' : B'.orthogonal Y ≤ Submodule.comap (↑g') (B'.orthogonal Y)) (he_inner : Submodule.comap (B'.orthogonal Y).subtype Y ≤ Submodule.comap ((↑g').restrict he') (Submodule.comap (B'.orthogonal Y).subtype Y)) : ∃ (b : Module.Basis (Fin 2) k' (↥(B'.orthogonal Y) ⧸ Submodule.comap (B'.orthogonal Y).subtype Y)) (a : k'), a ≠ 0 ∧ ((Submodule.comap (B'.orthogonal Y).subtype Y).mapQ (Submodule.comap (B'.orthogonal Y).subtype Y) ((↑g').restrict he') he_inner) (b 0) = a • b 1 ∧ ((Submodule.comap (B'.orthogonal Y).subtype Y).mapQ (Submodule.comap (B'.orthogonal Y).subtype Y) ((↑g').restrict he') he_inner) (b 1) = a⁻¹ • b 0

Existence of a hyperbolic-swap basis: on $Y^\perp / Y$ the induced map of $g'$ acts as a hyperbolic swap $b_0 \mapsto a \cdot b_1$, $b_1 \mapsto a^{-1} \cdot b_0$ in some basis.

theorem Oriflamme.det_quotient_YperpmodY_eq_neg_one {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (g' : V' ≃ₗ[k'] V') (hiso' : ∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) (hmaps' : Submodule.map (↑g') V₁ = V₂) (hfix : ∀ v ∈ Y, g' v = v) (he : Y ≤ Submodule.comap (↑g') Y) (he' : B'.orthogonal Y ≤ Submodule.comap (↑g') (B'.orthogonal Y)) (he_inner : Submodule.comap (B'.orthogonal Y).subtype Y ≤ Submodule.comap ((↑g').restrict he') (Submodule.comap (B'.orthogonal Y).subtype Y)) (hswap_basis : ∃ (b : Module.Basis (Fin 2) k' (↥(B'.orthogonal Y) ⧸ Submodule.comap (B'.orthogonal Y).subtype Y)) (a : k'), a ≠ 0 ∧ ((Submodule.comap (B'.orthogonal Y).subtype Y).mapQ (Submodule.comap (B'.orthogonal Y).subtype Y) ((↑g').restrict he') he_inner) (b 0) = a • b 1 ∧ ((Submodule.comap (B'.orthogonal Y).subtype Y).mapQ (Submodule.comap (B'.orthogonal Y).subtype Y) ((↑g').restrict he') he_inner) (b 1) = a⁻¹ • b 0) : LinearMap.det ((Submodule.comap (B'.orthogonal Y).subtype Y).mapQ (Submodule.comap (B'.orthogonal Y).subtype Y) ((↑g').restrict he') he_inner) = -1

The induced map of $g'$ on the quotient $Y^\perp / Y$ has determinant $-1$ (this is the hyperbolic swap contribution that flips orientation).

theorem Oriflamme.det_quotient_map_neg_one_of_isometry_swap {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (hV_dim : Module.finrank k' V' = 2 * n) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (g' : V' ≃ₗ[k'] V') (hiso' : ∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) (hmaps' : Submodule.map (↑g') V₁ = V₂) (hfix : ∀ v ∈ Y, g' v = v) (he : Y ≤ Submodule.comap (↑g') Y) : LinearMap.det (Y.mapQ Y (↑g') he) = -1

Combines the three filtration pieces $(Y, Y^\perp/Y, V/Y^\perp)$ to compute $\det(g'|_{V/Y}) = -1$ for an isometry swapping the two distinct maximal isotropic subspaces.

theorem Oriflamme.adjusted_isometry_det_neg_one {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (n : ℕ) (hV_dim : Module.finrank k' V' = 2 * n) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (g' : V' ≃ₗ[k'] V') (hiso' : ∀ (v w : V'), (B' (g' v)) (g' w) = (B' v) w) (hmaps' : Submodule.map (↑g') V₁ = V₂) (hfix : ∀ v ∈ Y, g' v = v) : LinearMap.det ↑g' = -1

The adjusted isometry $g'$ (from witt_adjust_isometry) swapping the two distinct maximal isotropic subspaces has $\det g' = -1$.

theorem Oriflamme.distinct_SO_orbits {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (hchar : 2 ≠ 0) (n : ℕ) (hV_dim : Module.finrank k' V' = 2 * n) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) : ¬∃ g ∈ SpecialIsometryGroup B', Submodule.map (↑g) V₁ = V₂

Distinctness of the two $\mathrm{SO}(n,n)$-orbits (Ch. 11): in characteristic $\ne 2$, no element of $\mathrm{SO}(V, B)$ can map one maximal isotropic $n$-subspace to a distinct one sharing a hyperplane, because such a map would have $\det = -1$.

theorem Oriflamme.exactly_two_SO_orbits {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (n : ℕ) (V_plus V_minus : Submodule k' V') (hVp_ti : IsTotallyIsotropic k' V' B' V_plus) (hVp_dim : Module.finrank k' ↥V_plus = n) (hVm_ti : IsTotallyIsotropic k' V' B' V_minus) (hVm_dim : Module.finrank k' ↥V_minus = n) (hVpm_ne : V_plus ≠ V_minus) (Y₀ : Submodule k' V') (_hY₀_ti : IsTotallyIsotropic k' V' B' Y₀) (hY₀_dim : Module.finrank k' ↥Y₀ = n - 1) (_hY₀_Vp : Y₀ ≤ V_plus) (_hY₀_Vm : Y₀ ≤ V_minus) (prop1_transported : ∀ g ∈ SpecialIsometryGroup B', ∀ (W : Submodule k' V'), IsTotallyIsotropic k' V' B' W → Module.finrank k' ↥W = n → Submodule.map (↑g) Y₀ ≤ W → W = Submodule.map (↑g) V_plus ∨ W = Submodule.map (↑g) V_minus) (so_transitive_codim1 : ∀ (Y₁ Y₂ : Submodule k' V'), IsTotallyIsotropic k' V' B' Y₁ → Module.finrank k' ↥Y₁ = n - 1 → IsTotallyIsotropic k' V' B' Y₂ → Module.finrank k' ↥Y₂ = n - 1 → ∃ g ∈ SpecialIsometryGroup B', Submodule.map (↑g) Y₁ = Y₂) (contains_codim1 : ∀ (W : Submodule k' V'), IsTotallyIsotropic k' V' B' W → Module.finrank k' ↥W = n → ∃ (Y : Submodule k' V'), IsTotallyIsotropic k' V' B' Y ∧ Module.finrank k' ↥Y = n - 1 ∧ Y ≤ W) (W : Submodule k' V') : IsTotallyIsotropic k' V' B' W → Module.finrank k' ↥W = n → (∃ g ∈ SpecialIsometryGroup B', Submodule.map (↑g) V_plus = W) ∨ ∃ g ∈ SpecialIsometryGroup B', Submodule.map (↑g) V_minus = W

Exactly two $\mathrm{SO}(V, B)$-orbits on maximal isotropic $n$-subspaces: under transitivity on codimension-$1$ isotropic subspaces, every maximal isotropic $n$-subspace lies in the orbit of $V_+$ or of $V_-$.

theorem Oriflamme.distinct_orbit_classes {k' : Type u_3} [Field k'] {V' : Type u_4} [AddCommGroup V'] [Module k' V'] [FiniteDimensional k' V'] (B' : LinearMap.BilinForm k' V') (hnd : B'.Nondegenerate) (hchar : 2 ≠ 0) (n : ℕ) (hV_dim : Module.finrank k' V' = 2 * n) (F : OriflammeFrame k' V' B' n) (Y : Submodule k' V') (hY_iso : IsTotallyIsotropic k' V' B' Y) (hY_dim : Module.finrank k' ↥Y = n - 1) (V₁ V₂ : Submodule k' V') (hV₁_iso : IsTotallyIsotropic k' V' B' V₁) (hV₁_dim : Module.finrank k' ↥V₁ = n) (hV₁_sub : V₁ ≤ B'.orthogonal Y) (hY_le_V₁ : Y ≤ V₁) (hV₂_iso : IsTotallyIsotropic k' V' B' V₂) (hV₂_dim : Module.finrank k' ↥V₂ = n) (hV₂_sub : V₂ ≤ B'.orthogonal Y) (hY_le_V₂ : Y ≤ V₂) (hV₁₂ : V₁ ≠ V₂) (orbit_class_transitive : ∀ (cls : MaxIsotropicClass) (W₁ W₂ : Submodule k' V'), IsInOrbitClass k' V' B' n F W₁ cls → IsInOrbitClass k' V' B' n F W₂ cls → ∃ g ∈ SpecialIsometryGroup B', Submodule.map (↑g) W₁ = W₂) (cls : MaxIsotropicClass) : ¬(IsInOrbitClass k' V' B' n F V₁ cls ∧ IsInOrbitClass k' V' B' n F V₂ cls)

The two oriflamme orbit classes are disjoint: no maximal isotropic subspace lies in both orbit classes simultaneously, since otherwise an $\mathrm{SO}$-element would identify the two distinguished types $V_1$ and $V_2$, contradicting distinct_SO_orbits.