Coordinate subspaces and Schur poset spaces

This file isolates the linear-algebraic endpoint of the manuscript's common-adapted-basis argument. Once all distinguished subspaces of a poset space are coordinate subspaces for one basis, a coordinate projection is a poset-space endomorphism. The Schur condition then forces total dimension at most one.

def MagnitudeConjecture.PosetSpace.AdaptedBasis.AdaptsSubmodule {k V : Type u} [Field k] [AddCommGroup V] [Module k V] {ι : Type v} (b : Module.Basis ι k V) (U : Submodule k V) : Prop

A subspace is adapted to a basis when it is spanned by a subset of the basis vectors.

noncomputable def MagnitudeConjecture.PosetSpace.AdaptedBasis.coordinateProjection {k V : Type u} [Field k] [AddCommGroup V] [Module k V] {ι : Type v} (b : Module.Basis ι k V) (i : ι) : V →ₗ[k] V

Projection onto one basis coordinate.

@[simp]

theorem MagnitudeConjecture.PosetSpace.AdaptedBasis.coordinateProjection_self {k V : Type u} [Field k] [AddCommGroup V] [Module k V] {ι : Type v} (b : Module.Basis ι k V) (i : ι) : (coordinateProjection b i) (b i) = b i

@[simp]

theorem MagnitudeConjecture.PosetSpace.AdaptedBasis.coordinateProjection_of_ne {k V : Type u} [Field k] [AddCommGroup V] [Module k V] {ι : Type v} (b : Module.Basis ι k V) {i j : ι} (hji : j ≠ i) : (coordinateProjection b i) (b j) = 0

theorem MagnitudeConjecture.PosetSpace.AdaptedBasis.coordinateProjection_mem_of_mem {k V : Type u} [Field k] [AddCommGroup V] [Module k V] {ι : Type v} (b : Module.Basis ι k V) {U : Submodule k V} (hU : AdaptsSubmodule b U) (i : ι) {x : V} (hx : x ∈ U) : (coordinateProjection b i) x ∈ U

A coordinate projection preserves every subspace adapted to the basis.

def MagnitudeConjecture.PosetSpace.HasCommonAdaptedBasis {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) : Prop

All distinguished subspaces of X are coordinate subspaces for one finite basis.

noncomputable def MagnitudeConjecture.PosetSpace.coordinateProjectionHom {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (b : Module.Basis (Fin (Module.finrank k X.carrier)) k X.carrier) (hb : ∀ (t : T), AdaptedBasis.AdaptsSubmodule b (X.subspace t)) (i : Fin (Module.finrank k X.carrier)) : X ⟶ X

A coordinate projection, regarded as an endomorphism of a poset space.

theorem MagnitudeConjecture.PosetSpace.finrank_le_one_of_isSchur_of_hasCommonAdaptedBasis {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) (hadapted : HasCommonAdaptedBasis X) : Module.finrank k X.carrier ≤ 1

A Schur poset space admitting a common adapted basis has total dimension at most one.

theorem MagnitudeConjecture.PosetSpace.finrank_eq_one_of_isSchur_of_hasCommonAdaptedBasis {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) (hadapted : HasCommonAdaptedBasis X) : Module.finrank k X.carrier = 1

In particular, a nonzero Schur poset space with a common adapted basis is one-dimensional.