A big cell of even partial flags

We construct a recursive affine cell inside the even partial flags. At one step the ambient space is K² × W. A linear map L : K² → W supplies its graph as the first retained two-dimensional subspace, and an even partial flag in W supplies all later retained subspaces. The graph recovers L; after L is known, inverse skew transport recovers the old partial flag. The resulting number of free scalar parameters satisfies d(k+1) = 2*(2*k+1) + d(k), hence d(k)=2*k².

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.submoduleProdEquiv {K : Type u_1} {X : Type u_2} {Y : Type u_3} [DivisionRing K] [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y] (P : Submodule K X) (Q : Submodule K Y) : ↥(P.prod Q) ≃ₗ[K] ↥P × ↥Q

The evident equivalence between a product submodule and the product of the two submodule types.

Equations

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

theorem MooreBound.DegreeDiameter.finrank_submodule_prod {K : Type u_1} {X : Type u_2} {Y : Type u_3} [DivisionRing K] [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y] [FiniteDimensional K X] [FiniteDimensional K Y] (P : Submodule K X) (Q : Submodule K Y) : Module.finrank K ↥(P.prod Q) = Module.finrank K ↥P + Module.finrank K ↥Q

noncomputable def MooreBound.DegreeDiameter.prependTwoComplete {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} (F : CompleteFlag K Y m) : CompleteFlag K ((Fin 2 → K) × Y) (m + 2)

Put the standard two-dimensional flag before a complete flag F.

Equations

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

def MooreBound.DegreeDiameter.shiftedRank (m : ℕ) (i : Fin (m + 1)) : Fin (m + 2 + 1)

Shift a rank in the old flag past the two newly prepended ranks.

Equations

• MooreBound.DegreeDiameter.shiftedRank m i = ⟨↑i + 2, ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.prependTwoComplete_shifted {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} (F : CompleteFlag K Y m) (i : Fin (m + 1)) : (prependTwoComplete F).space (shiftedRank m i) = ⊤.prod (F.space i)

def MooreBound.DegreeDiameter.skewEquiv {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] (L : (Fin 2 → K) →ₗ[K] Y) : ((Fin 2 → K) × Y) ≃ₗ[K] (Fin 2 → K) × Y

The lower block-unitriangular equivalence (x,y) ↦ (x, y + L x).

Equations

• MooreBound.DegreeDiameter.skewEquiv L = (LinearEquiv.refl K (Fin 2 → K)).skewProd (LinearEquiv.refl K Y) L

@[simp]

theorem MooreBound.DegreeDiameter.skewEquiv_apply {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] (L : (Fin 2 → K) →ₗ[K] Y) (z : (Fin 2 → K) × Y) : (skewEquiv L) z = (z.1, z.2 + L z.1)

theorem MooreBound.DegreeDiameter.map_top_prod_bot_skewEquiv {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] (L : (Fin 2 → K) →ₗ[K] Y) : Submodule.map (↑(skewEquiv L)) (⊤.prod ⊥) = L.graph

The image of the horizontal two-space under the skew equivalence is the graph of L.

theorem MooreBound.DegreeDiameter.linearMap_graph_injective {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] : Function.Injective fun (L : (Fin 2 → K) →ₗ[K] Y) => L.graph

noncomputable def MooreBound.DegreeDiameter.skewPrependComplete {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} (L : (Fin 2 → K) →ₗ[K] Y) (F : CompleteFlag K Y m) : CompleteFlag K ((Fin 2 → K) × Y) (m + 2)

Prepend two ranks and skew them so that rank two is graph L.

Equations

• MooreBound.DegreeDiameter.skewPrependComplete L F = MooreBound.DegreeDiameter.CompleteFlag.map (MooreBound.DegreeDiameter.skewEquiv L) (MooreBound.DegreeDiameter.prependTwoComplete F)

@[simp]

theorem MooreBound.DegreeDiameter.skewPrependComplete_shifted {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} (L : (Fin 2 → K) →ₗ[K] Y) (F : CompleteFlag K Y m) (i : Fin (m + 1)) : (skewPrependComplete L F).space (shiftedRank m i) = Submodule.map (↑(skewEquiv L)) (⊤.prod (F.space i))

theorem MooreBound.DegreeDiameter.skewPrependComplete_rank_two {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} (L : (Fin 2 → K) →ₗ[K] Y) (F : CompleteFlag K Y m) : (skewPrependComplete L F).space (shiftedRank m 0) = L.graph

theorem MooreBound.DegreeDiameter.skewPrepend_evenPart_recover {K : Type u_1} {Y : Type u_3} [DivisionRing K] [AddCommGroup Y] [Module K Y] {m : ℕ} {L M : (Fin 2 → K) →ₗ[K] Y} {F G : CompleteFlag K Y m} (h : PartialFlag.ofComplete 0 (skewPrependComplete L F) = PartialFlag.ofComplete 0 (skewPrependComplete M G)) : L = M ∧ PartialFlag.ofComplete 0 F = PartialFlag.ofComplete 0 G

Equality of the new even parts recovers both the graph parameter and the old even part.

def MooreBound.DegreeDiameter.BigCell (K : Type u) [Field K] : ℕ → Type u

The recursive affine parameter space.

Equations

• MooreBound.DegreeDiameter.BigCell K 0 = ULift.{?u.1, 0} Unit
• MooreBound.DegreeDiameter.BigCell K k.succ = (((Fin 2 → K) →ₗ[K] MooreBound.DegreeDiameter.FlagSpace K k) × MooreBound.DegreeDiameter.BigCell K k)

instance MooreBound.DegreeDiameter.bigCellFinite (K : Type u) [Field K] [Finite K] (k : ℕ) : Finite (BigCell K k)

noncomputable def MooreBound.DegreeDiameter.representativeComplete (K : Type u) [Field K] {V : Type u_1} [AddCommGroup V] [Module K V] {n parity : ℕ} (P : PartialFlag parity) : CompleteFlag K V n

Choose a complete representative of a partial flag.

Equations

• MooreBound.DegreeDiameter.representativeComplete K P = Classical.choose ⋯

theorem MooreBound.DegreeDiameter.representativeComplete_part (K : Type u) [Field K] {V : Type u_1} [AddCommGroup V] [Module K V] {n parity : ℕ} (P : PartialFlag parity) : PartialFlag.ofComplete parity (representativeComplete K P) = P

noncomputable def MooreBound.DegreeDiameter.bigCellFlag (K : Type u) [Field K] (k : ℕ) : BigCell K k → EvenPartialFlag

The big-cell injection into even partial flags.

Equations

• One or more equations did not get rendered due to their size.
• MooreBound.DegreeDiameter.bigCellFlag K 0 x_2 = MooreBound.DegreeDiameter.PartialFlag.ofComplete 0 (MooreBound.DegreeDiameter.CompleteFlag.ofBasis (Pi.basisFun K (Fin 1)))

theorem MooreBound.DegreeDiameter.bigCellFlag_injective (K : Type u) [Field K] (k : ℕ) : Function.Injective (bigCellFlag K k)

theorem MooreBound.DegreeDiameter.natCard_linearMap_from_two (K : Type u) [Field K] (k : ℕ) : Nat.card ((Fin 2 → K) →ₗ[K] FlagSpace K k) = Nat.card K ^ (2 * flagDim k)

theorem MooreBound.DegreeDiameter.natCard_bigCell (K : Type u) [Field K] (k : ℕ) : Nat.card (BigCell K k) = Nat.card K ^ (2 * k * k)

theorem MooreBound.DegreeDiameter.natCard_evenPartialFlag_lower (K : Type u) [Field K] [Finite K] (k : ℕ) : Nat.card K ^ (2 * k * k) ≤ Nat.card EvenPartialFlag

The 2*k²-dimensional affine cell gives the required vertex lower bound.