The halved flag graph

This file defines the two kinds of partial flags and their compatibility relation exactly as in the paper. A partial flag is represented by a full rank-indexed family in which ranks of the other parity are replaced by ⊥. The fixed endpoint ranks are retained; this does not change the objects and makes even and odd parts jointly determine a complete flag definitionally.

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.flagPart {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (parity : ℕ) (F : CompleteFlag K V n) : Fin (n + 1) → Submodule K V

Keep the ranks congruent to parity modulo two and erase the others.

Equations

• MooreBound.DegreeDiameter.flagPart parity F i = if ↑i % 2 = parity % 2 then F.space i else ⊥

def MooreBound.DegreeDiameter.PartialFlag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (parity : ℕ) : Type u_2

Partial complete flags supported on one parity of ranks.

Equations

• MooreBound.DegreeDiameter.PartialFlag parity = { P : Fin (n + 1) → Submodule K V // ∃ (F : MooreBound.DegreeDiameter.CompleteFlag K V n), MooreBound.DegreeDiameter.flagPart parity F = P }

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.EvenPartialFlag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : Type u_2

The subspaces at even ranks of some complete flag.

Equations

• MooreBound.DegreeDiameter.EvenPartialFlag = MooreBound.DegreeDiameter.PartialFlag 0

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.OddPartialFlag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : Type u_2

The subspaces at odd ranks of some complete flag.

Equations

• MooreBound.DegreeDiameter.OddPartialFlag = MooreBound.DegreeDiameter.PartialFlag 1

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

theorem MooreBound.DegreeDiameter.PartialFlag.ext {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} {P Q : PartialFlag parity} (h : ∀ (i : Fin (n + 1)), ↑P i = ↑Q i) : P = Q

theorem MooreBound.DegreeDiameter.PartialFlag.ext_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} {P Q : PartialFlag parity} : P = Q ↔ ∀ (i : Fin (n + 1)), ↑P i = ↑Q i

def MooreBound.DegreeDiameter.PartialFlag.ofComplete {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (parity : ℕ) (F : CompleteFlag K V n) : PartialFlag parity

The partial flag of a complete flag at the selected parity.

Equations

• MooreBound.DegreeDiameter.PartialFlag.ofComplete parity F = ⟨MooreBound.DegreeDiameter.flagPart parity F, ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.ofComplete_val {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (parity : ℕ) (F : CompleteFlag K V n) : ↑(ofComplete parity F) = flagPart parity F

def MooreBound.DegreeDiameter.Compatible {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (P : EvenPartialFlag) (Q : OddPartialFlag) : Prop

An even and an odd partial flag are compatible when they are the two parts of one complete flag.

Equations

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

theorem MooreBound.DegreeDiameter.compatible_parts {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (F : CompleteFlag K V n) : Compatible (PartialFlag.ofComplete 0 F) (PartialFlag.ofComplete 1 F)

theorem MooreBound.DegreeDiameter.compatible_unique {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {P : EvenPartialFlag} {Q : OddPartialFlag} {F G : CompleteFlag K V n} (hF : PartialFlag.ofComplete 0 F = P) (hF' : PartialFlag.ofComplete 1 F = Q) (hG : PartialFlag.ofComplete 0 G = P) (hG' : PartialFlag.ofComplete 1 G = Q) : F = G

Even and odd parts determine their common complete flag uniquely.

def MooreBound.DegreeDiameter.halvedFlagGraph {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : SimpleGraph EvenPartialFlag

The graph on even partial flags in which distinct flags are adjacent when they have a common compatible odd partial flag.

Equations

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

theorem MooreBound.DegreeDiameter.halvedFlagGraph_adj_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {P P' : EvenPartialFlag} : halvedFlagGraph.Adj P P' ↔ P ≠ P' ∧ ∃ (Q : OddPartialFlag), Compatible P Q ∧ Compatible P' Q

theorem MooreBound.DegreeDiameter.evenPart_eq_of_alternatingStep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {s : Fin n} {F G : CompleteFlag K V n} (h : AlternatingStep K V s F G) (hs : (↑s + 1) % 2 = 1) : PartialFlag.ofComplete 0 F = PartialFlag.ofComplete 0 G

theorem MooreBound.DegreeDiameter.oddPart_eq_of_alternatingStep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {s : Fin n} {F G : CompleteFlag K V n} (h : AlternatingStep K V s F G) (hs : (↑s + 1) % 2 = 0) : PartialFlag.ofComplete 1 F = PartialFlag.ofComplete 1 G

theorem MooreBound.DegreeDiameter.halved_edist_le_one_of_parts {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (F₀ F₁ F₂ : CompleteFlag K V n) (heven : PartialFlag.ofComplete 0 F₀ = PartialFlag.ofComplete 0 F₁) (hodd : PartialFlag.ofComplete 1 F₁ = PartialFlag.ofComplete 1 F₂) : halvedFlagGraph.edist (PartialFlag.ofComplete 0 F₀) (PartialFlag.ofComplete 0 F₂) ≤ 1

Two even parts separated by an odd step and then an even step have extended graph distance at most one.

theorem MooreBound.DegreeDiameter.edist_chain_le {W : Type u_3} (G : SimpleGraph W) (P : ℕ → W) (m : ℕ) : (∀ j < m, G.edist (P j) (P (j + 1)) ≤ 1) → G.edist (P 0) (P m) ≤ ↑m

A chain with at most unit extended distance at every step has distance at most its number of steps.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_ediam_le {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (k : ℕ) : halvedFlagGraph.ediam ≤ ↑k

The odd-first alternating route of Lemma 2.1 projects to a route of at most k edges in the halved graph on a (2*k+1)-dimensional space.