theorem GeometricAlgebra.isCompl_of_isOppositeFlag {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (i : Fin F.len) : IsCompl (F.spaces i) (F'.spaces ⟨F'.len - 1 - ↑i, ⋯⟩)

If F' is an opposite flag to F, then for each level i the space F.spaces i and the matching level F'.spaces (F'.len - 1 - i) of F' are complementary.

theorem GeometricAlgebra.opposite_top_is_bot {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (hlen : 0 < F.len) (hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) : F'.spaces ⟨0, ⋯⟩ = ⊥

If the top level of F is all of V and F' is opposite to F, then the bottom level of F' is the zero subspace.

theorem GeometricAlgebra.semidirect_existence_len_one {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (hlen1 : F.len = 1) (hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (p : V ≃ₗ[k] V) (hp : ∀ (i : Fin F.len), Submodule.map (↑p) (F.spaces i) = F.spaces i) : ∃ (d : V ≃ₗ[k] V) (u : V ≃ₗ[k] V), (∀ (i : Fin F.len), Submodule.map (↑d) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F'.len), Submodule.map (↑d) (F'.spaces i) = F'.spaces i) ∧ (∀ (i : Fin F.len), Submodule.map (↑u) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) ∧ ↑p = ↑d ∘ₗ ↑u

Base case of the semidirect existence theorem: for a length-one flag (with the unique level equal to V), the trivial factorization p = p ∘ id works.

theorem GeometricAlgebra.map_eq_of_forall_mem {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (W : Submodule k V) (e : V ≃ₗ[k] V) (h1 : ∀ w ∈ W, e w ∈ W) (h2 : ∀ w ∈ W, e.symm w ∈ W) : Submodule.map (↑e) W = W

A submodule W is preserved by a linear equivalence e iff e maps W into itself and e.symm maps W into itself.

theorem GeometricAlgebra.block_diagonal_decomp {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (W W' : Submodule k V) (hc : IsCompl W W') (p : V ≃ₗ[k] V) (hpW : Submodule.map (↑p) W = W) : ∃ (d₀ : V ≃ₗ[k] V) (u₀ : V ≃ₗ[k] V), Submodule.map (↑d₀) W = W ∧ Submodule.map (↑d₀) W' = W' ∧ Submodule.map (↑u₀) W = W ∧ (∀ (v : V), ↑u₀ v - v ∈ W) ∧ ↑p = ↑d₀ ∘ₗ ↑u₀ ∧ ∀ w ∈ W, d₀ w = p w

Block-diagonal decomposition: given a p-stable subspace W with complement W', factor p = d₀ ∘ u₀ where d₀ is block-diagonal (stabilizes both W and W' and agrees with p on W) and u₀ is "unipotent" along W (i.e. u₀ v - v ∈ W for every v). The block-diagonal part d₀ is constructed via the projection W' →ₗ W' induced by p.

theorem GeometricAlgebra.preserves_of_unipotent_le {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (S W : Submodule k V) (e : V ≃ₗ[k] V) (hunip : ∀ (v : V), ↑e v - v ∈ W) (hle : W ≤ S) : Submodule.map (↑e) S = S

A "unipotent" linear equivalence (one whose deviation from the identity lies in W) preserves every submodule S containing W.

theorem GeometricAlgebra.semidirect_existence_inductive_step {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (F F' : Flag k V) (hopp : F.isOppositeFlag F') (hlen : 2 ≤ F.len) (hcov : F.spaces ⟨F.len - 1, ⋯⟩ = ⊤) (p : V ≃ₗ[k] V) (hp : ∀ (i : Fin F.len), Submodule.map (↑p) (F.spaces i) = F.spaces i) (ih : ∀ (G G' : Flag k V), G.len = G'.len → (∀ (hlen_eq : G.len = G'.len) (i : Fin G.len), G.spaces i ⊔ G'.spaces ⟨G'.len - 1 - ↑i, ⋯⟩ = ⊤ ∧ G.spaces i ⊓ G'.spaces ⟨G'.len - 1 - ↑i, ⋯⟩ = ⊥) → G.len < F.len → ∀ (hGpos : 0 < G.len), G.spaces ⟨G.len - 1, ⋯⟩ = ⊤ → ∀ (q : V ≃ₗ[k] V), (∀ (j : Fin G.len), Submodule.map (↑q) (G.spaces j) = G.spaces j) → ∃ (d : V ≃ₗ[k] V) (u : V ≃ₗ[k] V), (∀ (j : Fin G.len), Submodule.map (↑d) (G.spaces j) = G.spaces j) ∧ (∀ (j : Fin G'.len), Submodule.map (↑d) (G'.spaces j) = G'.spaces j) ∧ (∀ (j : Fin G.len), Submodule.map (↑u) (G.spaces j) = G.spaces j) ∧ (∀ (j : Fin G.len), ∀ v ∈ G.spaces j, ↑u v - v ∈ if x : ↑j = 0 then ⊥ else G.spaces ⟨↑j - 1, ⋯⟩) ∧ ↑q = ↑d ∘ₗ ↑u) : ∃ (d : V ≃ₗ[k] V) (u : V ≃ₗ[k] V), (∀ (i : Fin F.len), Submodule.map (↑d) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F'.len), Submodule.map (↑d) (F'.spaces i) = F'.spaces i) ∧ (∀ (i : Fin F.len), Submodule.map (↑u) (F.spaces i) = F.spaces i) ∧ (∀ (i : Fin F.len), ∀ v ∈ F.spaces i, ↑u v - v ∈ if x : ↑i = 0 then ⊥ else F.spaces ⟨↑i - 1, ⋯⟩) ∧ ↑p = ↑d ∘ₗ ↑u

Inductive step of the semidirect existence theorem: given the IH for shorter flags, factor a stabilizer of F as p = d ∘ u where d preserves both F and the opposite flag F', and u is unipotent along the flag.