Sharp realization length for Schur poset spaces

This file formalizes the final equality step in the manuscript's poset-space argument. Under the sharp numerical bound, the three-antichain detour forces every Schur object to be one-dimensional. A nonzero nonisomorphism between one-dimensional poset spaces then strictly enlarges its support, so every nonzero composable chain has at most one arrow per poset element.

noncomputable def MagnitudeConjecture.PosetSpace.support (k T : Type u) [Field k] [PartialOrder T] [Fintype T] (X : Obj k T) : Finset T

The support of a poset space: the indices whose distinguished subspace is the whole ambient space. For a one-dimensional space these are exactly its nonzero distinguished subspaces.

@[simp]

theorem MagnitudeConjecture.PosetSpace.mem_support (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {X : Obj k T} {t : T} : t ∈ support k T X ↔ X.subspace t = ⊤

theorem MagnitudeConjecture.PosetSpace.submodule_eq_bot_or_eq_top_of_finrank_eq_one (k : Type u) [Field k] {V : Type u} [AddCommGroup V] [Module k V] (hV : Module.finrank k V = 1) (S : Submodule k V) : S = ⊥ ∨ S = ⊤

Every subspace of a one-dimensional vector space is zero or the whole space.

theorem MagnitudeConjecture.PosetSpace.support_mono_of_ne_zero_of_finrank_eq_one (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {X Y : Obj k T} (f : X ⟶ Y) (hf : f ≠ 0) (hY : Module.finrank k Y.carrier = 1) : support k T X ⊆ support k T Y

A nonzero map into a one-dimensional poset space can only enlarge support.

theorem MagnitudeConjecture.PosetSpace.isIso_of_ne_zero_of_finrank_eq_one_of_support_eq (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {X Y : Obj k T} (f : X ⟶ Y) (hf : f ≠ 0) (hX : Module.finrank k X.carrier = 1) (hY : Module.finrank k Y.carrier = 1) (hsupport : support k T X = support k T Y) : CategoryTheory.IsIso f

A nonzero map between one-dimensional poset spaces with equal support is an isomorphism.

theorem MagnitudeConjecture.PosetSpace.support_ssubset_of_ne_zero_of_not_isIso_of_finrank_eq_one (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {X Y : Obj k T} (f : X ⟶ Y) (hf : f ≠ 0) (hnot : ¬CategoryTheory.IsIso f) (hX : Module.finrank k X.carrier = 1) (hY : Module.finrank k Y.carrier = 1) : support k T X ⊂ support k T Y

Thus a nonzero nonisomorphism between one-dimensional poset spaces strictly enlarges support.

structure MagnitudeConjecture.PosetSpace.SchurRealizationFamily (k T : Type u) [Field k] [PartialOrder T] (I : Type v) : Type (max (u + 1) v)

A family of Schur poset spaces together with the manuscript's numerical multiplicity, identified with total-space dimension. The primitive-factor realization will instantiate this structure on its surviving labels.

• obj : I → Obj k T
• schur (i : I) : IsSchur k T (self.obj i)
• multiplicity : I → ℕ
• multiplicity_eq_finrank (i : I) : self.multiplicity i = Module.finrank k (self.obj i).carrier

theorem MagnitudeConjecture.PosetSpace.SchurRealizationFamily.multiplicity_eq_one (k T : Type u) [Field k] [PartialOrder T] {I : Type v} (R : SchurRealizationFamily k T I) (hline : ∀ (X : Obj k T), IsSchur k T X → Module.finrank k X.carrier = 1) (i : I) : R.multiplicity i = 1

Any theorem forcing every Schur poset space to be a line immediately forces all multiplicities in a realized family to be one.

theorem MagnitudeConjecture.PosetSpace.hasNonzeroNonisomorphismLengthAtMost_card_of_finrank_eq_one (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {P : Obj k T → Prop} (hline : ∀ (X : Obj k T), P X → Module.finrank k X.carrier = 1) : HasNonzeroNonisomorphismLengthAtMost (Obj k T) P (Fintype.card T)

If every admissible poset space is one-dimensional, strict support growth bounds every nonzero chain of nonisomorphisms by the cardinality of the indexing poset.

theorem MagnitudeConjecture.PosetSpace.finrank_eq_one_of_isSchur_of_positiveGrading_of_le_card (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) (hL : L ≤ Fintype.card T) (X : Obj k T) (hX : IsSchur k T X) : Module.finrank k X.carrier = 1

Under the sharp numerical bound L ≤ |T|, the three-antichain detour rules out every higher-dimensional Schur object.

theorem MagnitudeConjecture.PosetSpace.schurLengthAtMostCard_of_positiveGrading_of_le_card (k T : Type u) [Field k] [PartialOrder T] [Fintype T] {L : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) (hL : L ≤ Fintype.card T) : HasNonzeroNonisomorphismLengthAtMost (Obj k T) (IsSchur k T) (Fintype.card T)

The frozen manuscript's sharp equality conclusion for the realization category: once L ≤ |T|, every nonzero composable chain of Schur nonisomorphisms has at most |T| arrows.