Symmetry and regularity of the halved flag graph

Linear automorphisms act on complete and partial flags. The common-apartment part of Lemma 2.1 supplies an automorphism taking any chosen completion of one vertex to a chosen completion of another. Consequently the action on even partial flags is transitive and the halved graph is regular.

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

@[simp]

theorem MooreBound.DegreeDiameter.submodule_map_symm_map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (e : V ≃ₗ[K] V) (S : Submodule K V) : Submodule.map (↑e.symm) (Submodule.map (↑e) S) = S

noncomputable def MooreBound.DegreeDiameter.CompleteFlag.map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (F : CompleteFlag K V n) : CompleteFlag K V n

Transport every member of a complete flag along a linear equivalence.

Equations

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

@[simp]

theorem MooreBound.DegreeDiameter.CompleteFlag.map_apply {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (F : CompleteFlag K V n) (i : Fin (n + 1)) : (map e F).space i = (Submodule.orderIsoMapComap e) (F.space i)

@[simp]

theorem MooreBound.DegreeDiameter.CompleteFlag.map_symm_map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (F : CompleteFlag K V n) : map e.symm (map e F) = F

@[simp]

theorem MooreBound.DegreeDiameter.CompleteFlag.map_map_symm {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (F : CompleteFlag K V n) : map e (map e.symm F) = F

theorem MooreBound.DegreeDiameter.CompleteFlag.map_ofBasis {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (b : Module.Basis (Fin n) K V) : map e (ofBasis b) = ofBasis (b.map e)

Transporting a basis flag transports its basis.

noncomputable def MooreBound.DegreeDiameter.PartialFlag.map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (P : PartialFlag parity) : PartialFlag parity

Transport a partial flag along a linear equivalence.

Equations

• MooreBound.DegreeDiameter.PartialFlag.map e P = ⟨fun (i : Fin (n + 1)) => (Submodule.orderIsoMapComap e) (↑P i), ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.map_val {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (P : PartialFlag parity) (i : Fin (n + 1)) : ↑(map e P) i = (Submodule.orderIsoMapComap e) (↑P i)

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.map_symm_map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (P : PartialFlag parity) : map e.symm (map e P) = P

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.map_map_symm {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (P : PartialFlag parity) : map e (map e.symm P) = P

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

Linear transport is an equivalence on partial flags.

Equations

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

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.mapEquiv_apply {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (P : PartialFlag parity) : (mapEquiv e) P = map e P

@[simp]

theorem MooreBound.DegreeDiameter.PartialFlag.map_ofComplete {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n parity : ℕ} (e : V ≃ₗ[K] V) (F : CompleteFlag K V n) : map e (ofComplete parity F) = ofComplete parity (CompleteFlag.map e F)

theorem MooreBound.DegreeDiameter.Compatible.map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {P : EvenPartialFlag} {Q : OddPartialFlag} (h : Compatible P Q) (e : V ≃ₗ[K] V) : Compatible (PartialFlag.map e P) (PartialFlag.map e Q)

theorem MooreBound.DegreeDiameter.compatible_map_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (P : EvenPartialFlag) (Q : OddPartialFlag) : Compatible (PartialFlag.map e P) (PartialFlag.map e Q) ↔ Compatible P Q

noncomputable def MooreBound.DegreeDiameter.halvedFlagGraphIso {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) : halvedFlagGraph ≃g halvedFlagGraph

Every linear equivalence acts by an automorphism of the halved graph.

Equations

• MooreBound.DegreeDiameter.halvedFlagGraphIso e = { toEquiv := MooreBound.DegreeDiameter.PartialFlag.mapEquiv e, map_rel_iff' := ⋯ }

@[simp]

theorem MooreBound.DegreeDiameter.halvedFlagGraphIso_apply {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (e : V ≃ₗ[K] V) (P : EvenPartialFlag) : (halvedFlagGraphIso e) P = PartialFlag.map e P

theorem MooreBound.DegreeDiameter.exists_halvedFlagGraphIso_map_eq {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (P P' : EvenPartialFlag) : ∃ (φ : halvedFlagGraph ≃g halvedFlagGraph), φ P = P'

Transitivity on even partial flags.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_natCard_neighborSet_eq {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (P P' : EvenPartialFlag) : Nat.card ↑(halvedFlagGraph.neighborSet P) = Nat.card ↑(halvedFlagGraph.neighborSet P')

All neighbor sets have the same finite cardinality.

theorem MooreBound.DegreeDiameter.exists_halvedFlagGraph_common_degree {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} [Nonempty EvenPartialFlag] : ∃ (Δ : ℕ), ∀ (P : EvenPartialFlag), Nat.card ↑(halvedFlagGraph.neighborSet P) = Δ

A common natural-number degree for all vertices, stated without making the particular Fintype structures on neighbor sets part of the theorem.