structure GLnBuilding.BaseFlagHyp (k : Type u_1) [Field k] (n : ℕ) : Type u_1

Hypothesis providing a fixed maximal flag (chain of length $n-1$ of proper non-zero subspaces) to act as a starting point for refinements.

• base_chain : List (Submodule k (Vec k n))
• base_chain_is_chain : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) self.base_chain
• base_chain_length : self.base_chain.length = n - 1
• base_chain_proper (V : Submodule k (Vec k n)) : V ∈ self.base_chain → V ≠ ⊥ ∧ V ≠ ⊤

structure GLnBuilding.ChainInsertionHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: every pair $A < B$ of subspaces with $\dim B \ge \dim A + 2$ admits an intermediate subspace $W$ with $A < W < B$.

• fill_gap (A B : Submodule k (Vec k n)) : A < B → Module.finrank k ↥A + 2 ≤ Module.finrank k ↥B → ∃ (W : Submodule k (Vec k n)), A < W ∧ W < B

noncomputable def GLnBuilding.chainInsertionHyp (k : Type u_1) [Field k] (n : ℕ) : ChainInsertionHyp k n

Existence of an intermediate subspace whenever the dimension gap is at least $2$, by adjoining a single vector $v \in B \setminus A$.

structure GLnBuilding.FlagInsertionHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: a proper subspace $V$ can be inserted into any maximal flag to produce a new maximal flag containing both the original chain and $V$.

• insert (chain : List (Submodule k (Vec k n))) (V : Submodule k (Vec k n)) : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain → chain.length = n - 1 → (∀ W ∈ chain, W ≠ ⊥ ∧ W ≠ ⊤) → V ≠ ⊥ → V ≠ ⊤ → ∃ (chain' : List (Submodule k (Vec k n))), V ∈ chain' ∧ (∀ W ∈ chain, W ∈ chain') ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain' ∧ chain'.length = n - 1 ∧ ∀ W ∈ chain', W ≠ ⊥ ∧ W ≠ ⊤

noncomputable def GLnBuilding.latticeChainRefinementOfInsertion (k : Type u_1) [Field k] (n : ℕ) (base : BaseFlagHyp k n) (ins : FlagInsertionHyp k n) : LatticeChainRefinementHyp k n

Given a base flag and a single-subspace insertion hypothesis, refine any finite list of proper subspaces into a single maximal flag containing all of them, by inductively inserting them one at a time.