Hypothesis: from any maximal proper flag one can extract $n$ lines that span $k^n$ independently and are compatible with every subspace of the flag — i.e.\ an adapted basis.
- extract (chain : List (Submodule k (Vec k n))) : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain → chain.length = n - 1 → (∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤) → ∃ (lines : Fin n → Submodule k (Vec k n)), (∀ (i : Fin n), Module.finrank k ↥(lines i) = 1) ∧ iSupIndep lines ∧ ⨆ (i : Fin n), lines i = ⊤ ∧ ∀ V ∈ chain, ∃ (S : Finset (Fin n)), V = ⨆ j ∈ S, lines j
Instances For
noncomputable def
GLnBuilding.flagToFrameOfBasis
(k : Type u_1)
[Field k]
(n : ℕ)
(hyp : BasisFromFlagHyp k n)
:
FlagToFrameHyp k n
Package the extracted lines into a Frame k n, witnessing the flag-to-frame hypothesis.