Finite chains of subspaces and basis flags

This file proves the linear-algebraic bridge from a finite chain of subspaces to a complete basis flag containing that chain.

theorem MagnitudeConjecture.PosetSpace.finrank_flag {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) (m : Fin (n + 1)) : Module.finrank k ↥(b.flag m) = ↑m

The m-th subspace in a basis flag has dimension m.

noncomputable def MagnitudeConjecture.PosetSpace.appendQuotientBasis {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] (U : Submodule k V) {d q : ℕ} (bU : Module.Basis (Fin d) k ↥U) (bQ : Module.Basis (Fin q) k (V ⧸ U)) : Module.Basis (Fin (d + q)) k V

Append a basis of the quotient by U after a basis of U.

@[simp]

theorem MagnitudeConjecture.PosetSpace.appendQuotientBasis_castAdd {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] (U : Submodule k V) {d q : ℕ} (bU : Module.Basis (Fin d) k ↥U) (bQ : Module.Basis (Fin q) k (V ⧸ U)) (i : Fin d) : (appendQuotientBasis U bU bQ) (Fin.castAdd q i) = ↑(bU i)

theorem MagnitudeConjecture.PosetSpace.map_flag_eq_appendQuotientBasis_flag {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (U : Submodule k V) {d q : ℕ} (bU : Module.Basis (Fin d) k ↥U) (bQ : Module.Basis (Fin q) k (V ⧸ U)) (m : Fin (d + 1)) : Submodule.map U.subtype (bU.flag m) = (appendQuotientBasis U bU bQ).flag ⟨↑m, ⋯⟩

A flag subspace of the basis of U becomes the same initial flag subspace after appending a quotient basis.

theorem MagnitudeConjecture.PosetSpace.exists_flag_basis_of_finset_chain {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (C : Finset (Submodule k V)) (hC : IsChain (fun (x1 x2 : Submodule k V) => x1 ≤ x2) ↑C) : ∃ (b : Module.Basis (Fin (Module.finrank k V)) k V), ∀ U ∈ C, ∃ (m : Fin (Module.finrank k V + 1)), U = b.flag m

Every finite chain of subspaces of a finite-dimensional vector space is contained in the complete flag of some basis.

theorem MagnitudeConjecture.PosetSpace.hasFlagBasisOn_of_isChain {k : Type u} [Field k] {T : Type u} [PartialOrder T] [Fintype T] (X : Obj k T) (S : Set T) (hS : IsChain (fun (x1 x2 : T) => x1 ≤ x2) S) : HasFlagBasisOn X S

A chain of indices gives a family of distinguished subspaces lying in one complete basis flag.

theorem MagnitudeConjecture.PosetSpace.finrank_eq_one_of_isSchur_of_two_chain_cover {k : Type u} [Field k] {T : Type u} [PartialOrder T] [Fintype T] (X : Obj k T) (hschur : IsSchur k T X) (A B : Set T) (hcover : A ∪ B = Set.univ) (hA : IsChain (fun (x1 x2 : T) => x1 ≤ x2) A) (hB : IsChain (fun (x1 x2 : T) => x1 ≤ x2) B) : Module.finrank k X.carrier = 1

If two chains cover the indexing poset, every Schur poset space is one-dimensional.