@[irreducible]
theorem
GeometricAlgebra.semidirect_existence_compl
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
(G G' : Flag k V)
(hlen_eq : G.len = G'.len)
(hcompl :
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, ⋯⟩ = ⊥)
(hlen_pos : 0 < G.len)
(hcov : G.spaces ⟨G.len - 1, ⋯⟩ = ⊤)
(q : V ≃ₗ[k] V)
(hq : ∀ (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 h : ↑j = 0 then ⊥ else G.spaces ⟨↑j - 1, ⋯⟩) ∧ ↑q = ↑d ∘ₗ ↑u
Main inductive construction of the semidirect decomposition p = d ∘ u for a flag
stabilizer: starting from any automorphism q that preserves the flag G, peel off the
smallest level W = G.spaces 0 and its opposite W' = G'.spaces (G'.len - 1), decompose
the action on the block W ⊕ W', recurse on the truncated flags H, H', and reassemble
the decomposition. Proceeds by termination on G.len.
instance
GeometricAlgebra.instSemidirectExistencePropertyOfFiniteDimensional
{k : Type u_1}
[Field k]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[FiniteDimensional k V]
:
Strong-induction wrapper around semidirect_existence_compl that establishes the
SemidirectExistenceProperty for any finite-dimensional V: the parabolic stabilizer of
a flag admits the Levi-unipotent semidirect decomposition p = d ∘ u.