A common ordered basis for two complete flags

This file isolates and proves the standard common-basis fact used as the first step in the proof of Lemma 2.1 in Cames van Batenburg--Korsky. It is not an assumption: common_apartment constructs the basis and permutation, and common_basis_orderings spells out the two prefix-span formulas from the paper.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

structure MooreBound.DegreeDiameter.CompleteFlag (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) : Type u_2

A complete flag in an n-dimensional vector space, indexed by its ranks 0, ..., n. Both strictness and the rank condition are recorded explicitly, ruling out degenerate chains.

• space : Fin (n + 1) → Submodule K V

  The subspace at each rank of the complete flag.

• strictMono_space : StrictMono self.space
• finrank_space (i : Fin (n + 1)) : Module.finrank K ↥(self.space i) = ↑i
• space_zero : self.space 0 = ⊥
• space_last : self.space (Fin.last n) = ⊤

@[instance_reducible]

instance MooreBound.DegreeDiameter.CompleteFlag.instCoeFunForallFinHAddNatOfNatSubmodule {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : CoeFun (CompleteFlag K V n) fun (x : CompleteFlag K V n) => Fin (n + 1) → Submodule K V

Equations

• MooreBound.DegreeDiameter.CompleteFlag.instCoeFunForallFinHAddNatOfNatSubmodule = { coe := MooreBound.DegreeDiameter.CompleteFlag.space }

theorem MooreBound.DegreeDiameter.CompleteFlag.ext {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {F G : CompleteFlag K V n} (h : ∀ (i : Fin (n + 1)), F.space i = G.space i) : F = G

theorem MooreBound.DegreeDiameter.CompleteFlag.ext_iff {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {F G : CompleteFlag K V n} : F = G ↔ ∀ (i : Fin (n + 1)), F.space i = G.space i

noncomputable def MooreBound.DegreeDiameter.CompleteFlag.ofBasis {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Module.Basis (Fin n) K V) : CompleteFlag K V n

The complete flag of prefix spans of an ordered basis.

Equations

• MooreBound.DegreeDiameter.CompleteFlag.ofBasis b = { space := b.flag, strictMono_space := ⋯, finrank_space := ⋯, space_zero := ⋯, space_last := ⋯ }

def MooreBound.DegreeDiameter.PrefixSet {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin (n + 1)) : Set (Fin n)

The set of entries appearing before rank i in an ordering σ.

Equations

• MooreBound.DegreeDiameter.PrefixSet σ i = ⇑σ '' {j : Fin n | j.castSucc < i}

theorem MooreBound.DegreeDiameter.ofBasis_reindex_apply (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Module.Basis (Fin n) K V) (σ : Equiv.Perm (Fin n)) (i : Fin (n + 1)) : (CompleteFlag.ofBasis (b.reindex (Equiv.symm σ))).space i = Submodule.span K (⇑b '' PrefixSet σ i)

theorem MooreBound.DegreeDiameter.common_apartment (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (F F' : CompleteFlag K V n) : ∃ (b : Module.Basis (Fin n) K V) (π : Equiv.Perm (Fin n)), F = CompleteFlag.ofBasis b ∧ F' = CompleteFlag.ofBasis (b.reindex (Equiv.symm π))

Any two complete flags lie in a common apartment: after choosing one ordered basis, the second flag is obtained by permuting that same basis. The inverse in π.symm compensates for Mathlib's convention for Basis.reindex.

theorem MooreBound.DegreeDiameter.common_basis_orderings (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (F F' : CompleteFlag K V n) : ∃ (b : Module.Basis (Fin n) K V) (π : Equiv.Perm (Fin n)), (∀ (i : Fin (n + 1)), F.space i = Submodule.span K (⇑b '' {j : Fin n | j.castSucc < i})) ∧ ∀ (i : Fin (n + 1)), F'.space i = Submodule.span K (⇑b '' PrefixSet π i)

The common-basis step in the paper, written literally as prefix spans. For i : Fin (n + 1), {j | j.castSucc < i} represents the first i positions. Thus b is the ordered basis (v₁, ..., vₙ), while π gives the second ordering (v_{π(1)}, ..., v_{π(n)}).