Documentation

LeanPool.MooreBound.DegreeDiameter.FlagSpace

The recursively split flag space #

This file contains only the neutral ambient vector-space model used by both the exact flag-graph construction and the big-cell lower-bound argument. Keeping it separate prevents the exact Proposition 3.1 chain from depending on the lower-bound construction merely to obtain this coordinate model.

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

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.FlagSpace (K : Type u) :

ℕ → Type u

The recursively split (2*k+1)-dimensional coordinate space.

Equations

MooreBound.DegreeDiameter.FlagSpace K 0 = (Fin 1 → K)
MooreBound.DegreeDiameter.FlagSpace K k.succ = ((Fin 2 → K) × MooreBound.DegreeDiameter.FlagSpace K k)

Instances For

def MooreBound.DegreeDiameter.flagDim :

The dimension of FlagSpace, kept recursive so adjoining its first two coordinates remains definitionally transparent.

Equations

Instances For

theorem MooreBound.DegreeDiameter.flagDim_eq (k : ℕ) :

flagDim k = 2 * k + 1

@[instance_reducible]

instance MooreBound.DegreeDiameter.flagSpaceAddCommGroup (K : Type u) [Field K] (k : ℕ) :

AddCommGroup (FlagSpace K k)

Equations

MooreBound.DegreeDiameter.flagSpaceAddCommGroup K 0 = { toAddGroup := Pi.addGroup, add_comm := ⋯ }
MooreBound.DegreeDiameter.flagSpaceAddCommGroup K k.succ = { toAddGroup := Prod.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

instance MooreBound.DegreeDiameter.flagSpaceModule (K : Type u) [Field K] (k : ℕ) :

Module K (FlagSpace K k)

Equations

MooreBound.DegreeDiameter.flagSpaceModule K 0 = { toDistribMulAction := Pi.distribMulAction K, add_smul := ⋯, zero_smul := ⋯ }
MooreBound.DegreeDiameter.flagSpaceModule K k.succ = { toDistribMulAction := Prod.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance MooreBound.DegreeDiameter.flagSpaceFiniteDimensional (K : Type u) [Field K] (k : ℕ) :

FiniteDimensional K (FlagSpace K k)

theorem MooreBound.DegreeDiameter.finrank_flagSpace (K : Type u) [Field K] (k : ℕ) :

Module.finrank K (FlagSpace K k) = flagDim k

instance MooreBound.DegreeDiameter.flagSpaceFinite (K : Type u) [Finite K] (k : ℕ) :

Finite (FlagSpace K k)

theorem MooreBound.DegreeDiameter.natCard_flagSpace (K : Type u) (k : ℕ) :

Nat.card (FlagSpace K k) = Nat.card K ^ flagDim k