Exact enumeration of complete flags

For a natural number q, qInteger q n is the polynomial 1 + q + ... + q^(n-1). The product qFactorial q n is

[n]_q [n-1]_q ... [1]_q.

The order of the factors is reversed only to make the factorization used in the proof definitionally transparent; multiplication in ℕ is commutative.

We prove the complete-flag formula by counting adapted ordered bases. For a complete flag F, an adapted vector at step i is a vector in F_(i+1) \ F_i. Choosing one at every step always gives a basis, and every ordered basis is obtained exactly once after retaining its induced flag. Mathlib's exact enumeration of linearly independent tuples then gives the q-factorial formula.

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

def MooreBound.DegreeDiameter.qInteger (q n : ℕ) : ℕ

The q-integer [n]_q = 1 + q + ... + q^(n-1).

Equations

• MooreBound.DegreeDiameter.qInteger q n = ∑ i ∈ Finset.range n, q ^ i

def MooreBound.DegreeDiameter.qFactorial (q n : ℕ) : ℕ

The q-factorial [n]_q! = [n]_q [n-1]_q ... [1]_q.

Writing the factors in descending order agrees with the usual q-factorial because multiplication in ℕ is commutative.

Equations

• MooreBound.DegreeDiameter.qFactorial q n = ∏ i : Fin n, MooreBound.DegreeDiameter.qInteger q (n - ↑i)

@[simp]

theorem MooreBound.DegreeDiameter.qInteger_zero (q : ℕ) : qInteger q 0 = 0

@[simp]

theorem MooreBound.DegreeDiameter.qInteger_one (q : ℕ) : qInteger q 1 = 1

@[simp]

theorem MooreBound.DegreeDiameter.qFactorial_zero (q : ℕ) : qFactorial q 0 = 1

theorem MooreBound.DegreeDiameter.qFactorial_succ (q n : ℕ) : qFactorial q (n + 1) = qInteger q (n + 1) * qFactorial q n

theorem MooreBound.DegreeDiameter.qFactorial_eq_prod_range (q n : ℕ) : qFactorial q n = ∏ j ∈ Finset.range n, qInteger q (j + 1)

The descending-product definition is the conventional ascending product [1]_q [2]_q ... [n]_q.

theorem MooreBound.DegreeDiameter.qInteger_mul_sub_one (q n : ℕ) (hq : 1 ≤ q) : qInteger q n * (q - 1) = q ^ n - 1

instance MooreBound.DegreeDiameter.CompleteFlag.instFinite {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} [Finite V] : Finite (CompleteFlag K V n)

Complete flags form a finite type when the ambient vector space is finite.

def MooreBound.DegreeDiameter.FlagStepVector {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (F : CompleteFlag K V n) (i : Fin n) : Type u_2

A vector which advances the complete flag F from rank i to rank i+1.

Equations

• MooreBound.DegreeDiameter.FlagStepVector F i = { x : ↥(F.space i.succ) // ↑x ∉ F.space i.castSucc }

instance MooreBound.DegreeDiameter.flagStepVectorFinite {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} [Finite V] (F : CompleteFlag K V n) (i : Fin n) : Finite (FlagStepVector F i)

def MooreBound.DegreeDiameter.FlagStepChoices {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (F : CompleteFlag K V n) : Type u_2

One advancing vector at every rank of a complete flag.

Equations

• MooreBound.DegreeDiameter.FlagStepChoices F = ((i : Fin n) → MooreBound.DegreeDiameter.FlagStepVector F i)

instance MooreBound.DegreeDiameter.flagStepChoicesFinite {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} [Finite V] (F : CompleteFlag K V n) : Finite (FlagStepChoices F)

def MooreBound.DegreeDiameter.AdaptedFlagBasis (K : Type u_3) (V : Type u_4) [Field K] [AddCommGroup V] [Module K V] (n : ℕ) : Type u_4

A complete flag together with a choice of one advancing vector at every rank.

Equations

• MooreBound.DegreeDiameter.AdaptedFlagBasis K V n = ((F : MooreBound.DegreeDiameter.CompleteFlag K V n) × MooreBound.DegreeDiameter.FlagStepChoices F)

def MooreBound.DegreeDiameter.adaptedVectors {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (d : AdaptedFlagBasis K V n) : Fin n → V

Forget the submodule-membership proofs in an adapted flag basis.

Equations

• MooreBound.DegreeDiameter.adaptedVectors d i = ↑↑(d.snd i)

def MooreBound.DegreeDiameter.previousStepEquiv {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (F : CompleteFlag K V n) (i : Fin n) : { x : ↥(F.space i.succ) // ↑x ∈ F.space i.castSucc } ≃ ↥(F.space i.castSucc)

Vectors in the preceding subspace, regarded as vectors in the next subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem MooreBound.DegreeDiameter.natCard_flagStepVector {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} [Finite K] [Finite V] (F : CompleteFlag K V n) (i : Fin n) : Nat.card (FlagStepVector F i) = Nat.card K ^ (↑i + 1) - Nat.card K ^ ↑i

theorem MooreBound.DegreeDiameter.adaptedVectors_linearIndependent {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (d : AdaptedFlagBasis K V n) : LinearIndependent K (adaptedVectors d)

theorem MooreBound.DegreeDiameter.span_adaptedVectors_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (d : AdaptedFlagBasis K V n) [FiniteDimensional K V] (r : Fin (n + 1)) : Submodule.span K (adaptedVectors d '' {i : Fin n | i.castSucc < r}) = d.fst.space r

The span of the first r adapted vectors is exactly the rank-r subspace of the flag.

noncomputable def MooreBound.DegreeDiameter.adaptedFlagBasisEquivLinearIndependent {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} [FiniteDimensional K V] (hV : Module.finrank K V = n) : AdaptedFlagBasis K V n ≃ { v : Fin n → V // LinearIndependent K v }

An adapted flag basis is exactly a linearly independent n-tuple.

Equations

• One or more equations did not get rendered due to their size.

theorem MooreBound.DegreeDiameter.independentFactor_eq (q n : ℕ) (hq : 1 ≤ q) (i : Fin n) : q ^ n - q ^ ↑i = (q ^ (↑i + 1) - q ^ ↑i) * qInteger q (n - ↑i)

The factor in the exact count of independent tuples splits into the number of choices advancing a fixed flag and the corresponding q-integer.

theorem MooreBound.DegreeDiameter.independentProduct_eq (q n : ℕ) (hq : 1 ≤ q) : ∏ i : Fin n, (q ^ n - q ^ ↑i) = (∏ i : Fin n, (q ^ (↑i + 1) - q ^ ↑i)) * qFactorial q n

theorem MooreBound.DegreeDiameter.natCard_completeFlag_of_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] [FiniteDimensional K V] {n : ℕ} (hV : Module.finrank K V = n) : Nat.card (CompleteFlag K V n) = qFactorial (Nat.card K) n

The exact number of complete flags in an n-dimensional vector space over a finite field is [n]_q!, where q is the cardinality of the field.

theorem MooreBound.DegreeDiameter.natCard_completeFlag_finFun {K : Type u_1} [Field K] [Finite K] (n : ℕ) : Nat.card (CompleteFlag K (Fin n → K) n) = qFactorial (Nat.card K) n

Coordinate-space specialization of natCard_completeFlag_of_finrank. This is the literal formula |Flag(K^n)| = [n]_(|K|)!.